*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] HOLCF's continuity with partially defined operators*From*: Brian Huffman <huffman at in.tum.de>*Date*: Mon, 23 Jul 2012 11:33:13 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1343033044.4224.22.camel@kirk>*References*: <1343033044.4224.22.camel@kirk>

On Mon, Jul 23, 2012 at 10:44 AM, Joachim Breitner <breitner at kit.edu> wrote: > 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. Hi Joachim, First of all, I should point out that what you have defined is the *join*, not the *meet*. The meet is the infimum, i.e. greatest lower bound. > > 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? I would probably define a subclass of cpo for types for which a continuous meet operation exists: class meet_cpo = cpo + fixes meet :: "'a -> 'a -> 'a" assumes "meet\<cdot>x\<cdot>y \<sqsubseteq> x" assumes "meet\<cdot>x\<cdot>y \<sqsubseteq> y" assumes "z \<sqsubseteq> x ==> z \<sqsubseteq>y ==> z \<sqsubseteq> meet\<cdot>x\<cdot>y" Most instances of this class would need to have a bottom element. If you really need a meet operation for unpointed cpo types, then you might try defining the meet on the lifted cpo instead: class meet_cpo' = cpo + fixes meet :: "'a u -> 'a u -> 'a u" assumes "meet\<cdot>x\<cdot>y \<sqsubseteq> x" assumes "meet\<cdot>x\<cdot>y \<sqsubseteq> y" assumes "z \<sqsubseteq> x ==> z \<sqsubseteq>y ==> z \<sqsubseteq> meet\<cdot>x\<cdot>y" - Brian

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

**References**:**[isabelle] HOLCF's continuity with partially defined operators***From:*Joachim Breitner

- Previous by Date: [isabelle] HOLCF's continuity with partially defined operators
- Next by Date: Re: [isabelle] HOLCF's continuity with partially defined operators
- Previous by Thread: [isabelle] HOLCF's continuity with partially defined operators
- 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