Re: [isabelle] Fixed Points and Denotational Semantics
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,
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
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
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