Re: [isabelle] Fixed Points and Denotational Semantics



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.

lfp has type "('a => 'a) => 'a" where 'a must be of sort complete_lattice. _ set instantiates complete_lattice, so lfp can in particular be used for functionals on all sets. But you can also use other types that instantiate complete_lattice. For example, if 'a is a complete lattice, then so is _ => 'a, i.e., you can also use functions.

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.

All of the above solutions are based on type classes, and this is what makes them convenient. The package partial_function provides some front-end to fixp that does not rely on type classes, but I recommend that you use the type classes, because they make definitions and proofs much simpler.

Hope this helps,
Andreas

On 08/10/13 16:13, Alfio Martini wrote:
Dear Isabelle Users,

I (kind of) wanted to star playing a bit with fixpoint operators in
Isabelle, which is motivated by  experiments in denotational
semantics of imperative languages.

I have noticed that the theories available in the Isabelle
distribution (concerning the IMP language) follow Winskel´s
relational approach. That is to say, the denotation of a command
is a set of pair of states, and then one can easily define
the semantics of while by the least fixpoint of the appropriate
functional using Isabelle´s lfp fixpoint operator.

In general, the fix point operator  fix  has type
(D->D)->D where D must be a chain complete cpo with
a least element (according to Winskel´s Lecture Notes on
Denotational Semantics). In Isabelle, the operator
lfp has type ('a ->'a)->'a, and it is defined in the
theory Complete Lattice. So, what is the minimal requirement
in Isabelle

On the other hand, in section 6.5 of the Isabelle/HOL tutorial
the type of 'a is also a set of pairs and in the discussion
it is implied that 'a must always be a set.
The book "Concrete Semantics"
by Nipkow and Klein also uses a relational semantics

So  my main questions are:

1) How to use the fixpoint operator on functionals that
are not based on sets of pairs? ?

2) Do I need complete lattices or cpo´s with least elements
suffice?

3) Can I use functionals where D is a function space
(for instance, using partial maps provided by Isabelle).

4) Do I have to use type classes to make the appropriate
instantiations? (If yes I have no idea how)

Thanks for any help. This will be a long journey!





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