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



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.


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