Re: [isabelle] HOLCF's continuity with partially defined operators

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,

Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.