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=-2.9 required=5.0 tests=BAYES_00,MAILING_LIST_MULTI autolearn=unavailable autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,b61052ba3fdc8c26 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-11-01 17:40:08 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!newsfeeds.belnet.be!news.belnet.be!fr.usenet-edu.net!usenet-edu.net!enst!enst.fr!not-for-mail From: "Steven Deller" Newsgroups: comp.lang.ada Subject: RE: Integers and Mathematical Correctness Date: Thu, 1 Nov 2001 20:37:03 -0500 Organization: ENST, France Sender: comp.lang.ada-admin@ada.eu.org Message-ID: Reply-To: comp.lang.ada@ada.eu.org NNTP-Posting-Host: marvin.enst.fr Mime-Version: 1.0 Content-Type: text/plain; charset="Windows-1252" Content-Transfer-Encoding: 7bit X-Trace: avanie.enst.fr 1004665206 9212 137.194.161.2 (2 Nov 2001 01:40:06 GMT) X-Complaints-To: usenet@enst.fr NNTP-Posting-Date: Fri, 2 Nov 2001 01:40:06 +0000 (UTC) To: Return-Path: X-Priority: 3 (Normal) X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook CWS, Build 9.0.2416 (9.0.2911.0) Importance: Normal In-Reply-To: X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4807.1700 Errors-To: comp.lang.ada-admin@ada.eu.org X-BeenThere: comp.lang.ada@ada.eu.org X-Mailman-Version: 2.0.6 Precedence: bulk X-Reply-To: List-Help: List-Post: List-Subscribe: , List-Id: comp.lang.ada mail<->news gateway List-Unsubscribe: , List-Archive: Errors-To: comp.lang.ada-admin@ada.eu.org X-BeenThere: comp.lang.ada@ada.eu.org Xref: archiver1.google.com comp.lang.ada:15604 Date: 2001-11-01T20:37:03-05:00 > >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