Re: [isabelle] Fixed Points and Denotational Semantics
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
> program P applied to a set X of final states returns the initial states
> 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
> exists in the complete lattice of monotonic predicate transformers
> You can find formalizations of these concepts in the AFP entries:
>  Semantics and Data Refinement of Invariant Based Program<http://afp.sourceforge.net/entries/DataRefinementIBP.shtml>
> (sections 3 and 4)
>  Algebra of Monotonic Boolean Transformers<http://afp.sourceforge.net/entries/MonoBoolTranAlgebra.shtml> (Section
> and corresponding papers:
>  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.
>  Preoteasa, Viorel. Refinement algebra with dual operator.
> *Science of Computer Programming*.
> http://dx.doi.org/10.1016/j.scico.2013.07.002. 2013.
>  and  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.
>  and  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>
> 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,
> 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
> 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)
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil
This archive was generated by a fusion of
Pipermail (Mailman edition) and