Integer division and modulus/remainder in Mizar

[John Harrison-7]

I'm curious how Mizar defines division and modulus of integers where
one or both arguments are negative.

This is a well-known area where programming languages disagree or are
undefined, so I'm doing a little survey of some of the world's leading
theorem provers to see if there is a consensus there.

John.

[Artur Kornilowicz]

On Tue, 5 Aug 2008, John Harrison wrote:

>
> I'm curious how Mizar defines division and modulus of integers where
> one or both arguments are negative.
>
> This is a well-known area where programming languages disagree or are
> undefined, so I'm doing a little survey of some of the world's leading
> theorem provers to see if there is a consensus there.
>
> John.

Dear John,

in Mizar Mathematical Library division and modulus of integers are defined
as follows:

definition
   let i1,i2 be Integer;
   func i1 div i2 -> Integer equals
:: INT_1:def 7
   [\ i1 / i2 /];
end;

that is 'div' is the floor of frac and then

definition
   let i1,i2 be Integer;
   func i1 mod i2 -> Integer equals
:: INT_1:def 8
   i1 - (i1 div i2) * i2 if i2 <> 0
   otherwise 0;
end;

All details can be found at

http://merak.pb.bialystok.pl/mml/current/int_1.html

Best regards
Artur

[Freek Wiedijk]

Artur:

>in Mizar Mathematical Library division and modulus of
>integers are defined as follows:
>
>definition
>  let i1,i2 be Integer;
>  func i1 div i2 -> Integer equals
>:: INT_1:def 7
>  [\ i1 / i2 /];
>end;
>
>that is 'div' is the floor of frac and then
>
>definition
>  let i1,i2 be Integer;
>  func i1 mod i2 -> Integer equals
>:: INT_1:def 8
>  i1 - (i1 div i2) * i2 if i2 <> 0
>  otherwise 0;
>end;

Just for the record the floor function is defined a little
bit earlier:

definition
  let r be real number;
  func [\ r /] -> Integer means
:: INT_1:def 4
  it <= r & r - 1 < it;
end;

(that is, the way you would expect it.)  Now XCMPLX_1:49
states that for all complex numbers

  a / 0 = 0

This all means that in Mizar

  i mod 0 = 0
  i div 0 = 0

for all integers i.  The second statement is INT_1:75, but I
don't find the first, although in REAL_3 there is the cluster

registration
  let n;
  cluster n div 0 -> zero;
  cluster n mod 0 -> zero;
  cluster 0 div n -> zero;
  cluster 0 mod n -> zero;
end;

Interestingly, in AOFA_I00 (Grzegorz' "Mizar Analysis of
Algorithms: Algorithms over Integers" from 2008), there is
the comment:

:: Remark:
:: Incorrect definition of "mod" in INT_1:  5 mod 0 = 0 i 5 div 0 = 0
:: and  5 <> 0*(5 div 0)+(5 mod 0)

This suggests that 5 mod 0 really should have been 5, right?
(And it makes me wonder: is "i" the Polish word for "and"?)

Freek

[Freek Wiedijk]

Andrzej:

>and always   0 <= abs(i mod j) <= abs j

So John apparently prefers to have

        0 <= i mod j < abs j

for negative j, although he didn't explain why.

Also, can you tell us what was the reason for taking

        i mod 0 = 0

instead of

        i mod 0 = i

?

Freek

[trybulec]

Hi John,

Artur and Freek explained the situation. Maybe it is worth to look how
it works with negative integers.

 (-7) div 3 = -3, (-7) mod 3 = 2
 so  -7 = ((-7) div 3)*3 + (-7) mod 3

for negative j,  i mod j is negative
7 div (-3) = -3, 7 mod (-3) =  -2
(-7) div (-3) = 2, (-7)  mod (-3) = -1

so for non zero j we have
     i = (i div j)*j + i mod j.

and always   0 <= abs(i mod j) <= abs j
(the second equality only for j=0).

We plan to generalize it to real numbers. Actually, it is long overdue.
Your message prompted us to do it in the next revision.
 I believe, Euclid did it for positive reals (for intervals), so back to
Euclid. The same goes for gcd and lcm.

Regards,
Andrzej


John Harrison wrote:

>I'm curious how Mizar defines division and modulus of integers where
>one or both arguments are negative.
>
>This is a well-known area where programming languages disagree or are
>undefined, so I'm doing a little survey of some of the world's leading
>theorem provers to see if there is a consensus there.
>
>John.
>
>  
>

[trybulec]

Hi Freek:

Freek Wiedijk wrote:

>Interestingly, in AOFA_I00 (Grzegorz' "Mizar Analysis of
>Algorithms: Algorithms over Integers" from 2008), there is
>the comment:
>
>:: Remark:
>:: Incorrect definition of "mod" in INT_1:  5 mod 0 = 0 i 5 div 0 = 0
>:: and  5 <> 0*(5 div 0)+(5 mod 0)
>
>This suggests that 5 mod 0 really should have been 5, right?
>(And it makes me wonder: is "i" the Polish word for "and"?)
>
>Freek
>
>  
>

Yes, you right 'i' is Polish for 'and'. The same in Russian.

I do not agree with Grzegorz' opinion. We do dirty tricks with the
division by 0, the only objective is to make the formalization easier.  
More general theorems (without assumption that a number is non zero) are
easier to use. _Technically_ more general because on the substantial
level it is nothing. A proof of such a theorem quite often needs to be
done per cases, and we want
the case zero to be simple. So the i mod 0 = 0 helps (and even more if
we use registration).

Artur pointed out  (we discussed the Grzegorz' complain yesterday) that
       i mo 0 = j mod 0
also helps to simplify the proof.

Regards,
Andrzej

[trybulec]

Freek Wiedijk wrote:

Andrzej:

  

and always   0 <= abs(i mod j) <= abs j
    

So John apparently prefers to have

	0 <= i mod j < abs j
  

I would like it. Actually, I was certain that it is the case in Mizar. Well, Mizar has a different opinion. But I would like
to have
     i = (i div j)*j + i mod j,
too. We can't probably have both?

for negative j, although he didn't explain why.
  

It was a simultaneous job. I have sent a message with an explanation seconds before I get this one.

Also, can you tell us what was the reason for taking

	i mod 0 = 0

instead of

	i mod 0 = i

?

Freek

  

[John Harrison-7]

Freek writes:

| So John apparently prefers to have
|
| 0 <= i mod j < abs j
|  
| for negative j, although he didn't explain why.

I was convinced by a discussion with Rob Arthan, and by reading:

  Raymond Boute:
  "The Euclidean definition of the functions div and mod".
  ACM TOPLAS vol. 14 (1992), pp127-144

that this definition fits more nicely with the "abstract algebra"
viewpoint. For example, you can think of "i mod j" as a canonical
representative of i's equivalence class modulo the ideal <j>. If you
think of it in this ideal-centric way, then since <j> = <-j>, the
representative should be independent of the sign.

Andrzej writes:

| I would like it. Actually, I was certain that it is the case in Mizar.
| Well, Mizar has a different opinion. But I would like
| to have
|      i = (i div j)*j + i mod j,
| too. We can't probably have both?

Well, you can have it if you're prepared to make the definition
"mod-dominant" in the terminology of Boute's paper, i.e. define mod
first and then div to make that equation hold. Boute distinguishes
three main possibilities, all of which satisfy that law for nonzero
divisor. (Like Freek, I support i div 0 = 0 and i mod 0 = i so it
holds even for zero divisors, and I've recently changed HOL Light's
definitions accordingly.) Then the choices are determined by the
following:

  T-definition: i div j = trunc(i / j), i.e. rounded towards zero
  F-definition: i div j = floor(i / j), i.e. rounded towards -infinity
  E-definition: 0 <= i mod j < |j|

The little survey of a few leading theorem provers that I conducted
(my message to this forum was part of it) came up with the following
results:

  ACL2: following Common LISP, provides different choices, floor/mod
        giving the F-definition and truncate/rem the T-definition.

  Coq: F-definition

  HOL Light: E-definition

  HOL4: F-definition, at least according to my reading of
        integerScript.sml, where the definition is a bit involved.

  Isabelle/HOL: F-definition, which section 8.4.3 of the Tutorial
                says is "mathematical practice".

  Mizar: F-definition

  ProofPower: E-definition

  PVS: Not defined for negative divisors in the PVS prelude. A
       supplementary NASA library uses the T-definition ("Ada style").

The HOL Light entry is cheating, really, since I chose it after
starting my survey and starting to think about the topic.

Note that common programming languages either tend to use the
T-definition or to leave it to the underlying hardware, which also
tends to use the T-definition. There is quite a nice Wikipedia page
with a survey:

  http://en.wikipedia.org/wiki/Modulo_operation 

John.

[Robert Boyer]

Hey, why discriminate against rounding towards positive
infinity (Lisp:ceiling) or to the nearest integer
(lisp:round).  And then, how to round 1/2?  Round to
odd?  Round to even?  I vote for adding 'round to
nearest prime' :)

Before you finally settle these important things, may I
suggest you also consult with Vel Kahan, the Turing
award winner who is largely responsible for the IEEE
floating point standard.  He has very serious and
considered views on such matters.  And Knuth, too.  It
would be so nice if we had an agreed upon formal
version of that IEEE standard.

In his book 'A Theory of Sets', A. P. Morse really
likes to make function calls on strange args, e.g.,
x/0, default to some default values rather than being
undefined or 'giving an error', whatever that may mean.
Morse's default approach certainly simplifies lemmas
and proofs, both for humans and machines.  Nqthm does a
lot of such defaulting in definitions and theorems.
'Social' obstacles, however, exist. If you default
where much of the world says 'undefined', others may
think your results queer, or never remember what your
defaults are, or get sloppy and use x^0=1 and 0^x=0 to
give rise to a contradiction, as in some in computer
algebra systems.  I remain unsure whether keeping the
undefined undefined is wisest.  Though Lewis Carol may
believe that words mean what he makes them mean, one
can go to jail for screaming 'Fire' in a theater even
if you make 'Fire' mean 'Popcorn'.

Bob

[John Harrison-7]

Hi Bob,

| Hey, why discriminate against rounding towards positive
| infinity (Lisp:ceiling) or to the nearest integer
| (lisp:round).  And then, how to round 1/2?  Round to
| odd?  Round to even?  I vote for adding 'round to
| nearest prime' :)

I was just limiting myself to the cases where Common LISP has both the
division function *and* the corresponding remainder function as a
pair, satisfying the usual division law. As far as I know there are
only the two integer remainder functions, mod and rem, even though
there are four versions of division. Is that right?

| Before you finally settle these important things, may I
| suggest you also consult with Vel Kahan, the Turing
| award winner who is largely responsible for the IEEE
| floating point standard.  He has very serious and
| considered views on such matters.  And Knuth, too.  It
| would be so nice if we had an agreed upon formal
| version of that IEEE standard.

I used to meet Kahan regularly because of the IEEE 754 revision
meetings, so I could have asked my question in person had my interest
been piqued earlier. I can send him an email anyway. Boute's paper
mentions that Knuth, in vol. 1 of The Art of Computer Programming,
gives the F-definition. Whether he merely mentions it or actively
advocates it, I don't know. (I only have volume 2 to hand at the
moment.)

| In his book 'A Theory of Sets', A. P. Morse really
| likes to make function calls on strange args, e.g.,
| x/0, default to some default values rather than being
| undefined or 'giving an error', whatever that may mean.
| Morse's default approach certainly simplifies lemmas
| and proofs, both for humans and machines.  Nqthm does a
| lot of such defaulting in definitions and theorems.

Traditionally, HOL has not done much of this, but I determinedly set
inv(0) = 0 over the reals (and later, over other structures). This is
particularly nice for streamlining lemmas, since it makes all these
handy rules true without exceptions, and they are the kind of thing
I use informally for simplifying rational functions without even
thinking:

 inv(x * y) = inv(x) * inv(y)
 inv(inv(x)) = x
 inv(x) = inv(y) <=> x = y

Nevertheless, some people find it upsetting, particularly since 0 is
as far away as possible from their preferred intuition of "infinity",
whatever that may mean to them.

| I remain unsure whether keeping the undefined undefined is wisest.

I share your doubts exactly for the reasons you stated. But then,
given that our logics (unlike, say, IMPS) don't have a first-class
notion of undefinedness, there is always going to be some dissonance
with an intuition based on undefinedness. For example, one would
expect to have x / y defined as x * inv(y) in any ring, which would
still give 0 / 0 = 0 however one defines inv(0). Well, in an
untyped setting like pure set theory or ACL2 you have a bit more
freedom to choose a value that isn't even in the ring, I suppose.

Incidentally, if one considers "i mod j" to be, as I said in my
earlier message, a canonical representative of the image of i in the
quotient ring Z/<j>, then "i mod 0 = i" just looks right because
Z/<0> is isomorphic to Z.

John.

[trybulec]

John Harrison wrote:

>  E-definition: 0 <= i mod j < |j|
>  
>

So, 0 <= i mod 0 < |0| ?

Regards,
Andrzej

[Freek Wiedijk]

John:

>Boute's paper mentions that Knuth, in vol. 1 of The Art
>of Computer Programming, gives the F-definition. Whether
>he merely mentions it or actively advocates it, I don't
>know. (I only have volume 2 to hand at the moment.)

I'm looking at it right now, and I think he just states
the definition, without explicit arguments for the specific
choice of that definition.

He does mention that the law

        0 <= x/y - floor(x/y) = (x mod y)/y < 1

holds for all y <> 0, so maybe that's one of the motivations?

For the record, here is his definition:

        x mod y = x - y*floor(x/y) if y <> 0
        x mod 0 = x

(Of course he doesn't have x/0 = 0, which explains why he
has the y = 0 case separately.)

[inv(0) = 0]
>Nevertheless, some people find it upsetting, particularly
>since 0 is as far away as possible from their preferred
>intuition of "infinity", whatever that may mean to them.

Not that it matters, but intuitionistically it does not
work either.  You get a non-continuous function, and in
the intuitionistic way of looking at things everything
is continuous.

>Well, in an untyped setting like pure set theory or ACL2
>you have a bit more freedom to choose a value that isn't
>even in the ring, I suppose.

The natural choices for a default element in those two
worlds seem to be the empty set and the NIL atom, but the
first actually happens to be the number zero :-)

Freek

[John Harrison-7]

Hi Andrzej,

| So, 0 <= i mod 0 < |0| ?

Ahem :-) When I wrote:

| Boute distinguishes three main possibilities, all of which satisfy
| that law for nonzero divisor. (Like Freek, I support i div 0 = 0 and i
| mod 0 = i so it holds even for zero divisors, and I've recently
| changed HOL Light's definitions accordingly.)

by "that law" I just meant the division law i = (i div j)*j + i mod j.
The characterizing properties of the three approaches to division
were just intended for nonzero divisors, and my introduction of the
case of zero was meant to be a separate question. It was probably
unwise of me to fold these together.

John.