Re: [isabelle] Isabelle: A logic of total functions (?)



Hmmm - a little bit off topic  .. is the meta-Logic of Isabelle also in effect a logic of total functions as well?
Or could you build a logic of partial functions on top of it ? â not that this would help Alfio muchâ

My understanding about undefinedness and/or partial functions is that there are a variety
of ways to work with them - three-valued logics, adding bottom elements to semantic domains, having definedness side-conditions (everywhere)
all with their plusses and minusses - but there is no way to avoid some pain. You have find whatever hurts leasts (which depends on what you are trying to do), and stick with that.

RAndrew

> On 17 Apr 2015, at 16:16, David Cock <david.cock at inf.ethz.ch> wrote:
> 
> Just to reinforce this idea - there really is no getting away from the fact that HOL is a logic of total functions. If you try to define a partial function without e.g. option, you introduce unexpected relationships.
> 
> On 17 April 2015 4:23:42 PM CEST, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
>> Dear Alfio,
>> 
>> Your usage of undefined matches the usual conventions in Isabelle/HOL
>> specification tools. 
>> Whether it accurately models your specification depends on your
>> understanding of the 
>> specification. Nowadays in HOL, we are normally happy if we get a any
>> function definition 
>> that satisfies the specification. However, many packages internally
>> refine the 
>> specification. For example, you can prove that sumR evaluates to the
>> same value for all 
>> intervals (l,r) with r < l (but you don't know which one).
>> 
>> If you wanted to model say a hardware instruction of a processor with
>> under-specified 
>> behaviour, then this usage of undefined is probably not faithful,
>> because the result of 
>> executing the instructor for r < l may probably depend on l, r, the
>> weather and whatever 
>> else. So it really depends on what you are trying to define and do.
>> 
>> Andreas
>> 
>> On 17/04/15 15:52, Alfio Martini wrote:
>>> Dear Isabelle Users,
>>> 
>>> Taking into account the discussion  that follow, I would like to know
>> if my
>>> use of the constant "undefined"  is correct
>>> or justified. I wanted to avoid the option type at all costs and in
>> some of
>>> the
>>> examples below I would not even know how to use it.
>>> 
>>> To begin with, I wanted to define a paryial recursive function such
>> that the
>>> following (informal) specification is satisfied:
>>> 
>>> sumR: int -> int ->_par int
>>> -- a partial function to sum the first k integers between
>>> --  l and u. It is not defined when l>u.
>>> requires l <= u
>>> ensures sumI(l,u) = \Sigma_{l<=k<=u} k
>>> 
>>> I came up with the following solution (well I did a pencil and paper
>>> proof and have yet to check it with Isabelle/Isar):
>>> 
>>> function  sumR:: "int => int => int" where
>>> "sumR   n n = n" |
>>> "n <  m ==> sumR n m = m + sumR n (m - 1)"|
>>> "n>m ==> sumR n m = undefined"
>>> apply atomize_elim
>>> apply auto
>>> done
>>> termination sumR
>>> apply (relation "measure (Î(i,N). nat ((N+1) - i))")
>>> 
>>> apply auto
>>> done
>>> 
>>> Similarly, the definition of an integer division that satisfies the
>>> following specification
>>> 
>>> div:: nat => nat => nat
>>> requires n>0
>>> ensures div m n = floor(m/n)
>>> 
>>> can be given by
>>> 
>>> function  divV::"nat â nat â nat" where
>>> "x < Suc y ==> divV x (Suc y) = 0"|
>>> "xâ Suc y ==> divV x (Suc y) = 1 + divV (x - Suc y)  (Suc y)"|
>>> "divV x 0 = undefined"
>>> apply atomize_elim
>>> apply auto
>>> apply arith
>>> done
>>> termination by lexicographic_order
>>> 
>>> Then I remembered that primitive recursive definitions allow for non-
>>> exaustive patterns.
>>> So divV can be given a simpler definition like this:
>>> 
>>> fun divN:: "nat â nat â nat" where
>>> "divN x (Suc y) = (if x < Suc y then 0 else 1 + divN (x - Suc y) 
>> (Suc y))"
>>> 
>>> In this case, Isabelle prints the following warning, which means to
>> that it
>>> uses "undefined" in the internal
>>> workings of the primrec package.
>>> 
>>> constants
>>>   divN :: "nat â nat â nat"
>>> Missing patterns in function definition:
>>> /\ a. divN a 0 = undefined
>>> 
>>> 
>>> 
>>> Looking at previous discussions about this in the mailing list, I
>> found
>>> this enlightening explanation
>>> from Andreas:
>>> 
>>> 
>>> A long time ago (before Isabelle2009), "undefined" was called
>> "arbitrary",
>>>> and "arbitrary"
>>>> reflected the specification of the element better: it was some
>> element of
>>>> the type.
>>>> However, as definitional packages (and some users) used undefined
>> for
>>>> cases when the
>>>> desired specification of a constant did not say anything, it got
>> renamed
>>>> to undefined. But
>>>> logically, it still is just an arbitrary element of the type. And
>> None
>>>> would be a very
>>>> special element of that type.
>>>> Hope this helps,
>>>> Andreas
>>> 
>>> 
>>> 
>>> Thanks for any explanation of my use of "undefined".
>>> 
>>> Best!
>>> 
> 
> -- 
> Sent from my Android device with K-9 Mail. Please excuse my brevity.

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