RE: Integers and Mathematical Correctness

["Steven Deller" <deller@smsail.com>]

> >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