From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.66.196.193 with SMTP id io1mr15053571pac.28.1411722451178; Fri, 26 Sep 2014 02:07:31 -0700 (PDT) X-Received: by 10.140.96.244 with SMTP id k107mr235qge.39.1411722451074; Fri, 26 Sep 2014 02:07:31 -0700 (PDT) Path: border2.nntp.dca1.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!h15no7087250igd.0!news-out.google.com!i10ni38qaf.0!nntp.google.com!k15no16269qaq.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 26 Sep 2014 02:07:30 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=185.30.133.97; posting-account=hya6vwoAAADTA0O27Aq3u6Su3lQKpSMz NNTP-Posting-Host: 185.30.133.97 References: User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: Integers and Mathematical Correctness From: vincent.diemunsch@gmail.com Injection-Date: Fri, 26 Sep 2014 09:07:31 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: number.nntp.dca.giganews.com comp.lang.ada:189164 Date: 2014-09-26T02:07:30-07:00 List-Id: Le vendredi 2 novembre 2001 02:40:08 UTC+1, Steven Deller a =E9crit=A0: > > >To most this may seem insignificant but I'm more > mathematically mind= ed > and I just found something out. Many programming languages > don't imp= lement division properly!...> Interesting.> > We only learned that in progr= amming 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 kn= ow and I'll send it to you when I'm done. >> Bye,> ChrisChris, I too am mat= hematically minded. And the proclaimed "definition of division" is a procla= mation of mathematical charlatans.What I find interesting is the leap to pr= oclaim there is one and only one proper definition of division simply becau= se there a proof of one particular theorem about integers that has one proo= f (of many possible) using algorithm construction and proving the algorithm= by making use of the Well-Ordering Principle.The Well-Ordering Principle a= pplies only for sets of positive integers, so it was important in the algor= ithm proof to have the remainder (r) limited to be a positive integer. It i= s additional unfortunate that the algorithmic proof was dubbed "The Divisio= n Algorithm". It should have been called "Algorithm For Proving Uniqueness = of Integers Selected with Certain Extended-Ring Properties" If I remember c= orrectly the existence of both * and + would make this a Ring theorem. Nega= tive 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 learn= ed 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 divis= ion. In fact, the Theorem being proven doesn't even mention a division oper= ation: If a and m are any integers with m not zero, then there are unique i= ntegers q and r such that a =3D qm+r with 0 <=3D r < |m|Note that there is = NO division in this theorem and this is not the only theorem about unique v= alues 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 integ= ers q and r such that a =3D qm+r with |qm| < |a| and 0 <=3D |r| < |m|Anothe= r provable theorem is:If a and m are any integers with m not zero, then the= re are unique integers q and r such that a =3D qm+r with 0 <=3D ar and 0 <= =3D |r| < |m|Yet another is: If a and m are any integers with m not zero, t= hen there are unique integers q and r such that a =3D qm + r and |a| =3D |q= ||m| + |r| with 0 <=3D |r| < |m|And another:If a and m are any integers wit= h m not zero, then there are unique integers q and r such that a =3D qm + r= and -a =3D -qm - r with 0 <=3D |r| < |m|I particularly like the last theor= em because, if we are going to admit to negative numbers, then I feel we sh= ould 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 eq= uivalent and all match the definition of division in Ada, other languages a= nd most hardware.PowerPC manuals describe division as The quotient is the u= nique signed integer that satisfies the equation dividend=3D(quotient*divis= or)+r where 0 <=3D r < |divisor| if the dividend is non-negative and -|divi= sor| r <=3D 0 if the dividend is negative.This is yet another formulation o= f the quotient definition that is equivalent to the last 4 theorems above.T= he reason this definition is used in most hardware is that there is an very= simple bit-iterative algorithm that produces this quotient without requiri= ng any intermediate storage. (I remember analyzing the algorithm on PDP-9 h= ardware 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 Tuck= er mentioned, this formulation also has the desirable property that the quo= tient is independent of where negative signs are applied:-(a/b) =3D -a/b = =3D a/-bWithout this, -3/2 would be different from -(3/2) which would be ve= ry disturbing to many practitioners. The "proper" division you describe doe= s not have this property (call that division by the name "div").-( 3 div 2 = ) =3D -1- 3 div 2 =3D -2Basically, it is more desirable to have quotient ma= gnitude constancy than it is to have a positive remainder.Regards,Steve "Th= en, after a second or so, nothing continued to happen." Steven Deller Smoot= h 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 : =20 A =3D (A/B)*B + (A rem B) is not true for modular types. So modular type= s should not have a "rem" operator. Only A =3D (A div B)*B + (A mod B) is consistent. So we should have a "d= iv" operator. 2. The very existence of the=20 =20 function "/" (Left, Right : Integer) return Integer;=20 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 =A74.6 defines that=20 Integer(-0.4) =3D 0; which means that rounding is toward zero, I think that we should write=20 =20 Integer_Type ( A / B )=20 instead of A / B to express integer division of A, B : Integer_Type. Note that we still have for signed integers : =20 A =3D Integer(A/B)*B + (A rem B) Integer( -A / B) =3D Integer (A / -B) =3D - Integer (A/B)=20 =20 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=20 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