Integers and Mathematical Correctness

Integers and Mathematical Correctness

[chris.danx]

Hi,

To most this may seem insignificant but I'm more mathematically minded and I
just found something out.  Many programming languages don't implement
division properly!

For example -3/2 should be -2 not -1, with a remainder 1 not -1.

I'm trying to implement integer division the "proper" way (according to
Euclid), just for fun (and to provide a mathematically correct package for
anyone who gets annoyed by this).


The problem is this...

   type c_integer is new integer;

   function "/" (a, b : c_integer) return c_integer is
   begin
      return standard."/" (a, b); -- simple test of override
   end "/";

The line > standard."/" (a, b) doesn't work!  I check the RM and the "/" for
integers is defined in standard, but it's not accepting it (this is just a
simple stub, it doesn't implement division properly for negatives yet!!!
The div is correct for non-negatives though).

Note: this works

xxx : c_integer := c_integer(-3)/c_integer(2);

when the above function is commented out!

What small detail am I missing this time?

Thanks,
Chris

Re: Integers and Mathematical Correctness

[David C. Hoos]

----- Original Message ----- 
From: "chris.danx" <chris.danx@ntlworld.com>
<snip>
>    type c_integer is new integer;
> 
>    function "/" (a, b : c_integer) return c_integer is
>    begin
>       return standard."/" (a, b); -- simple test of override
If you want to use Standard."/" here, you must convert
a and b to Integer, because Standard doesn't know about
c_integer.
>    end "/";
> 
<snip>

Re: Integers and Mathematical Correctness

[Mark Johnson]

"chris.danx" wrote:

> [snip]

> The problem is this...
>
>    type c_integer is new integer;
>
>    function "/" (a, b : c_integer) return c_integer is
>    begin
>       return standard."/" (a, b); -- simple test of override
>    end "/";
>
> The line > standard."/" (a, b) doesn't work!  I check the RM and the "/" for
> integers is defined in standard, but it's not accepting it (this is just a
> simple stub, it doesn't implement division properly for negatives yet!!!
> The div is correct for non-negatives though).

How about the following. I found w/ GNAT on Linux that...
  Z := "/"(X, Y);
where Z, X, and Y are all of the type C_Integer works just fine - if you want
that syntax.

Why the use of Standard."/" does not work I will leave to other language
lawyers.
  --Mark

Re: Integers and Mathematical Correctness

[chris.danx]

"David C. Hoos" <david.c.hoos.sr@ada95.com> wrote in message
news:mailman.1004563184.27931.comp.lang.ada@ada.eu.org...
>
> ----- Original Message -----
> From: "chris.danx" <chris.danx@ntlworld.com>
> <snip>
> >    type c_integer is new integer;
> >
> >    function "/" (a, b : c_integer) return c_integer is
> >    begin
> >       return standard."/" (a, b); -- simple test of override

> If you want to use Standard."/" here, you must convert
> a and b to Integer, because Standard doesn't know about
> c_integer.

why does

xxx : c_integer := c_integer(-3)/c_integer(2);

work then?  Is it not the same?

Thanks,
Chris

RE: Integers and Mathematical Correctness

[Beard, Frank]

-----Original Message-----
From: chris.danx [mailto:chris.danx@ntlworld.com]

> why does
>
> xxx : c_integer := c_integer(-3)/c_integer(2);  work then?
                                  ^
Because --------------------------^ this operator
is inherited from integer for the new type.  This
division operator is for the new derived type
c_integer.  Remember "new" causes it to be treated as
a unique type (i.e. they can't be intermixed without
conversion).


>Is it not the same?
No, it's for the derived type.

Now if you did the following, it would be the same
(same being, it would use Standard integer).

xxx : c_integer := c_integer(-3/2);

or maybe

xxx : c_integer := c_integer(integer(-3)/integer(2));

The first may be universal integer, whereas, the second
is integer.

Frank

Re: Integers and Mathematical Correctness

[David C. Hoos]

----- Original Message ----- 
From: "chris.danx" <chris.danx@ntlworld.com>
Newsgroups: comp.lang.ada
To: <comp.lang.ada@ada.eu.org>
Sent: Wednesday, October 31, 2001 4:16 PM
Subject: Re: Integers and Mathematical Correctness
<snip>
> why does
> 
> xxx : c_integer := c_integer(-3)/c_integer(2);
> work then?  Is it not the same?

No.  The "/" operator in the above line is the new
operator for the c_integer type you declared, and it's
not the same as any of the Standard."/" operators
(i.e., for Integer, Float, etc.).

A new type means exactly _that_ -- a _new_ type,
with new operators.
 
<snip>

Re: Integers and Mathematical Correctness

[chris.danx]

> > why does
> >
> > xxx : c_integer := c_integer(-3)/c_integer(2);
> > work then?  Is it not the same?
>
> No.  The "/" operator in the above line is the new
> operator for the c_integer type you declared, and it's
> not the same as any of the Standard."/" operators
> (i.e., for Integer, Float, etc.).
>
> A new type means exactly _that_ -- a _new_ type,
> with new operators.

So when a new integer type is declared, a group of operators are created for
that type but their behaviour can be still be changed?  Ok, I get it now!

Thanks,
Chris

Re: Integers and Mathematical Correctness

[Matthew Heaney]

"chris.danx" <chris.danx@ntlworld.com> wrote in message
news:Ij%D7.47224$a14.5418893@news6-win.server.ntlworld.com...
> So when a new integer type is declared, a group of operators are created
for
> that type but their behaviour can be still be changed?  Ok, I get it now!

Yes.  This is the same inheritance model like any other OO language.  In
general:

package P is

   type T is <whatever>;
   procedure Op (O : T);
...
end P;

package Q is
   type NT is new T;
end;

At the point of declaration of Q.NT, operation Q.Op is implicitly declared.

It doesn't matter that the parent type in your example was
Standard.Integer -- the model is the same.  Primitive operations of the
parent type are inherited by the derived type.

In the case of predefined types, you can "squirral away" (ha ha, Bob) a
predefined operator prior to overriding it:

package Q is
   type My_Integer is new Integer;
   function Predefined_Div (L, R: My_Integer) return My_Integer renames "/";
   function "/" (L, R : My_Integer) return My_Integer; --override
end;

The saves you the trouble of having to convert back to the parent type in
the body, when you need the predefined behavior (here, for division).

Re: Integers and Mathematical Correctness

[Wes Groleau]

"chris.danx" wrote:
> To most this may seem insignificant but I'm more mathematically minded and I
> just found something out.  Many programming languages don't implement
> division properly!

In the case of Ada, "properly" means

   (-A)/B = -(A/b) = A/(-B)     RM95 4.5.5(6-7)

See also the notes on the next page (para. 23-30).
If the compiler doesn't do this, send a bug report.

If your c_integer package is going to do something
else, I would advise the following comment at the
beginning of it:

-- NOTE: This package redefines integer division
--       for the benefit of folks who think the
--       RM definition is stupid.  Do not expect
--       division of these types to behave like
--       other integer types!

-- 
Wes Groleau
http://freepages.rootsweb.com/~wgroleau

Re: Integers and Mathematical Correctness

[Charles Sampson]

chris.danx <chris.danx@ntlworld.com> wrote:

> Hi,
> 
> To most this may seem insignificant but I'm more mathematically minded and I
> just found something out.  Many programming languages don't implement
> division properly!
> 
> For example -3/2 should be -2 not -1, with a remainder 1 not -1.
> 
> I'm trying to implement integer division the "proper" way (according to
> Euclid), just for fun (and to provide a mathematically correct package for
> anyone who gets annoyed by this).

     I'm not sure how you determined that the "proper" definition of 
integer division is to return floor (a/b), where "/" is mathematical 
division.  The definition used by most programming languages preserves 
the very useful property -(a/b) = (-a)/b = a/(-b), where this time "/" 
represents integer division.

     Please explain the Euclid reference.  I don't have any History of 
Mathematics books available, but I don't remember that Euclid had nega-
tive numbers to work with.

                                Charlie

Re: Integers and Mathematical Correctness

[Charles Lindsey]

In <h8ZD7.46340$a14.5285167@news6-win.server.ntlworld.com> "chris.danx" <chris.danx@ntlworld.com> writes:


>Hi,

>To most this may seem insignificant but I'm more mathematically minded and I
>just found something out.  Many programming languages don't implement
>division properly!

>For example -3/2 should be -2 not -1, with a remainder 1 not -1.

Yes, the history of this goes back a long way, to ALGOL 60. The Europeans
(who were all mathematicians) were happy to define division for Reals and
were not particularly interested in integers. The Americans (who were all
programmers) saw a need for it, so the Europeans just said "OK, how do you
want to define it", and the Americans responded with the "obvious" and ONE
TRUE (i.e. FORTRAN) WAY.

Then, of course, hardware got to be built the "wrong" way. In every
subsequent programming language (ALGOL 68, Pascal, Ada) the language
designers knew perfectly well that they were designing it wrong, but dared
not make the change. I railed against this in 1983, and that is more or
less what I was told :-( .

-- 
Charles H. Lindsey ---------At Home, doing my own thing------------------------
Tel: +44 161 436 6131 Fax: +44 161 436 6133   Web: http://www.cs.man.ac.uk/~chl
Email: chl@clw.cs.man.ac.uk      Snail: 5 Clerewood Ave, CHEADLE, SK8 3JU, U.K.
PGP: 2C15F1A9      Fingerprint: 73 6D C2 51 93 A0 01 E7 65 E8 64 7E 14 A4 AB A5

Re: Integers and Mathematical Correctness

[wilhelm.spickermann]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain; charset=us-ascii, Size: 1177 bytes --]


On 01-Nov-01 Wes Groleau wrote:
> If your c_integer package is going to do something
> else, I would advise the following comment at the
> beginning of it:
> 
> -- NOTE: This package redefines integer division
> --       for the benefit of folks who think the
> --       RM definition is stupid.  Do not expect
> --       division of these types to behave like
> --       other integer types!
> 

I think, thats going too far. I, for instance, do not not believe
the "RM definition is stupid" -- it just reflects the abilities
of normal hardware and that is a *good* idea (thanks to Robert
Dewar for pointing me on that fact). I will not use the
c_integer_package, but only because it cannot make the old
division operator vanish completely and I don�t want to have two
of them with the same name and a different semantics.

But: It would be much more practical, if the division operator
(and the hardware) would be the way Chris Danx called
"mathematically correct". Most programs with integer division
- avoid negative numbers or 
- have to do additional operations which would not be necessary
  with mathematical."/" and "mod" or
- would be equally complex.

Wilhelm

Re: Integers and Mathematical Correctness

[Marin David Condic]

Just because I think the Ada attributes for math (and, of course, other
stuff) are really cool things to have, I thought I'd mention: ARM Annex K
wherein you can find S'Ceiling and S'Floor. They apply to floating point
types, but they might be interesting in this context anyway. I don't know of
other languages providing so many handy mathematical attributes that let you
develop code for portability and/or precise behavior. Its one more reason
why Ada ought to be of interest to those doing mathematical/scientific
programming.

MDC
--
Marin David Condic
Senior Software Engineer
Pace Micro Technology Americas    www.pacemicro.com
Enabling the digital revolution
e-Mail:    marin.condic@pacemicro.com
Web:      http://www.mcondic.com/


"Charles Sampson" <csampson@inetworld.net> wrote in message
news:1f26o22.1xfvwvo111pfi4N%csampson@inetworld.net...
> chris.danx <chris.danx@ntlworld.com> wrote:
> > I'm trying to implement integer division the "proper" way (according to
> > Euclid), just for fun (and to provide a mathematically correct package
for
> > anyone who gets annoyed by this).
>
>      I'm not sure how you determined that the "proper" definition of
> integer division is to return floor (a/b), where "/" is mathematical
> division.  The definition used by most programming languages preserves
> the very useful property -(a/b) = (-a)/b = a/(-b), where this time "/"
> represents integer division.

Re: Integers and Mathematical Correctness

[chris.danx]

> "chris.danx" wrote:
> > To most this may seem insignificant but I'm more mathematically minded
and I
> > just found something out.  Many programming languages don't implement
> > division properly!
>
> In the case of Ada, "properly" means
>
>    (-A)/B = -(A/b) = A/(-B)     RM95 4.5.5(6-7)
>
> See also the notes on the next page (para. 23-30).
> If the compiler doesn't do this, send a bug report.
>
> If your c_integer package is going to do something
> else, I would advise the following comment at the
> beginning of it:
>
> -- NOTE: This package redefines integer division
> --       for the benefit of folks who think the
> --       RM definition is stupid.  Do not expect
> --       division of these types to behave like
> --       other integer types!

When did I say it was stupid?  I said it's technically incorrect, not that
it's stupid.  Division is performed this way in Ada because ppl expect it to
be.  They are taught it wrongly, they are taught that negative remainders
are allowed which changes the whole division.

It is not stupid because ppl expect it to be this way, but it is technically
mathematically incorrect.


Chris

Re: Integers and Mathematical Correctness

[chris.danx]

"Charles Sampson" <csampson@inetworld.net> wrote in message
news:1f26o22.1xfvwvo111pfi4N%csampson@inetworld.net...
> chris.danx <chris.danx@ntlworld.com> wrote:
>
> > Hi,
> >
> > To most this may seem insignificant but I'm more mathematically minded
and I
> > just found something out.  Many programming languages don't implement
> > division properly!
> >
> > For example -3/2 should be -2 not -1, with a remainder 1 not -1.
> >
> > I'm trying to implement integer division the "proper" way (according to
> > Euclid), just for fun (and to provide a mathematically correct package
for
> > anyone who gets annoyed by this).
>
>      I'm not sure how you determined that the "proper" definition of
> integer division is to return floor (a/b), where "/" is mathematical
> division.  The definition used by most programming languages preserves
> the very useful property -(a/b) = (-a)/b = a/(-b), where this time "/"
> represents integer division.
>
>      Please explain the Euclid reference.  I don't have any History of
> Mathematics books available, but I don't remember that Euclid had nega-
> tive numbers to work with.

According to Euclid, the "division algorithm" (which isn't an algorithm)
asserts that for a/b

a = kb + r

where r >= 0
      k <- Integers


[For anyone unfamiliar with Haskell or (possibly) other functional languages
"<-" reads as "is a member of"].

So for -4 / 3

-4 = 3k + r

r > 0, so k = -2

-4 = 3(-2) + r
-4 = -6 + r
r  = 2

however in Ada (and others) this is,

-4/3 = -1

-4 = 3k + r
-4 = 3(-1) + r
-4 = -3 + r
r  = -1

Which is wrong!  r can never be negative according to Euclid.

Tons on the division algorithm can be found on the net,
http://www.utm.edu/research/primes/glossary/DivisionAlgorithm.html is one
such resource but I'm having trouble finding any history.  I don't know if
Euclid had negatives, but the Division Algorithm works for negatives.

This page has something on it (coding it in C),

http://www.csclub.uwaterloo.ca/~mpslager/compsci/GCD.html#Division%20Algorit
hm


Bye,
Chris

Re: Integers and Mathematical Correctness

[Chad Robert Meiners]

On Thu, 1 Nov 2001, chris.danx wrote:

>
> "Charles Sampson" <csampson@inetworld.net> wrote in message
> news:1f26o22.1xfvwvo111pfi4N%csampson@inetworld.net...
> > chris.danx <chris.danx@ntlworld.com> wrote:
> >
> > > Hi,
> > >
> > > To most this may seem insignificant but I'm more mathematically minded
> and I
> > > just found something out.  Many programming languages don't implement
> > > division properly!
> > >
> > > For example -3/2 should be -2 not -1, with a remainder 1 not -1.
> > >
> > > I'm trying to implement integer division the "proper" way (according to
> > > Euclid), just for fun (and to provide a mathematically correct package
> for
> > > anyone who gets annoyed by this).
> >
> >      I'm not sure how you determined that the "proper" definition of
> > integer division is to return floor (a/b), where "/" is mathematical
> > division.  The definition used by most programming languages preserves
> > the very useful property -(a/b) = (-a)/b = a/(-b), where this time "/"
> > represents integer division.
> >
> >      Please explain the Euclid reference.  I don't have any History of
> > Mathematics books available, but I don't remember that Euclid had nega-
> > tive numbers to work with.
>
> According to Euclid, the "division algorithm" (which isn't an algorithm)
> asserts that for a/b
>
> a = kb + r
>
> where r >= 0
>       k <- Integers

Shouldn't it be

where 0 <= r < b
      K <- Integers

otherwise k could be -3 and r would then be 5.

-CRM

Re: Integers and Mathematical Correctness

[Wes Groleau]

"chris.danx" wrote:
> According to Euclid, the "division algorithm" (which isn't an algorithm)
> asserts that for a/b
> 
> a = kb + r
> 
> where r >= 0
>       k <- Integers
>
> .....  r can never be negative according to Euclid.

I have a lot of respect for Euclid, but the issue for
a programming language is what's useful.  I have never
seen a problem I could blame on non-Euclidean division.

-- 
Wes Groleau
http://freepages.rootsweb.com/~wgroleau

Re: Integers and Mathematical Correctness

[Tucker Taft]

"chris.danx" wrote:
> ...
> The problem is this...
> 
>    type c_integer is new integer;
> 
>    function "/" (a, b : c_integer) return c_integer is
>    begin
>       return standard."/" (a, b); -- simple test of override
>    end "/";
> 
> The line > standard."/" (a, b) doesn't work!  I check the RM and the "/" for
> integers is defined in standard, but it's not accepting it...

Change the line to:

     return standard."/"(integer(a), integer(b));

The "/" in standard operates on integer, not c_integer.

In fact, you don't need the "standard." part because
overload resolution will find the operator, so long
as you do the conversion.  Hence, the following will work:

    return integer(a) / integer(b);

Or if you want to ensure that the remainder is positive:

    if a < 0 then
        return - ((-integer(a))/integer(b));
    else
        return integer(a)/integer(b);
    end if;

[Note that this might overflow if integer(a) = integer'first.]


> ...
> Thanks,
> Chris

-- 
-Tucker Taft   stt@avercom.net   http://www.avercom.net
Chief Technology Officer, AverCom Corporation (A Titan Company) 
Bedford, MA  USA (AverCom was formerly the Commercial Division of AverStar:
http://www.averstar.com/~stt)

Re: Integers and Mathematical Correctness

[Wilhelm Spickermann]

--On Thursday, November 01, 2001 16:11:06 +0000 Charles Lindsey 
<chl@clw.cs.man.ac.uk> wrote:

> Then, of course, hardware got to be built the "wrong" way. In
> every subsequent programming language (ALGOL 68, Pascal, Ada)
> the language designers knew perfectly well that they were
> designing it wrong, but dared not make the change. I railed
> against this in 1983, and that is more or less what I was told
> :-( .

At least Niklaus Wirth was daring enough -- Oberon had a 
"div"-Operator obeying
x=(x div y)*y+(x mod y)   and
0<=(x mod y)<y or y<(x mod y)<=0

Wilhelm

Re: Integers and Mathematical Correctness

[David Starner]

On Wed, 31 Oct 2001 20:27:16 -0000, chris.danx <chris.danx@ntlworld.com> wrote:
> To most this may seem insignificant but I'm more mathematically minded and I
> just found something out.  Many programming languages don't implement
> division properly!
> 
> For example -3/2 should be -2 not -1, with a remainder 1 not -1.

I guess this was a big deal in Forth, so "Forth, the New Model" covers
it in detail. (It's a nice book, and you can find it for pretty cheap.)
Basically, a division is correct if

dividend / divisor = quotient, modulus 
	implies that 
(quotient * divisor) + modulus = dividend 
	But 
(-2 * 2) + 1 = -3 = (-1 * 2) + -1. 
The first is division floored to negative infinity, and the second is 
division symmetric around zero, and either are valid. Forth-83 picked
the first, and Ada and Forth-79 picked the second. (ANSI Forth, being a
standard, cut the difference and offered operators for both.)

-- 
David Starner - dstarner98@aasaa.ofe.org
Pointless website: http://dvdeug.dhis.org
"I saw a daemon stare into my face, and an angel touch my breast; each 
one softly calls my name . . . the daemon scares me less."
- "Disciple", Stuart Davis

Re: Integers and Mathematical Correctness

[Mark Johnson]

Mark Johnson wrote:

>
> Why the use of Standard."/" does not work I will leave to other language
> lawyers.

I just figured this part out. The following example compiles cleanly with GNAT on
Linux...

procedure C is
  type C_Integer is new Integer;
  X, Y, Z : C_Integer;
begin
  Z := X/Y;
  Z := "/"(X, Y);
  Z := C."/"(X, Y);
end C;

You can't use Standard."/" because as others have pointed out - that is for
Integers (and other Standard types) only. C_Integers are defined in procedure C
(in this example), so the proper prefix to refer to the function "/" is C, not
Standard.
  --Mark

Re: Integers and Mathematical Correctness

[chris.danx]

> Shouldn't it be
> 
> where 0 <= r < b
>       K <- Integers
> 
> otherwise k could be -3 and r would then be 5.

Yes!  Sorry.

Re: Integers and Mathematical Correctness

[chris.danx]

> >To most this may seem insignificant but I'm more mathematically minded
and I
> >just found something out.  Many programming languages don't implement
> >division properly!
>
> >For example -3/2 should be -2 not -1, with a remainder 1 not -1.
>
> Yes, the history of this goes back a long way, to ALGOL 60. The Europeans
> (who were all mathematicians) were happy to define division for Reals and
> were not particularly interested in integers. The Americans (who were all
> programmers) saw a need for it, so the Europeans just said "OK, how do you
> want to define it", and the Americans responded with the "obvious" and ONE
> TRUE (i.e. FORTRAN) WAY.
>
> Then, of course, hardware got to be built the "wrong" way. In every
> subsequent programming language (ALGOL 68, Pascal, Ada) the language
> designers knew perfectly well that they were designing it wrong, but dared
> not make the change.

> I railed against this in 1983, and that is more or
> less what I was told :-( .

Interesting.

We only learned that in programming languages (and primary school),
technically division is incorrect the other day, and I was a bitty
surprised.  I don't really mind that it's "wrong", the package is just being
written as a little distraction.  I may never need it, but it's there if I
do.

Anyone wants it, let me know and I'll send it to you when I'm done.


Bye,
Chris

Re: Integers and Mathematical Correctness

[Wilhelm Spickermann]

--On Thursday, November 01, 2001 18:54:34 +0000 David Starner 
<dvdeug@x8b4e53cd.dhcp.okstate.edu> wrote:

> Basically, a division is correct if
>
> dividend / divisor = quotient, modulus
> 	implies that
> (quotient * divisor) + modulus = dividend
> 	But
> (-2 * 2) + 1 = -3 = (-1 * 2) + -1.
> The first is division floored to negative infinity, and the
> second is  division symmetric around zero, and either are
> valid. Forth-83 picked

Both Equations are valid, but only the first one (the first 
part) uses a modulus -- the second one uses a remainder. A 
modulus can take only abs(divisor) different values while a 
remainder can take 2*abs(divisor)-1 different values.

Wilhelm

RE: Integers and Mathematical Correctness

[Steven Deller]

> >To most this may seem insignificant but I'm more
> mathematically minded
> and I just found something out.  Many programming languages
> don't implement division properly!
...
> Interesting.
>
> We only learned that in programming languages (and primary school),
> technically division is incorrect the other day, and I was a bitty
> surprised.  I don't really mind that it's "wrong", the
> package is just being
> written as a little distraction.  I may never need it, but
> it's there if I
> do.
>
> Anyone wants it, let me know and I'll send it to you when I'm done.
>
> Bye,
> Chris

Chris,
I too am mathematically minded.  And the proclaimed "definition of division"
is a proclamation of mathematical charlatans.

What I find interesting is the leap to proclaim there is one and only one
proper definition of division simply because there a proof of one particular
theorem about integers that has one proof (of many possible) using algorithm
construction and proving the algorithm by making use of the Well-Ordering
Principle.

The Well-Ordering Principle applies only for sets of positive integers, so
it was important in the algorithm proof to have the remainder (r) limited to
be a positive integer.  It is additional unfortunate that the algorithmic
proof was dubbed "The Division Algorithm".  It should have been called
"Algorithm For Proving Uniqueness of Integers Selected with Certain
Extended-Ring Properties" If I remember correctly the existence of both *
and + would make this a Ring theorem.  Negative numbers require an inverse
"existence" postulate that I don't believe Rings have.  Does that make this
a Field (I'm trying to recall lessons learned 40 years ago :-) ).

The presence of that theorem and the "deemed" name of the algorithm used
doesn't make the definition "the correct one" for division.  In fact, the
Theorem being proven doesn't even mention a division operation:
  If a and m are any integers with m not zero,
  then there are unique integers q and r such that
  a = qm+r with 0 <= r < |m|

Note that there is NO division in this theorem and this is not the only
theorem about unique values of q and r for a pair of arbitrary integers.

Another provable theorem is:
  If a and m are any integers with m not zero,
  then there are unique integers q and r such that
  a = qm+r with |qm| < |a| and 0 <= |r| < |m|

Another provable theorem is:
  If a and m are any integers with m not zero,
  then there are unique integers q and r such that
  a = qm+r with 0 <= ar and 0 <= |r| < |m|

Yet another is:
  If a and m are any integers with m not zero,
  then there are unique integers q and r such that
  a = qm + r and |a| = |q||m| + |r| with 0 <= |r| < |m|

And another:
  If a and m are any integers with m not zero,
  then there are unique integers q and r such that
  a = qm + r and -a = -qm - r with 0 <= |r| < |m|

I particularly like the last theorem because, if we are going
to admit to negative numbers, then I feel we should have
some sort of symmetry between positive and negative
expressions.  The formulation with positive remainders
does not have this symmetry.

These last 4 theorems (I can think up more if you like) can be
proven, all are equivalent and all match the definition of
division in Ada, other languages and most hardware.

PowerPC manuals describe division as
  The quotient is the unique signed integer that satisfies the
  equation  dividend=(quotient*divisor)+r where
  0 <= r < |divisor| if the dividend is non-negative and
  -|divisor| r <= 0 if the dividend is negative.

This is yet another formulation of the quotient definition that
is equivalent to the last 4 theorems above.

The reason this definition is used in most hardware is that there
is an very simple bit-iterative algorithm that produces this
quotient without requiring any intermediate storage. (I remember
analyzing the algorithm on PDP-9 hardware microcode and implementing
it in software on a PDP-11/20 -- I might be able to dig up details
if you are interested).

That iterative algorithm also provides a proof by construction
of the uniqueness of q and hence of r.

Newer hardware most likely produces the result directly without
iteration, but remains consistent with previous definitions for
compatibility.

As Tucker mentioned, this formulation also has the desirable
property that the quotient is independent of where negative
signs are applied:
  -(a/b) = -a/b = a/-b

Without this, -3/2 would be different from -(3/2) which would
be very disturbing to many practitioners.  The "proper" division
you describe does not have this property (call that division by
the name "div").
  -( 3 div 2 ) = -1
  -  3 div 2   = -2

Basically, it is more desirable to have quotient magnitude constancy
than it is to have a positive remainder.

Regards,
Steve
"Then, after a second or so, nothing continued to happen."
Steven Deller        Smooth Sailing LLC
410 757 6924         deller@smsail.com

Re: Integers and Mathematical Correctness

[chris.danx]

I give up!  I shouldn't have mentioned why I was implementing the package
just the difficulty I had, and save all this fussing over division being
"performed" one way or another.  It doesn't matter (anymore).

Can we forget about it now?


Chris

Re: Integers and Mathematical Correctness

[Charles Sampson]

chris.danx <chris.danx@ntlworld.com> wrote:


> According to Euclid, the "division algorithm" (which isn't an algorithm)
> asserts that for a/b
> 
> a = kb + r
> 
> where r >= 0
>       k <- Integers

     Disclaimer: Working from long dormant memory.

     Yes, this is also the definition used when you develop numbers be-
ginning with the Peano postulates (with the correction, noted elsewhere,
of 0 <= r < b).  However, in both cases only non-negative integers are 
being considered.  So the claim "according to Euclid" is incorrect in 
the case of negative integers.

     The mathematical issue is, how do you extend the definition of di-
vision to include negative integers?  The extension I'm familiar with is
the same as the definition used in most programming languages, including
Ada.

     I'm not even sure what the mathematical implications would be if 
you adopted the above "Euclid definition" of a/b if a < 0 and b > 0.  I
suspect that things would become very sloppy along the way.  They cer-
tainly would be in programming.

                                Charlie

Re: Integers and Mathematical Correctness

[Richard Riehle]

Marin David Condic wrote:

> Just because I think the Ada attributes for math (and, of course, other
> stuff) are really cool things to have, I thought I'd mention: ARM Annex K
> wherein you can find S'Ceiling and S'Floor. They apply to floating point
> types, but they might be interesting in this context anyway. I don't know of
> other languages providing so many handy mathematical attributes that let you
> develop code for portability and/or precise behavior. Its one more reason
> why Ada ought to be of interest to those doing mathematical/scientific
> programming.

In other languages, these are provided as functions.   In Ada, they are
attributes that
behave as if they were functions.

Richard Riehle

Re: Integers and Mathematical Correctness

[Marin David Condic]

Just a quick look at my C book here indicates that there are functions
"floor" and "ceil", but I didn't see anything like 'Mantissa and 'Exponent
and so on. Not to mention the fact that they are not exactly connected to
the data type, so there is no real distinction between, say, a Float and a
Long_Float. (I didn't even bother to check for equivalents to things like
'Range, 'First and 'Last - althought there are probably ways of getting
there - just not nearly so slick and convenient.)

I grant you that other languages can and sometimes do provide similar
features. Just not as an inherent part of the language describing the
characteristics of data types, objects, etc. I think attributes are one of
the more handy features of Ada - especially for math oriented computing -
and one that is not always duplicated as thoroughly or as nicely in other
languages.

MDC
--
Marin David Condic
Senior Software Engineer
Pace Micro Technology Americas    www.pacemicro.com
Enabling the digital revolution
e-Mail:    marin.condic@pacemicro.com
Web:      http://www.mcondic.com/


"Richard Riehle" <richard@adaworks.com> wrote in message
news:3BE4232D.6CC9ACA3@adaworks.com...
>
> In other languages, these are provided as functions.   In Ada, they are
> attributes that
> behave as if they were functions.
>

Re: Integers and Mathematical Correctness

[Eric G. Miller]

In <9s68pu$9j5$1@nh.pace.co.uk>, Marin David Condic wrote:

> Just a quick look at my C book here indicates that there are functions
> "floor" and "ceil", but I didn't see anything like 'Mantissa and
> 'Exponent and so on. Not to mention the fact that they are not exactly
> connected to the data type, so there is no real distinction between,
> say, a Float and a Long_Float. (I didn't even bother to check for
> equivalents to things like 'Range, 'First and 'Last - althought there
> are probably ways of getting there - just not nearly so slick and
> convenient.)

#include <float.h>
#include <limits.h>
#include <math.h>


In C: sizeof float <= sizeof double <= sizeof long double

It's all there.  Granted, there are a few things where there's no analog
in C that you'd have to code/check yourself (limited ranges, fixed
precision).

Re: Integers and Mathematical Correctness

[James Rogers]

"Eric G. Miller" wrote:
> 
> #include <float.h>
> #include <limits.h>
> #include <math.h>
> 
> In C: sizeof float <= sizeof double <= sizeof long double
> 
> It's all there.  Granted, there are a few things where there's no analog
> in C that you'd have to code/check yourself (limited ranges, fixed
> precision).

The include files listed above declare constants for various values,
such as FLT_MAX. In one sense they are like 'First and 'Last in 
that they identify value boundaries. Unfortunately, these values in C
are not as useful as their Ada counterparts.

Take the following C snippet:

float f = FLT_MAX;
double d = 2;


f *= d;


What will the result of this be? There is no error issued either at
compile or run time. The value output by printf using a gcc
compiler is "1.#INF".

Note that C does a number of implicit conversions for the above code.
The integer 2 is implicitly converted to a double 2.0.
The calculation "f *= d" implicitly converts f to a double on the
right hand side, performs the calculation, then implicitly
converts the result back to a double.

Note that this error would have been caught by an Ada compiler.
C never notices the problem at all.

Jim Rogers
Colorado Springs, Colorado USA

Re: Integers and Mathematical Correctness

[peter]

In article <3BE766F6.3D014CD8@worldnet.att.net>, James says...
>
 
>Note that this error would have been caught by an Ada compiler.
>C never notices the problem at all.
>
 
Many languages do not notice these things and more, but people still use
them, much more than Ada, and they spend long hours in the 'debugger' trying
to find why the problem does not work (then feel so good about finding the
bug). There is a whole industry out there build around debugging C 
flavoured languages.  

I wonder if the latest C flavoured language 'C#/windows only language',  
from Microsoft fixes some of these problems?

Re: Integers and Mathematical Correctness

[James Rogers]

"peter@nospam" wrote:
> 
> In article <3BE766F6.3D014CD8@worldnet.att.net>, James says...
> >
> 
> >Note that this error would have been caught by an Ada compiler.
> >C never notices the problem at all.
> >
> 
> Many languages do not notice these things and more, but people still use
> them, much more than Ada, and they spend long hours in the 'debugger' trying
> to find why the problem does not work (then feel so good about finding the
> bug). There is a whole industry out there build around debugging C
> flavoured languages.
> 
> I wonder if the latest C flavoured language 'C#/windows only language',
> from Microsoft fixes some of these problems?

I think this was the point Marin was making. C has header files that
define minimum and maximum values for numeric types, but the use
of those header files is optional. Furthermore, those minimum and
maximum values are not part of the type definition. Instead, they
are simply constants defined in several header files.

The C constants provide you the opportunity to develop code to 
check for overflow or underflow conditions. There is no default
check for those conditions.

My cursory look at C# indicates that it also has the implicit
conversions found in C, C++, and Java. Note that Java, for
instance, "solves" the implicit conversion problem by making all
integer forms use unsigned semantics even though all the 
integer types are signed entities. This ensures that the result
of all implicit conversions will be a value within the range of
the type on the left hand side of an assignment. Of course, there
is no assurance that the result will be even remotely correct
in a mathematical sense.

As you say, many people use these languages and spend long hours
debugging their code. My experience is that people use these
languages for two primary reasons: they have been told to and
they do not know any better. Neither of these reasons provide any
technical justification.

Jim Rogers
Colorado Springs, Colorado USA

Re: Integers and Mathematical Correctness

[Marin David Condic]

...And as constants (probably #define...), they can easily be overriden by
the inclusion of another header file or within the file itself. Nothing
stops you from doing: "#define FLT_MAX 1.0" There's nothing to stop you from
accidentally having that appear in some other header file that is brought
into your code invisibly. The sizeof is at least something the compiler is
likely to make sure is correct - but it isn't as useful as knowing what the
'Mantissa or 'Exponent of a float is.

As I said, it isn't as if other languages don't give you *some* of the
things you get from Ada's Attributes in some alternate form. Its just that
the Ada Attributes are generally more useful and more safe - and probably
more breadth of coverage as well. You get a *lot* of power from the
attributes and when I taught Ada to newbies, I always tried to cover them as
much as I could - they are very useful and introduce newbies to The Ada
Way...

MDC
--
Marin David Condic
Senior Software Engineer
Pace Micro Technology Americas    www.pacemicro.com
Enabling the digital revolution
e-Mail:    marin.condic@pacemicro.com
Web:      http://www.mcondic.com/


"James Rogers" <jimmaureenrogers@worldnet.att.net> wrote in message
news:3BE7F836.B9B78AB5@worldnet.att.net...
> "peter@nospam" wrote:
>
> I think this was the point Marin was making. C has header files that
> define minimum and maximum values for numeric types, but the use
> of those header files is optional. Furthermore, those minimum and
> maximum values are not part of the type definition. Instead, they
> are simply constants defined in several header files.
>

Re: Integers and Mathematical Correctness

[Eric G. Miller]

In <3BE766F6.3D014CD8@worldnet.att.net>, James Rogers wrote:

> "Eric G. Miller" wrote:
>> 
>> #include <float.h>
>> #include <limits.h>
>> #include <math.h>
>> 
>> In C: sizeof float <= sizeof double <= sizeof long double
>> 
>> It's all there.  Granted, there are a few things where there's no analog
>> in C that you'd have to code/check yourself (limited ranges, fixed
>> precision).
> 
> The include files listed above declare constants for various values, such
> as FLT_MAX. In one sense they are like 'First and 'Last in that they
> identify value boundaries. Unfortunately, these values in C are not as
> useful as their Ada counterparts.
> 
> Take the following C snippet:
> 
> float f = FLT_MAX;
> double d = 2;
> 
> f *= d;
> 
> What will the result of this be? There is no error issued either at
> compile or run time. The value output by printf using a gcc compiler is
> "1.#INF".

Yes, you have to do sanity checking at run time.  C promotes all sorts
of unsafe things (as you well know).  Funny, I ran the snippet through
lint (default settings), and it didn't see an error either (nor does
-Wall generate any warnings).

[snip]

> Note that this error would have been caught by an Ada compiler. C never
> notices the problem at all.

This is one of the things that drew me Ada.  It's taking some getting used
to, but I think it's worth it.  I was shocked (and somewhat annoyed) by
how much the compiler complained when working on my first program.  The
programs are better because of it, though.

Re: Integers and Mathematical Correctness

[vincent.diemunsch]

Le vendredi 2 novembre 2001 02:40:08 UTC+1, Steven Deller a écrit :
> > >To most this may seem insignificant but I'm more > mathematically minded > and I just found something out. Many programming languages > don't implement division properly!...> Interesting.> > We only learned that in programming languages (and primary school), > technically division is incorrect the other day, and I was a bitty > surprised. I don't really mind that it's "wrong", the > package is just being > written as a little distraction. I may never need it, but > it's there if I> do.> > Anyone wants it, let me know and I'll send it to you when I'm done. >> Bye,> ChrisChris, I too am mathematically minded. And the proclaimed "definition of division" is a proclamation of mathematical charlatans.What I find interesting is the leap to proclaim there is one and only one proper definition of division simply because there a proof of one particular theorem about integers that has one proof (of many possible) using algorithm construction and proving the algorithm by making use of the Well-Ordering Principle.The Well-Ordering Principle applies only for sets of positive integers, so it was important in the algorithm proof to have the remainder (r) limited to be a positive integer. It is additional unfortunate that the algorithmic proof was dubbed "The Division Algorithm". It should have been called "Algorithm For Proving Uniqueness of Integers Selected with Certain Extended-Ring Properties" If I remember correctly the existence of both * and + would make this a Ring theorem. Negative numbers require an inverse "existence" postulate that I don't believe Rings have. Does that make this a Field (I'm trying to recall lessons learned 40 years ago :-) ).The presence of that theorem and the "deemed" name of the algorithm used doesn't make the definition "the correct one" for division. In fact, the Theorem being proven doesn't even mention a division operation: If a and m are any integers with m not zero, then there are unique integers q and r such that a = qm+r with 0 <= r < |m|Note that there is NO division in this theorem and this is not the only theorem about unique values of q and r for a pair of arbitrary integers.Another provable theorem is:If a and m are any integers with m not zero, then there are unique integers q and r such that a = qm+r with |qm| < |a| and 0 <= |r| < |m|Another provable theorem is:If a and m are any integers with m not zero, then there are unique integers q and r such that a = qm+r with 0 <= ar and 0 <= |r| < |m|Yet another is: If a and m are any integers with m not zero, then there are unique integers q and r such that a = qm + r and |a| = |q||m| + |r| with 0 <= |r| < |m|And another:If a and m are any integers with m not zero, then there are unique integers q and r such that a = qm + r and -a = -qm - r with 0 <= |r| < |m|I particularly like the last theorem because, if we are going to admit to negative numbers, then I feel we should have some sort of symmetry between positive and negative expressions. The formulation with positive remainders does not have this symmetry.These last 4 theorems (I can think up more if you like) can be proven, all are equivalent and all match the definition of division in Ada, other languages and most hardware.PowerPC manuals describe division as The quotient is the unique signed integer that satisfies the equation dividend=(quotient*divisor)+r where 0 <= r < |divisor| if the dividend is non-negative and -|divisor| r <= 0 if the dividend is negative.This is yet another formulation of the quotient definition that is equivalent to the last 4 theorems above.The reason this definition is used in most hardware is that there is an very simple bit-iterative algorithm that produces this quotient without requiring any intermediate storage. (I remember analyzing the algorithm on PDP-9 hardware microcode and implementing it in software on a PDP-11/20 -- I might be able to dig up details if you are interested).That iterative algorithm also provides a proof by construction of the uniqueness of q and hence of r.Newer hardware most likely produces the result directly without iteration, but remains consistent with previous definitions for compatibility.As Tucker mentioned, this formulation also has the desirable property that the quotient is independent of where negative signs are applied:-(a/b) = -a/b = a/-bWithout this, -3/2 would be different from -(3/2) which would be very disturbing to many practitioners. The "proper" division you describe does not have this property (call that division by the name "div").-( 3 div 2 ) = -1- 3 div 2 = -2Basically, it is more desirable to have quotient magnitude constancy than it is to have a positive remainder.Regards,Steve "Then, after a second or so, nothing continued to happen." Steven Deller Smooth Sailing LLC410 757 6924 deller@smsail.com



I thing there are two problems with the current Ada implementation :

1. It is not consistent with modular types :
   
   A = (A/B)*B + (A rem B) is not true for modular types. So modular types
   should not have a "rem" operator.

   Only A = (A div B)*B + (A mod B) is consistent. So we should have a "div"
   operator.

2. The very existence of the 
   
   function "/" (Left, Right : Integer) return Integer; 

prevents the implementation and the use of Rational types in Ada, which are otherwise very simple to implement using a record type, just like complex numbers. Since ARM §4.6 defines that 

   Integer(-0.4) = 0;

which means that rounding is toward zero, I think that we should write 
    
   Integer_Type ( A / B ) 

instead of A / B to express integer division of A, B : Integer_Type.
Note that we still have for signed integers :
   
   A = Integer(A/B)*B + (A rem B)
   Integer( -A / B) = Integer (A / -B) = - Integer (A/B) 
   

To summary, we should correct Ada to have :
   A "div" operator
   A Rational type, defined like complex types that are relative to
   a given floating point type, based on an integer type T, and assert 
   that T ( T1 / T2) is of type T and rounds towards zero.
   Obviously, the compiler would automaticaly create the rational type
   whenever a new integer type is created. There would be no need to use
   explicitly a generic unit.


Vincent

Re: Integers and Mathematical Correctness

[Niklas Holsti]

On 14-09-26 12:07 , vincent.diemunsch@gmail.com wrote:
> Le vendredi 2 novembre 2001 02:40:08 UTC+1, Steven Deller a écrit :

[ a mess of unformatted text ]

> I thing there are two problems with the current Ada implementation :

...

> 2. The very existence of the 
>    
>    function "/" (Left, Right : Integer) return Integer; 
> 
> prevents the implementation and the use of Rational types in Ada,

False. Ada can overload operators on the result type, so you can very
well add

   function "/" (Left, Right : Integer) return Rational;

and have both"/" visible and used with in-fix notation.

> which are otherwise very simple to implement using a record type,
> just like complex numbers.

I beg to disagree. Rational numbers with Integer numerator and
denominator are not very useful, because after a relatively small number
of arithmetic operations, the numerator and denominator often become
very large and overflow the Integer range.

IMO rational numbers are useful only when the numerator and denominator
are "bignums", effectively unbounded integer types.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .

Re: Integers and Mathematical Correctness

[Adam Beneschan]

On Friday, September 26, 2014 2:07:32 AM UTC-7, vincent....@gmail.com wrote:

> 2. The very existence of the 
> 
>    function "/" (Left, Right : Integer) return Integer; 
> 
> prevents the implementation and the use of Rational types in Ada, which are otherwise very simple to implement using a record type, just like complex numbers. 

How does the existence of this operator prevent it?

I just tried this:

package Rational_Numbers is
    type Rational is private;
    function "/" (Numerator, Denominator : Integer) return Rational;
private
    ...
end Rational_Numbers;

with Rational_Numbers;
procedure Test is
    use type Rational_Numbers.Rational;
    R : Rational_Numbers.Rational;
begin
    R := 5 / 2;
end Test;

Which compiles fine and does what you'd expect.  If there is some other thing that you'd like to do with rational numbers that you can't because of the predefined "/", please elaborate.

                               -- Adam

Re: Integers and Mathematical Correctness

[Adam Beneschan]

On Friday, September 26, 2014 2:07:32 AM UTC-7, vincent....@gmail.com wrote:

> 1. It is not consistent with modular types :
> 
>    A = (A/B)*B + (A rem B) is not true for modular types. So modular types
>    should not have a "rem" operator.

Actually, I question whether you're correct here.  Can you provide an example of a modular type, and values A and B of that type (B /= 0), such that

   (A/B)*B + (A rem B) /= A ?

(using the Ada definitions of the operators)?  I may be missing something, but I don't think it's possible.

                             -- Adam

Re: Integers and Mathematical Correctness

[AdaMagica]

On Friday, September 26, 2014 6:38:10 PM UTC+2, Niklas Holsti wrote:

> False. Ada can overload operators on the result type, so you can very 
> well add
>
>    function "/" (Left, Right : Integer) return Rational;
>
> and have both"/" visible and used with in-fix notation.

Nah, it's not that easy. The reason is that Integer is defined in Standard, which always has precedence for any use-clause.

You need a separate integer type

  type Whole is range ...
  function "/" (Left, Right: Whole) return Rational;

There is a complete implementation in
http://www.christ-usch-grein.homepage.t-online.de/Ada/Dimension/SI.html
with Text_IO, Image and Value; appropriate test units exist also.

GNAT had much fun with overload resolution - it took very long until it could deal with my rational numbers.

Re: Integers and Mathematical Correctness

[Adam Beneschan]

On Friday, September 26, 2014 9:59:00 AM UTC-7, AdaMagica wrote:
> On Friday, September 26, 2014 6:38:10 PM UTC+2, Niklas Holsti wrote:
 
> > False. Ada can overload operators on the result type, so you can very 
> > well add
> >
> >    function "/" (Left, Right : Integer) return Rational;
> 
> > and have both"/" visible and used with in-fix notation.
>
> Nah, it's not that easy. The reason is that Integer is defined in Standard, which always has precedence for any use-clause.

The precedence of use clauses is irrelevant.  This (and other rules about visibility and hiding) are used when there are two homographs and the compiler needs to decide which one is meant.  Thus, if you have a type "Integer" defined in Standard, and a type "Integer" defined in some USE'd package, I think the one in Standard would hide the other one, as you say.

However, functions are homographs only if they have the same name, same parameter types, and same return type.  Thus, the function

   function "/" (Left, Right : Integer) return Integer;

defined in Standard cannot hide the function

   function "/" (Left, Right : Integer) return Rational;

defined somewhere else.  The compiler uses the overloading rules, not the USE rules or any such visibility rules, to determine which one is meant.  So if use use / in a context where the result is Rational, it will work fine--the definition in Standard cannot hide it.  If you use it in a context where the compiler can't tell which one is meant, the expression is ambiguous--the rules about USE clauses and such will not help to make it unambiguous.
 
 
> You need a separate integer type
> 
>   type Whole is range ...
>   function "/" (Left, Right: Whole) return Rational;

No, this is not necessary.  Unless the compiler is faulty.

                             -- Adam

Re: Integers and Mathematical Correctness

[AdaMagica]

Adam,
Na, you forget
A: Rational := 1/3+1/4;
This will be 0 for your function.

Re: Integers and Mathematical Correctness

[AdaMagica]

Just to elaborate a bit:

I guess a rational number package is not complete if there is no possibility to add a whole and a rational number; in general, mixing of whole and rational numbers in all operators should be possible.

For this, you definitely need an integer type different from Standard.Integer.

And you'll be astonished how many functions this will at the end. (Don't forget relational operators and equality (1 = 2/2).)

Christoph

Re: Integers and Mathematical Correctness

[gautier_niouzes]

Le vendredi 26 septembre 2014 18:38:10 UTC+2, Niklas Holsti a écrit :

> I beg to disagree. Rational numbers with Integer numerator and
> denominator are not very useful, because after a relatively small number
> of arithmetic operations, the numerator and denominator often become
> very large and overflow the Integer range.

There is always the possibility of reducing the fraction - see below.

> IMO rational numbers are useful only when the numerator and denominator
> are "bignums", effectively unbounded integer types.

Bignums are probably more useful but prehaps slower. Anyway there is an universal solution with generics, where you can choose what you want.
For instance if you really want to use the type Integer, that's easy:

package Rationals is new Frac_Euclid(Integer, 0,1, "-","+","-","*","/");

The package Frac_Euclid is defned below (works also with non-numerci types!):

generic                              -- to provide:
          type ring_elt is private;                  -- ring element type
          zero, one: ring_elt;                       -- 0 and 1 elements

          with function "-" (a:ring_elt) return ring_elt;    -- unary oper.
          with function "+" (a,b:ring_elt) return ring_elt;  -- binary oper.
          with function "-" (a,b:ring_elt) return ring_elt;
          with function "*" (a,b:ring_elt) return ring_elt;
          with function "/" (a,b:ring_elt) return ring_elt;
                        -- returns the quotient:  a= b*q + r
                        -- q:quotient, r:rest

package Frac_euclid is
  type frac_elt is record a,b:ring_elt; end record;     -- define fraction

  frac_0: constant frac_elt:= (zero,one);
  frac_1: constant frac_elt:= (one,one);

  function Reduction(f: frac_elt) return frac_elt;
  pragma Inline(Reduction);

  function "+" (f: frac_elt) return frac_elt;                 -- unary oper.
  function "-" (f: frac_elt) return frac_elt;

  function "+" (f1,f2: frac_elt) return frac_elt;             -- binary oper.
  function "+" (a: ring_elt; f: frac_elt) return frac_elt;
  function "+" (f: frac_elt; a: ring_elt) return frac_elt;
  function "-" (f1,f2: frac_elt) return frac_elt;
  function "-" (a: ring_elt; f: frac_elt) return frac_elt;
  function "-" (f: frac_elt; a: ring_elt) return frac_elt;
  function "*" (f1,f2: frac_elt) return frac_elt;
  function "*" (a: ring_elt; f: frac_elt) return frac_elt;
  function "*" (f: frac_elt; a: ring_elt) return frac_elt;
  function "/" (f1,f2: frac_elt) return frac_elt;
  function "/" (a: ring_elt; f: frac_elt) return frac_elt;
  function "/" (f: frac_elt; a: ring_elt) return frac_elt;
  function "/" (a,b: ring_elt) return frac_elt;

  function Eq(f1,f2: frac_elt) return Boolean;               -- returns f1=f2

  auto_reduce: Boolean:= True;
  reduce_in_add: Boolean:= True;

  Zero_denominator:          exception;
  Division_by_null_fraction: exception;

end Frac_Euclid;

The implementation (as well as a bigint implementation) is in MathPaqs:
http://sf.net/projects/mathpaqs/

Subdirectory : algebra and multi.

Enjoy
_________________________ 
Gautier's Ada programming 
http://www.openhub.net/accounts/gautier_bd

Re: Integers and Mathematical Correctness

[vincent.diemunsch]

> > 1. It is not consistent with modular types :
> > 
> 
> >    A = (A/B)*B + (A rem B) is not true for modular types. So modular types
> 
> >    should not have a "rem" operator.
> 
> 
> 
> Actually, I question whether you're correct here.  Can you provide an example of a modular type, and values A and B of that type (B /= 0), such that
> 
>    (A/B)*B + (A rem B) /= A ?
> 

> (using the Ada definitions of the operators)?  I may be missing something, but I don't think it's possible.
> 
> 
>                              -- Adam

Hi Adam,

I tried to create a small example to illustrate. Let's try, and please tell me if I am wrong. 

First suppose that you have 4 processors on which you wish to dispatch some piece of work. Imagine that you have 42 simple computations. Each processor will need to process 10 computations and it remains 2 computations that we give to processor n°4. We do have :

     42 = (42 /  4) *4 + (42 rem 4) = 10*4 + 2;

Now we will use a ring buffer to store our computations, instead of a simple array from 1 ... 42. So the buffer has 1024 entries. The 42 computations are located from location n° 1023 - 29 to location n° 12.
We still have 42 computations :  
    
     Last - First + 1 =  11 - (1023 -29) + 1 = -982 == 42 mod 1024.
    
I see that Ada / Gnat correct the modular value to put in 0 .. 1023 before applying the divide operators
/ and rem. So we get the correct result with modular types :  (-982) / 4 = 10 and (-982) rem 4 = 2. 
And finally : ((-982) / 4 ) * 4 + ((-982) rem 4) = 42 == -982 mod 1024.  But clearly 42 /= -982 from the point of view of integers, even if in Ada (-982) = 42 would return true for modular types defined as mod 1024.

So you are right : that means that

      A = (A/B)*B + (A rem B)

holds providing that we understand it the Ada way, which is something like :  

A mod 1024 == Round((A mod 1024) / (B mod 1024))* (B mod 1024) + ((A mod 1024) rem (B mod 1024))

This implies that :
     (-982) / 4 = 10
that I found really ugly and with very little mathematical sense.

And the famous  -A / B  = A / -B = - (A/B)  which is given as the main argument to use "/" instead of "div" is completely false for modular integers in Ada...
   since for exemple -982 /  4 =    42 / 4      = 10
                                982 / -4 = 982 / 1020 = 0
                            -( 982 /  4) = -245 = 779

Now, on the other hand, 

      A = (A div B)*B + A mod B,  

is always true : 
a) for integers : -982 = -246*4 + 2, but I recognize that A div B = -982 div 4 = -246 is of no use for my little problem !!
b) for modular integers (mod 1024), if you set that (-982) div 4 = 10, and (-982) = 42 ! I am not shocked that (-982) div 4 = 10 neither than 982 div (-4) = 0, because the "div" operator is specific and there is no possible confusion with rational division.

So finally I change my mind, the problem is not the "rem" operator for modular type but clearly the use of "/" instead of "div" for modular types. And for signed integers I still would prefer to be able to write Integer (A/B) than simply A/B for the reason that it is simpler in the context of rational types (think of 4 + 1/3 : is it 5/3 or 4 ?).

Re: Integers and Mathematical Correctness

[Niklas Holsti]

On 14-09-27 12:01 , AdaMagica wrote:
> Adam,
> Na, you forget
> A: Rational := 1/3+1/4;
> This will be 0 for your function.

That seems not to be the case. With the definition

   type Rational is record
      Numerator, Denominator : Integer;
   end record;

and the obvious definitions of "+", "/", and Image for Rational, the
program fragment

   R : Rational := 1/4 + 3/2;
begin
   Put_Line (Image (R));

results in the output

 7 / 2

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .

Re: Integers and Mathematical Correctness

[Jeffrey Carter]

On 09/27/2014 09:32 AM, Niklas Holsti wrote:
> 
>    R : Rational := 1/4 + 3/2;
> begin
>    Put_Line (Image (R));
> 
> results in the output
> 
>  7 / 2

Too bad, since the correct answer is 7/4.

-- 
Jeff Carter
"C++: The power, elegance and simplicity of a hand grenade."
Ole-Hjalmar Kristensen
90

Re: Integers and Mathematical Correctness

[Niklas Holsti]

On 14-09-27 19:49 , Jeffrey Carter wrote:
> On 09/27/2014 09:32 AM, Niklas Holsti wrote:
>>
>>    R : Rational := 1/4 + 3/2;
>> begin
>>    Put_Line (Image (R));
>>
>> results in the output
>>
>>  7 / 2
> 
> Too bad, since the correct answer is 7/4.

My program is buggy, my face is red... (error in reduction of denominator).

But at least the answer was not zero.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .

Re: Integers and Mathematical Correctness

[Adam Beneschan]

On Saturday, September 27, 2014 9:32:52 AM UTC-7, Niklas Holsti wrote:
> On 14-09-27 12:01 , AdaMagica wrote:
> 
> > Adam,
> > Na, you forget
> > A: Rational := 1/3+1/4;
> > This will be 0 for your function.
> 
> That seems not to be the case. With the definition
> 
>    type Rational is record
>       Numerator, Denominator : Integer;
>    end record;
> 
> and the obvious definitions of "+", "/", and Image for Rational, the
> program fragment
> 
>    R : Rational := 1/4 + 3/2;
> begin
>    Put_Line (Image (R));
> 
> results in the output
> 
>  7 / 2

Well, it should be 7/4 as Jeff pointed out, but yes, that's what I'd expect as long as there are no versions of "+" that take one Integer and one Rational parameter and return Rational.  If there is a visible "+" like that, the program would be rejected as ambiguous.  But 0 (or 0/1 or any Rational number representing 0) is not a possible result.

Christoph did point out that having those versions of "+" is important.  Defining another integer type to use as parameters to those functions is one way of eliminating ambiguity--I assume that this type would use "is abstract" to nullify all of the standard operator declarations that this type definition would create.  

    function "+" (Left, Right : Whole_Number) return Whole_Number is abstract;
    etc.

But it's not the only way; you can manage without defining a new integer type.  If 

    R : Rational := 1/4 + 3/2

is ambiguous, you can disambiguate like this:

    R : Rational := Rational'(1/4) + Rational'(3/2);

which forces the compiler to use the versions of "/" that have a Rational result, and ignore the declarations in Standard that return Integer.  I think there's a tradeoff.  Having to add this in some places could be inconvenient.  But the solution of defining another integer type is probably going to require some type conversions to and from that integer type (since you would not be able to use other arithmetic operations on that type), which could also be inconvenient.  I don't know which is the better solution.

Finally, I want to reiterate the point I made earlier: when it comes to overload resolution, the *location* where the operators are declared (in a USE'd package, in Standard, in the local scope or an enclosing scope or a parent package) is not relevant.  It's relevant when you have two or more declarations that have the same name, AND the same parameters AND the same result type.  When that happens, the location is used to determine which declaration takes precedence over all other declarations THAT HAVE THE SAME PARAMETER AND RESULT TYPES.  Once that's done, there is at most one of each operator with the same parameter/result types, but there can still be more than one that have different parameter and/or result types.  Deciding which of those is used is called overload resolution or name resolution, and the locations where the operators are declared has no effect on overload resolution.

                                -- Adam

Re: Integers and Mathematical Correctness

[Adam Beneschan]

On Saturday, September 27, 2014 11:54:33 AM UTC-7, Adam Beneschan wrote:

> Well, it should be 7/4 as Jeff pointed out, but yes, that's what I'd expect as long as there are no versions of "+" that take one Integer and one Rational parameter and return Rational.  If there is a visible "+" like that, the program would be rejected as ambiguous.  But 0 (or 0/1 or any Rational number representing 0) is not a possible result.

I suppose I should clarify: 0 is not a possible result if we assume that the "/" and "+" operations in Rational are implemented correctly ;) ;) ;)

                             -- Adam

Re: Integers and Mathematical Correctness

[AdaMagica]

On Saturday, September 27, 2014 8:20:32 PM UTC+2, Adam Beneschan wrote:
> It may choose it for *one* of the operands, depending on whether these functions are directly visible:
>
>     function "+" (Left : Rational; Right : Integer) return Rational;
>     function "+" (Left : Integer; Right : Rational) return Rational;
>
> Actually, if either of those is visible, then there is more than one way to
> choose the meanings of "+" and "/" to form an acceptable interpretation.
> Because of this, the expression would be treated as ambiguous, and the
> compiler would reject it.

Exactly that's my point, the compiler will reject it. (You're right, the result is not 0, the compiler rejects the code. My error!)

With Integer, there's always visible with preference

function "/" (Left, Right: Integer) return Integer;

which will ruin 1/2 + 2/3, because your two functions above are there. Thus these interpretations are possible, which the compiler cannot resolve:

Rational + Rational = Rational
Integer  + Rational = Rational
Rational + Integer  = Rational

So you have to remove the integer division, which is only possible for a new type Whole:

overriding function "/" (Left, Right: Whole) return Whole is abstract;

Now everything can work. There is of course no

function "+" (Left, Right: Whole) return Rational;

So in short: The crux is not rational numbers combined with themselves, but mixed arithmetics (i.e. rational and whole).

So I still do not believe that you can do mixed arithmetics with rationals constructed from Integer:

  function "+" (Left: Rational; Right: Integer ) return Rational;
  function "+" (Left: Integer ; Right: Rational) return Rational;
  function "+" (Left: Rational; Right: Rational) return Rational;
  "/" (Left, Right: Integer) return Rational;  -- constructor
  "/" (Left, Right: Integer) return Integer;   -- from Standard

You cannot hide the last function!

[OK, you can make 1/2 + 1/3 work by qualifying the functions, but that's not the point (and extremely ugly.]

Re: Integers and Mathematical Correctness

[Dmitry A. Kazakov]

On Sat, 27 Sep 2014 14:13:39 -0700 (PDT), Adam Beneschan wrote:

> Therefore, any
> operation that returns a modular type will automatically convert a
> negative value to the value modulo the modulus.

No. This is a description of some possible implementation of the operation
based on an integer type. This is not the only one implementation, e.g.
there exist machine instructions directly implementing modular operations
for moduli 2**16, 2**32 ...

> If one remembers that there are no negative values of a modular type,

Technically speaking -A is not a negative value it is an [additive] inverse
element of A. The meaning is

   Y is an inverse of X iff

    X + Y = 0  [mod K] (in our case)

where 0 is the zero element.

And yes,

   982 + 42 = 0 [mod 1024]

> then any angst over why (-A)/B might be different from -(A/B) or A/(-B)
> seems more like an academic issue than a practical one. 

Why should they be same?

I also do not understand how all this might be related to rational numbers,
which are neither integer nor modular. BTW, Ada's fixed-point numbers are
rational, what is wrong with them?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Integers and Mathematical Correctness

[Adam Beneschan]

On Sunday, September 28, 2014 12:47:18 AM UTC-7, Dmitry A. Kazakov wrote:

> > Therefore, any 
> > operation that returns a modular type will automatically convert a
> > negative value to the value modulo the modulus.
> 
> No. This is a description of some possible implementation of the operation
> based on an integer type. This is not the only one implementation, e.g.
> there exist machine instructions directly implementing modular operations
> for moduli 2**16, 2**32 ...

I'm not sure we're on the same page... I'm talking about modular types in Ada, and my statement is taken directly from RM 3.5.4(19).  (Of course, it's always possible for a clever optimizing compiler to generate code that skips a step.)


> I also do not understand how all this might be related to rational numbers,
> which are neither integer nor modular. 

There's no relation.  The post from Vincent that started this said "I thing [sic] there are two problems with the current Ada implementation :", and then he described two separate problems, one dealing with modular types and one dealing with rational numbers.  (It's just a coincidence that both involved division, I think.)

                               -- Adam

Re: Integers and Mathematical Correctness

[Dmitry A. Kazakov]

On Mon, 29 Sep 2014 07:58:56 -0700 (PDT), Adam Beneschan wrote:

> On Sunday, September 28, 2014 12:47:18 AM UTC-7, Dmitry A. Kazakov wrote:
> 
>>> Therefore, any 
>>> operation that returns a modular type will automatically convert a
>>> negative value to the value modulo the modulus.
>> 
>> No. This is a description of some possible implementation of the operation
>> based on an integer type. This is not the only one implementation, e.g.
>> there exist machine instructions directly implementing modular operations
>> for moduli 2**16, 2**32 ...
> 
> I'm not sure we're on the same page... I'm talking about modular types in
> Ada, and my statement is taken directly from RM 3.5.4(19).

Should probably be rewritten, because it looks in contradiction with
4.5(10) that claims:

"The predefined operations on integer types either yield the mathematically
correct result or raise the exception Constraint_Error."

The mathematically correct result of any modulo K arithmetic operation is
an element of the ring {0, 1, ..., K-1}

   10 + 10 = 20  is mathematically incorrect for modulo 16

The mathematically correct one is:

   10 + 10 = 4

Though, of course

   10 + 10 ≡ 4  (mod 16)
   10 + 10 ≡ 20 (mod 16)
   10 + 10 ≡ 36 (mod 16)
   10 + 10 ≡ 52 (mod 16)
   ...

[ Elements of the ring can be considered ether numbers

   { 0, 1, ..., K-1 }

or sets of equivalence

  {{ 0, K, 2K, ... }, { 1, 1+K, 1+2K, ...}, ... , { K-1, 2K-1, 3K-1, ...}}

In ether case there is only one correct result, which cannot be "outside
the base range." ]

> (Of course, it's always possible for a clever optimizing compiler to
> generate code that skips a step.)

I bet that is the case for Unsigned_64, Unsigned_32 etc.

>> I also do not understand how all this might be related to rational numbers,
>> which are neither integer nor modular. 
> 
> There's no relation.

OK

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Integers and Mathematical Correctness

[vincent.diemunsch]

> There's no relation.  The post from Vincent that started this said "I thing [sic] there are two problems with the current Ada implementation :", and then he described two separate problems, one dealing with modular types and one dealing with rational numbers.  (It's just a coincidence that both involved division, I think.)
> 
> 
> 
>                                -- Adam

No, there is no coincidence : I am disappointed that Ada uses "/" as an integer division operator. 

I understand the reasons that dated back from Ada 83 : direct hardware instruction mapping, difference with the "mathematical" "div" operator on negative numbers and the relation -5 / 4 = 5 / -4. 

(Even if you call me a charlatan, I still maintain that Euclid was right : imagine that 3 friends need to pay a bill (which means that they have a negative amount of money) the only way to share is rounding toward -Infinity  :-) )).

But now that we have operator overloading and that I use it for rationals or symbolic expression, I am bothered that an integer division has exactly the syntax I would like to use for a rational number...

And this gives rise to a deeper question : should the revision of the Ada langage be used to improve the langage (make it better) sometimes with the same core functionality, or should it be intended only for adding new features keeping backward compatibility ? The response is not obvious for me, since the only motivation I have to use Ada is that it is a "better" (cleaner, easier to use, to read, to understand) langage than C.

Kind regards,

Vincent

Re: Integers and Mathematical Correctness

[G.B.]

On 01.10.14 21:48, vincent.diemunsch@gmail.com wrote:
> But now that we have operator overloading and that I use it for rationals or symbolic expression, I am bothered that an integer division has exactly the syntax I would like to use for a rational number...

A story about John von Neumann has him say something like
"what a waste of valuable programmer time", when approached by
someone enthusiastically demonstrating early Fortran syntax,
assuming that source texts looking "like math" rather than "like
assembler" would help.

In fact, I think that, provided that one is using languages
not specifically made for mathematics, distracting peoples'
attention from computing devices by way of "math like"
syntax is a terrible mistake.  It is the prime invitation
to not think about the thing you are programming, and then
make corresponding mistakes, led by the wrong assumptions.

Computer formalisms deserve their own syntax. It does not
make them non-mathematical. Operators that are not operating
like the ones you learned at school should never look like
those.  Cf. C's INT_MAX + 1 ... or feed the following program
to GNAT's default compilation to watch "+" in action:

procedure Plus is
    X : Integer := Integer'Last;
begin
    for Y in Integer loop
       X := X + 1;
    end loop;
end Plus;