Dear W. Douglas,
Am 07.10.2014 um 22:37 schrieb W. Douglas Maurer <maurer at gwu.edu>:
I've been looking at theory Option for some time now, and I've been
wondering why it isn't used more often than it is. If you're going to
have a type with an extra element called None, an obvious use of this
(obvious to me, anyway) would be to interpret None as "undefined."
Division of real numbers, for example, could be a function from (real
option) x (real option) -> real option, with x/0 = None and None/x =
y/None = None. This is in fact exactly how floating point numbers
work on computers today, except that there None is called NaN, which
is an abbreviation for Not a Number.
The advantage of this over the current system of using zero to mean
"undefined" is that there you can't tell the difference, after the
fact, between a zero meaning "undefined" and a real zero.
Any scheme is bound to have advantages and inconvenients. The difficulty above arises when you pass the result of division to another operator, e.g. "+". Would addition also take two options as argument? If yes, this leads to a number of issues:
1. At definition time: All operations must specify a behavior in case some of their arguments are "None".
2. At lemma-stating time: Many properties only hold for non-"None" values and must hence be written carefully, e.g. "x + 1 > x" becomes "Some x + Some 1 > Some x".
3. At reasoning time: In your proofs, you then need to perform case distinctions.
If not, this means you must introduce a "case" construct or a "the" each time you have a division inside, say, a "+". (And "the" isn't much better than not using options at all.)
The situation with NaN is illustrative -- how many actual programs work correctly once NaNs have started appearing in computations? Many procedures are written without considering the case where the inputs are NaN, nor is much thought given to when they may arise in much of the programming out there (with some noteworthy exceptions). Why? Because the alternative is clumsy and tedious, and without formal verification or a rich type system it's hard to catch all cases.
Another advantage for me is that if I'm trying to explain Isar to
mathematicians who are complex analysts or other non-algebraists, as
I intend to try to do, it could take a lot of explaining to convince
them that defining x/0 to be 0 (rather than None) doesn't lead to
This doesn't have to be difficult.
As far as absurdities are concerned, there is no risk between "x/0" is *defined* as meaning something, as opposed to axiomatized. One could also define "2 + 2 = 5" and use it to prove many things; this wouldn't lead to absurdities either (but would give addition different properties than what we are used to). Absurdities start arising when you overconstraint your specification, which can in principle only happen if you use axioms (or re-definitions, which Isabelle forbids).
To take another example: Donald Knuth defines the binomial coefficients also for negative values of either numbers. This is nonstandard, but he won't be able to derive false that way. Problems will only occur if you combine his results with those from Joe Hacker, who also extends the binomial coefficients but in a different, incompatible way. Clearly, one cannot use two different, incompatible definitions for the same symbol and mix-and-match the corresponding theorems naively.
This having been said, there is a slight catch with "x/0 = 0". If your main definitions and theorems use division, this must be born in mind when reading them, communicating them to fellow mathematicians, etc. (The same issue arises with Knuth's theorems about binomial coefficients.) This is regrettable, and much could be said in favor of leaving "x/0" unspecificed or equal to "undefined". Or you could avoid Isabelle's division in your main interface with mathematicians, relying on your own division operator instead that would be unspecified for 0.
In short, if it takes a lot of convincing, this means that either the explanation is unclear or that they don't understand what a definition is. I would presume mathematicians are familiar enough with definitions.