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 MHonArc.