Re: Integers and Mathematical Correctness

[vincent.diemunsch@gmail.com]

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