*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Fixed Points and Denotational Semantics*From*: Viorel Preoteasaa <viorel.preoteasa at abo.fi>*Date*: Wed, 9 Oct 2013 14:37:01 +0300*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Brian Huffman <huffman.brian.c at gmail.com>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <CAAMXsibtk9snE7CWPE673+do6BQ7F7dYS1DTOGkhBQRPaudW-w@mail.gmail.com>*References*: <CAAPnxw3vjYU=JkC_+OnoY3Av8QHdBy6_FE3_cgoJ4So0k=K8+w@mail.gmail.com> <52541771.8040309@inf.ethz.ch> <CAAMXsibtk9snE7CWPE673+do6BQ7F7dYS1DTOGkhBQRPaudW-w@mail.gmail.com>

Hi Alfio, Another approach of using least fix points for semantics of programs is when using a predicate transformer semantics. As compared to programs as relations which can be used for modelling partial correctness, predicate transformers allows modelling total correctness. If S is the set of computation states, programs are modelled as monotonic functions from power set of S (Pred.S = S->bool) to Pred.S. In this model a program P applied to a set X of final states returns the initial states from which P terminates, and it terminates in a state from X. Iteration can be defined in this model as a least fix point of a monotonic function from (Pred.S)->(Pred.S) to (Pred.S)->(Pred.S). This least fix point exists in the complete lattice of monotonic predicate transformers ((Pred.S)->(pred.S)) You can find formalizations of these concepts in the AFP entries: [1] Semantics and Data Refinement of Invariant Based Programs (sections 3 and 4) [2] Algebra of Monotonic Boolean Transformers (Section 3) and corresponding papers: [3] Preoteasa, Viorel and Back, Ralph-Johan. Invariant Diagrams with Data Refinement. Formal Aspect of Computing. Vol: 24, Num: 1, Pages 67-95. Springer London. http://dx.doi.org/10.1007/s00165-011-0195-2. 2012. [4] Preoteasa, Viorel. Refinement algebra with dual operator. Science of Computer Programming. http://dx.doi.org/10.1016/j.scico.2013.07.002. 2013. [2] and [4] introduces an algebra for modelling programs. The basic model for this algebra is set of monotonic predicate transformers with their operations, so everything that is done in the algebra is true in the model. Actually you will find the definition of the while statement and its properties the algebra part of the paper. The model contains just the the results needed to show that it is indeed a model for the algebra. [2] and [4] uses an arbitrary Boolean algebra B instead of Pred.S The algebra is more abstract than the model. In the algebra only fixed points of certain functions are axiomatised. These are the functions needed for defining the while statements. Best regards, Viorel Preoteasa On Oct 8, 2013, at 7:59 PM, Brian Huffman <huffman.brian.c at gmail.com> wrote: > On Tue, Oct 8, 2013 at 7:32 AM, Andreas Lochbihler > <andreas.lochbihler at inf.ethz.ch> wrote: >> Hi Alfio, >> >> Have you already looked at HOLCF? It formalises domain theory and >> denotational semantics. If not, that's where you should go first. Brian >> Huffman's PhD thesis describes what is in there and how to use it. > [...] >> If you only have a chain-complete partial order with a least element, you >> cannot use lfp, but instead fixp from the theory Complete_Partial_Order, but >> you have to deal with admissibility yourself. This is where HOLCF greatly >> helps you. > > Hi Alfio, > > I should point out a few differences between the HOLCF and > Complete_Partial_Order formalizations of fixpoints: > > Class ccpo from Complete_Partial_Order uses a slightly stronger > completeness condition than HOLCF uses; ccpo requires lubs of > arbitrary chains, while HOLCF requires lubs only for countable chains. > On the other hand, class ccpo has fixpoints for all monotone > functions, whereas HOLCF additionally requires functions to be > continuous. > > The other major consideration is that HOLCF uses a continuous function > space type "'a -> 'b" almost everywhere, rather than using ordinary > functions "'a => 'b" with a continuity predicate. One consequence is > that you are locked in to using type classes for cpos (type 'a -> 'b > is only defined for cpo types); Complete_Partial_Order is a bit more > flexible in this regard. > > That said, if you are willing to commit to using type classes and the > continuous function space type, HOLCF provides highly tuned automation > for proving continuity and admissibility. > > Whichever library you decide to use, I'd welcome any questions, > comments, or suggestions for improvements to either library. > > - Brian >

**Follow-Ups**:**Re: [isabelle] Fixed Points and Denotational Semantics***From:*Alfio Martini

**References**:**[isabelle] Fixed Points and Denotational Semantics***From:*Alfio Martini

**Re: [isabelle] Fixed Points and Denotational Semantics***From:*Andreas Lochbihler

**Re: [isabelle] Fixed Points and Denotational Semantics***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Isabelle2013-1-RC1 available for testing
- Next by Date: Re: [isabelle] Fixed Points and Denotational Semantics
- Previous by Thread: Re: [isabelle] Fixed Points and Denotational Semantics
- Next by Thread: Re: [isabelle] Fixed Points and Denotational Semantics
- Cl-isabelle-users October 2013 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