Re: [isabelle] The theory Option
On 14-10-07 15:37, W. Douglas Maurer wrote:
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.
On 14-10-07 17:30, Jasmin Christian Blanchette wrote:
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.
It seems to me, division in HOL is another example of the use of types
in Isabelle/HOL, without the benefit of types.
If I knew anything much more about HOL numbers than that the successor
of 0 is 1, I would define a new type, real_minus_zero, using typedef of
course, and then I would define division so that the denominator of
division is of type real_minus_zero. You can't get divide by zero if the
type guarantees no zero in the denominator.
The use of real_minus_zero would be effortless, because it would
automatically get coerced to real. Or maybe it wouldn't be effortless,
because now there would be two types to deal with, instead of just one.
This archive was generated by a fusion of
Pipermail (Mailman edition) and