[isabelle] The theory Option
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. 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
absurdities. I've done complex analysis myself (my theorem says that
if S and S' are countable dense sets on the complex plane, there
exists an entire function taking S onto S') so I should be believable
when talking to complex analysts.
Is there a good reason why this wouldn't work in practice?
Prof. W. Douglas Maurer Washington, DC 20052, USA
Department of Computer Science Tel. (1-202)994-5921
The George Washington University Fax (1-202)994-4875
This archive was generated by a fusion of
Pipermail (Mailman edition) and