*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*: Wed, 25 Jul 2012 13:54:47 +0200*In-reply-to*: <CAAMXsiahLz3wyUsjGfP9eU5hKBmD=Ymsm+R7wmR1BGc4F5x=qw@mail.gmail.com>*References*: <1343033044.4224.22.camel@kirk> <CAAMXsiYgpvXL=+yWkh78sZrbJavWgz700eVA9FjBLMoQJsi21A@mail.gmail.com> <1343040279.4224.38.camel@kirk> <CAAMXsiahLz3wyUsjGfP9eU5hKBmD=Ymsm+R7wmR1BGc4F5x=qw@mail.gmail.com>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Dear Brian, Am Montag, den 23.07.2012, 13:47 +0200 schrieb Brian Huffman: > On Mon, Jul 23, 2012 at 12:44 PM, Joachim Breitner <breitner at kit.edu> wrote: > > 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? > > Adding a top element (at least to the return type of the join > function) seems like a reasonable thing to do. > > Arbitrary meets exist in every Scott domain, so I would expect that > they exist in your Value type. > > I don't think omega-bifinite domains (aka SFP domains, formalized as > the default class "domain" in HOLCF) have arbitrary meets, though, so > you couldn't define a generic binary join function directly on class > "domain". You'll need to define a new subclass of cpo to use with your > binary join function, but I expect that it shouldn't be too hard to > instantiate it. I am trying this path, now that my class-related issues are resolved (thanks for that). I introduced a type class Top_cpo for cpo’s with top¹. Then I created a dual of HOLCF/Up.thy, e.g. a type "'a d" that adjoins a top element², with an instance for Top_cpo and the necessary setup to use it in domain equations (is this generally useful? Feel free to include it in HOLCF/Library). Finally I introduced type classes for cpo where meets of non-empty sets, arbitrary Meets and arbitrary Joins, respectively, exists, and showed that a type with top and arbitrary meets has arbitrary joins. I also shows that if 'a has non-empty meets, then "'a d" has. Then I defined domain Value_ = Fn (lazy "Value_ d → Value_ d") type_synonym Value = "Value_ d" and it seems that instantiating Nonempty_Meet_cpo for Value_ is what is left to do. Morally, things look clear to me: Either the set has a bottom, the the meet is bottom, or all elements are of the form "Fn _", then I take the meet pointwise. But this recurses, so I’m not sure how to define it. Because of the indirect recursion in the definition of Value_, no “normal” induction rules are available. My first approach would be to show that for every nonempty S, I find a meet of "Value__take i ` S" (and I am hoping that I can show this by induction on i, but I’m not sure yet). Then the lub of these seems to be the meet of M. I am a bit worried about the use of cfun_map in Value__take and whether it behaves well in the inductive step of the proof. Thanks, Joachim ¹ http://darcs.nomeata.de/isa-launchbury/HOLCF-Top.thy ² http://darcs.nomeata.de/isa-launchbury/Down.thy -- 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:*Joachim Breitner

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

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

**Re: [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] Isabelle/jedit
- Next by Date: Re: [isabelle] Proving cardinality
- 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