*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] HOLCF's continuity with partially defined operators*From*: Joachim Breitner <breitner at kit.edu>*Date*: Mon, 23 Jul 2012 10:44:04 +0200*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Hello, I’m in the progress of formalizing Launchbury’s natural semantics for lazy evaluation. For the denotational part, I use HOLCF machinery (which was interesting to combine with Nominal, but it seems that I sailed around that cliff). The type of the semantic environments are a chain-complete partial order (typeclass cpo). My current problem is that Launcbury uses the meet on these, leaving it to the reader to believe that it is only used with arguments where the least upper bound exists. If I try to follow this path and define definition meet :: "'a => 'a => 'a" (infixl "⊔" 70) where "x ⊔ y = lub {x, y}" definition have_meet :: "'a => 'a => bool" where "have_meet x y = (∃ z. {x, y} <<| z)" then maybe I will be able to show the have_meet property everywhere where I use the meet. But to be able to use HOLCF’s machinery, e.g. the lemmas from CFun.thy and Fix.thy, I’d also have to show that the meet is continuous in both its arguments, and that is currently not the case; it is not even continuous, as x ⊔ y might exist, but x' ⊔ y for x' ⊒ x not. What would be a sensible way to tackle this problem? Using the type "'a => 'a => 'a option", introducing a notion of continuous_if_defined and re-creating most of HOLCF’s lemmas using this notation¹? Or maybe there is a way to extend the meet continuously? Thanks, Joachim ¹ I already had to do that for the lemmas and definitions in Fix.thy, as due to restrictions from Nominal, the environments need to have finite support. But the type of maps with finite domain (which I introduced) is not a pcpo, just a cpo, so I now have the notion of a least fixed point “above a certain value”. If someone has use for that type, help yourself at http://darcs.nomeata.de/isa-launchbury/, theories FMap, FMap-Nominal, FMap-HOLCF and FMap-Nominal-HOLCF. -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.info.uni-karlsruhe.de/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] HOLCF's continuity with partially defined operators***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Next by Date: Re: [isabelle] HOLCF's continuity with partially defined operators
- Previous by Thread: Re: [isabelle] Isabelle/jedit
- Next by Thread: Re: [isabelle] HOLCF's continuity with partially defined operators
- Cl-isabelle-users July 2012 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