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



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
Description: This is a digitally signed message part



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