[isabelle] Fixed Points and Denotational Semantics
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!
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 - Brasi
This archive was generated by a fusion of
Pipermail (Mailman edition) and