Re: [isabelle] Fixed Points and Denotational Semantics



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
> 




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