*To*: Andrew Butterfield <Andrew.Butterfield at scss.tcd.ie>*Subject*: Re: [isabelle] Isabelle: A logic of total functions (?)*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Fri, 17 Apr 2015 17:47:33 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>, David Cock <david.cock at inf.ethz.ch>, Alfio Martini <alfio.martini at acm.org>*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>

Yes itâs possible, e.g. a logic with a definedness predicate could be defined. LCF and HOLCF are also, in effect, logics of definedness, in that you can reason about whether or not something is the value UU (undefined), which really is treated specially, in that it induces a partial ordering on all types. They are all a pain to use. Larry Paulson > On 17 Apr 2015, at 16:43, 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.

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