Re: [mizar] Integer division

[freek <freek@cs.ru.nl>]

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