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



On Fr, 2015-04-17 at 17:53 +0200, David Cock wrote:
> There are people on this list better qualified to answer than me 
The same applies to me ;)

> but no, the meta-logic does not require it. More general domains are possible, see HOL-CF.
In my understanding, HOL-CF is build entirely on top of HOL, 
introducing it's own function type, which is a (typedef) subtype of a=>b

In Pure, the reflexivity rule is already there, e.g., you can prove:

f x == f x

even for places x where f is undefined.

And you can use ==-equalities to prove substitutions in your theorems
(as done, e.g., by the (Pure) conversion mechanism).

Is this behaviour compatible with the goal of specifying a logic with
partial functions?

--
  Peter



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






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