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



There are people on this list better qualified to answer than me but no, the meta-logic does not require it. More general domains are possible, see HOL-CF.

On 17 April 2015 5:43:59 PM CEST, Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie> wrote:
>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/
>--------------------------------------------------------------------

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