Re: [isabelle] The theory Option



Dear W. Douglas,

 Jasmin is quite right about the disadvantage of Option, but if you still feel the need
to use it, it might be worth looking at “monads” - specifically the technique adopted by
Haskell programmers to handle I/O and structure large programs.

This allows a form of encapsulation of an Option type where the propagation of None
is done “under the hood”

For the Haskell take on monads see : http://www.haskell.org/haskellwiki/Monad
and http://en.wikipedia.org/wiki/Monad_(functional_programming)#The_Maybe_monad

You want the “Maybe Monad”   -  “Maybe” is Haskell for “Option"

I’m not sure what Isabelle/HOL theory introduces monads, but I am sure one exists.

We did a comparative study reasoning about I/O in pure lazy functional languages
back in the early/mid noughties, looking at both Haskell (uses monads for I/O)
and Clean (uses uniqueness (linear) typing) and found it was easier to *reason* about
Clean I/O if we cast it into a monadic-style (quite easy to do).

So if you do want to reason about Option, 
and are happy for the rule  None `op` * = None =  * `op` None to hold,
then a monadic approach should be the easiest.

Andrew.
On 7 Oct 2014, at 23:30, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:

> 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 
>> absurdities.
> 
> 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.
> 
> Regards,
> 
> Jasmin
> 
> 

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero at TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                          http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------





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