*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] HOLCF's continuity with partially defined operators*From*: Joachim Breitner <breitner at kit.edu>*Date*: Mon, 23 Jul 2012 12:44:39 +0200*In-reply-to*: <CAAMXsiYgpvXL=+yWkh78sZrbJavWgz700eVA9FjBLMoQJsi21A@mail.gmail.com>*References*: <1343033044.4224.22.camel@kirk> <CAAMXsiYgpvXL=+yWkh78sZrbJavWgz700eVA9FjBLMoQJsi21A@mail.gmail.com>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Dear Brian, thanks for your reply. Am Montag, den 23.07.2012, 11:33 +0200 schrieb Brian Huffman: > 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. ah, right, I keep confusing the two names. I did mean the join (and I should just say supremum, which is a name less likely confused). > > > > 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" The problem is that for my types, defined as: domain Value = Fn (lazy "Value → Value") type_synonym Env = "(var, Value) fmap" the join does not always exist, so I could not instantiate the join_cpo class for Env. I thought about adding an artificial Top to my cpo, defining x ⊔ y to be that instead of undefined when there is no supremum of x and y. But it seems that this is not enough to make the join monotonous: If x ⊑ x' and x' ⊔ y exists it is possible that x and y, although having upper bounds, do not have a least upper bound. To make this work, I’d need arbitrary meets (this time I really mean meets) to exist in Value; not sure if that holds. What do you think of that approach? Greetings, Joachim -- 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

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

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

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