# 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.
`
Regards,
GB

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*