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