Re: [mizar] Integer division

[John Harrison <John.Harrison@cl.cam.ac.uk>]

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.