*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] The theory Option*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Wed, 08 Oct 2014 13:23:30 +0200*In-reply-to*: <1DD2F112-6260-4A03-A42B-B1F33D94347C@scss.tcd.ie>*References*: <a06200713d059fe24adb2@[192.168.1.10]> <637E28C3-9D2A-4031-A0FD-D6887CCCC95E@in.tum.de> <1DD2F112-6260-4A03-A42B-B1F33D94347C@scss.tcd.ie>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.1.1

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/ --------------------------------------------------------------------

**References**:**[isabelle] The theory Option***From:*W. Douglas Maurer

**Re: [isabelle] The theory Option***From:*Jasmin Christian Blanchette

**Re: [isabelle] The theory Option***From:*Andrew Butterfield

- Previous by Date: Re: [isabelle] The theory Option
- Next by Date: [isabelle] Two new AFP entries: XML and Certification Monads
- Previous by Thread: Re: [isabelle] The theory Option
- Next by Thread: Re: [isabelle] The theory Option
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list