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



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.

- Brian





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