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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.