Re: [isabelle] undefined & None



Further to Stephan's response...

The type of "None" is "T option", for any type T. Suppose T has elements {a,b,c,d}. Then "T option" will contain the elements {None, Some a, Some b, Some c, Some d}. "None" is just an extra element added to the type.

"None" is often used when defining partial functions: an input is sent to "None" when the partial function is not defined for that input. But otherwise "None" and the special "undefined" constant are completely unrelated.

There are other uses of "None", unrelated to definedness. For instance, None could represent an error in a calculation. A division function might return "Some 10" when asked to divide 50 by 5, and "None" when a division-by-zero is attempted. Another use is to represent natural-numbers-with-infinity. The type "nat" only includes finite numbers, but if you use "nat option" then you can use "None" to stand for infinity.

In short, None is just an extra element added to an existing type.

john



On 14 Jul 2013, at 10:22, Stephan Merz wrote:

> Henri,
> 
> On Jul 13, 2013, at 11:17 PM, Henri DEBRAT <Henri.Debrat at loria.fr> wrote:
> 
>> I try to discover where the undefined value is ... defined. I could not find any undefined_def lemma or axiom.
>> 
>> In particular, is it polymorphic ? What are its properties ? What are the mathematical foundations and consequences of how it has been defined ?
> 
> grepping for undefined in src/HOL yields
> 
> HOL.thy:axiomatization undefined :: 'a
> 
> As you can see, the constant is not defined but declared as a polymorphic constant for arbitrary type. This is logically unproblematic because types in HOL must be non-empty. The value denotes some unspecified value of arbitrary type, this is sometimes useful when no particular property of the value is required.
> 
> Note that in theory Hilbert_Choice one could actually define
> 
> definition undefined where "(undefined::'a) = Some (x::'a). True"
> 
>> I also wonder why the "None" option types constructor does not point to undefined in some way or another. Furthermore, I do not understand whether None is typed of not. 
> 
> Since "undefined" is polymorphic, it exists for any option type. Defining "undefined :: 'a option" to be None would be more specific than what is required.
> 
> Hope this helps,
> 
> Stephan
> 
> 





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