Re: [isabelle] The theory Option



Just a side remark. Syntax for Haskell-style do notation is made available by ~~/src/HOL/Library/Monad_Syntax.thy (where also a bind operation for the option type is registered).

However, at least for this Isabelle/HOL version of monads I would argue that not much is done "under the hood". It's just notational convenience (the famous "syntactic sugar") and does not make reasoning any easier.

cheers

chris

On 10/08/2014 09:33 AM, Andrew Butterfield wrote:
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.