*To*: Viorel Preoteasaa <viorel.preoteasa at abo.fi>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Fixed Points and Denotational Semantics*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Wed, 9 Oct 2013 09:26:27 -0300*In-reply-to*: <4D9521E7-8E35-4E2C-9D8D-171B1C6BE448@abo.fi>*References*: <CAAPnxw3vjYU=JkC_+OnoY3Av8QHdBy6_FE3_cgoJ4So0k=K8+w@mail.gmail.com> <52541771.8040309@inf.ethz.ch> <CAAMXsibtk9snE7CWPE673+do6BQ7F7dYS1DTOGkhBQRPaudW-w@mail.gmail.com> <4D9521E7-8E35-4E2C-9D8D-171B1C6BE448@abo.fi>*Sender*: alfio.martini at gmail.com

Thank you Viorel for the very detailed reply and the great references. I was not aware of them! All the Best! On Wed, Oct 9, 2013 at 8:37 AM, Viorel Preoteasaa <viorel.preoteasa at abo.fi>wrote: > 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 Program<http://afp.sourceforge.net/entries/DataRefinementIBP.shtml> > s > (sections 3 and 4) > [2] Algebra of Monotonic Boolean Transformers<http://afp.sourceforge.net/entries/MonoBoolTranAlgebra.shtml> (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 > > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) www.inf.pucrs.br/alfio Lattes: http://lattes.cnpq.br/4016080665372277 Associate Professor at Faculty of Informatics (PUCRS) Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil

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

**Re: [isabelle] Fixed Points and Denotational Semantics***From:*Viorel Preoteasaa

- Previous by Date: Re: [isabelle] Fixed Points and Denotational Semantics
- Next by Date: [isabelle] Isabelle2013-1-RC2 available for testing
- Previous by Thread: Re: [isabelle] Fixed Points and Denotational Semantics
- Next by Thread: [isabelle] Evaluation of record expressions
- 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