*To*: Alfio Martini <alfio.martini at acm.org>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Fixed Points and Denotational Semantics*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 8 Oct 2013 16:32:17 +0200*In-reply-to*: <CAAPnxw3vjYU=JkC_+OnoY3Av8QHdBy6_FE3_cgoJ4So0k=K8+w@mail.gmail.com>*References*: <CAAPnxw3vjYU=JkC_+OnoY3Av8QHdBy6_FE3_cgoJ4So0k=K8+w@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Hi Alfio,

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!

**Follow-Ups**:**Re: [isabelle] Fixed Points and Denotational Semantics***From:*Brian Huffman

**References**:**[isabelle] Fixed Points and Denotational Semantics***From:*Alfio Martini

- Previous by Date: [isabelle] Fixed Points and Denotational Semantics
- Next by Date: [isabelle] Evaluation of record expressions
- Previous by Thread: [isabelle] Fixed Points and Denotational Semantics
- Next by Thread: Re: [isabelle] Fixed Points and Denotational Semantics
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list