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



On Thu, Jul 26, 2012 at 11:25 AM, Joachim Breitner <breitner at kit.edu> wrote:
> 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.

You should try constructing the witness for the binary meet directly
as a continuous function, e.g.

fixrec meet :: "Value_ → Value_ → Value_"
  where "meet⋅(Fn⋅f)⋅(Fn⋅g) =
    Fn⋅(Λ x. (Λ (up⋅a) (up⋅b). up⋅(meet⋅a⋅b))⋅(f⋅x)⋅(g⋅x))"

Using this definition, I was able to prove "(t ⊑ meet⋅u⋅v) = (t ⊑ u ∧
t ⊑ v)" by take induction on t.

[...]
> 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?

No magic should be necessary; binary meets of (continuous) functions
are defined pointwise.

- Brian





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