*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Fixed Points and Denotational Semantics*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 8 Oct 2013 11:13:52 -0300*Sender*: alfio.martini at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Fixed Points and Denotational Semantics***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Poor man's LaTeX markup for Isabelle listings
- Next by Date: Re: [isabelle] Fixed Points and Denotational Semantics
- Previous by Thread: Re: [isabelle] Auto sledgehammer fails to find proofs sledgehammer finds.
- 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