*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*: Thu, 26 Jul 2012 11:25:05 +0200*In-reply-to*: <CAAMXsibTcvy=kJfM2VtgooxmKep-ckVm25UjsFy=jYTTAzvyYQ@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> <1343217287.4148.17.camel@kirk> <1343227480.4148.32.camel@kirk> <CAAMXsibTcvy=kJfM2VtgooxmKep-ckVm25UjsFy=jYTTAzvyYQ@mail.gmail.com>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Dear Brian, Am Donnerstag, den 26.07.2012, 07:39 +0200 schrieb Brian Huffman: > > You know the domains better than me: Do you still expect that is > > possible to show the existence of arbitrary meets for such a data type, > > and if so, how? > > > > Thanks a lot in advance, > > Joachim > > Hi Joachim, > > Your idea of finding the meet of set M by taking the lub of a sequence > of meets of (take i ` M) is on the right track. > > I think you should be able to show that any bifinite domain with > binary meets has arbitrary nonempty meets. First, note that if you > have binary meets then you have all nonempty finite meets. Then from > bifiniteness, there exists a chain of approx functions: Like take > functions, these have their lub = ID, but more importantly each one > also has a finite range, so (approx i ` M) is always a finite set. > Finally, LUB i. Meet (approx i ` M) should give you the meet for M. thanks for the hint, here is my progress so far: I was able to define and proof the following class relations: class Finite_Meet_cpo = cpo + assumes binary_meet_exists: "∃ l. l ⊑ x ∧ l ⊑ y ∧ (∀ z. (z ⊑ x ∧ z ⊑ y) ⟶ z ⊑ l)" class Finite_Meet_bifinite_cpo = Finite_Meet_cpo + bifinite instance Finite_Meet_bifinite_cpo ⊆ Nonempty_Meet_cpo So indeed all I need to do is to give an instance Value_ :: Finite_Meet_cpo but it seems I am stuck at the same problem as before. To show the existence the meet of two values of the form "Fn f" and "Fn g" (while, by induction, knowing that their images have pairwise meets), I can define that as "Fn (Λ x . f x ⨅ g x)" but I have trouble showing that it is continuous. To add to my worries, here is an example which tries to transfer the analysis example from my last mail. It may just implies that there is little hope in relating the meet of a set of functions with the meet at its points. Consider a domain D such that D = Fn (lazy (D → D)), and these (hopefully continuous) functions: f :: D → D f x = Fn (λ _ . x) f' x = Fn (λ y . if y = ⊥ ⋀ x ⊑ µ f then x else µ f) g ⊥ = ⊥ g (Fn h) = h (Fn id) Now g (f x) = x and (⨆i. f^i ⊥) = (⨆i. f'^i ⊥) = µ f. Looking at (⨅i. g^i) I find pointwise (⨅i. g^i (f^j ⊥)) = ⨅{⊥} = ⊥ (⨅i. g^i (f'^j ⊥)) = ⨅{µ f} = µ f (⨅i. g^i (µ f) = ⨅{µ f} = µ f so if (⨅i. g^i) exists, it cannot be (λ x (⨅i. g^i x)). Of course ⊥ is still a candidate, and I don’t have an example handy where I find many lower bounds, but not a greatest. It seems that I don’t take the right approach to define the meet of two function values. Is there some more magic required to define the meet? Thanks a lot, 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

**Re: [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:*Joachim Breitner

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

- Previous by Date: Re: [isabelle] Unicode tokens in jedit
- Next by Date: Re: [isabelle] Sledgehammer and Nitpick from the command line?
- 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