*To*: Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie>, Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Isabelle: A logic of total functions (?)*From*: David Cock <david.cock at inf.ethz.ch>*Date*: Fri, 17 Apr 2015 17:53:18 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <79E03E4A-0530-416A-A489-0B9FC8BDB382@scss.tcd.ie>*References*: <CAAPnxw2pFXpLG4sJjgorgKXm-awB2hRu5PymUuTPDZvacCxf-g@mail.gmail.com> <5531176E.4040004@inf.ethz.ch> <E7348706-8E1A-40E4-B218-2646B18C717A@inf.ethz.ch> <79E03E4A-0530-416A-A489-0B9FC8BDB382@scss.tcd.ie>*User-agent*: K-9 Mail for Android

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.

**Follow-Ups**:**Re: [isabelle] Isabelle: A logic of total functions (?)***From:*Peter Lammich

**References**:**[isabelle] Isabelle: A logic of total functions (?)***From:*Alfio Martini

**Re: [isabelle] Isabelle: A logic of total functions (?)***From:*Andreas Lochbihler

**Re: [isabelle] Isabelle: A logic of total functions (?)***From:*David Cock

**Re: [isabelle] Isabelle: A logic of total functions (?)***From:*Andrew Butterfield

- Previous by Date: [isabelle] Last Call for Papers: UNIF 2015
- Next by Date: Re: [isabelle] Isabelle: A logic of total functions (?)
- Previous by Thread: Re: [isabelle] Isabelle: A logic of total functions (?)
- Next by Thread: Re: [isabelle] Isabelle: A logic of total functions (?)
- Cl-isabelle-users April 2015 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