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

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



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