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



On Mon, Jul 23, 2012 at 10:44 AM, Joachim Breitner <breitner at kit.edu> wrote:
> Hello,
>
> I’m in the progress of formalizing Launchbury’s natural semantics for
> lazy evaluation. For the denotational part, I use HOLCF machinery (which
> was interesting to combine with Nominal, but it seems that I sailed
> around that cliff).
>
> The type of the semantic environments are a chain-complete partial order
> (typeclass cpo). My current problem is that Launcbury uses the meet on
> these, leaving it to the reader to believe that it is only used with
> arguments where the least upper bound exists.
>
> If I try to follow this path and define
>
>         definition meet :: "'a => 'a => 'a" (infixl "⊔" 70)
>           where "x ⊔ y = lub {x, y}"
>         definition have_meet :: "'a => 'a => bool"
>           where "have_meet x y = (∃ z. {x, y} <<| z)"
>
> then maybe I will be able to show the have_meet property everywhere
> where I use the meet.
>
> But to be able to use HOLCF’s machinery, e.g. the lemmas from CFun.thy
> and Fix.thy, I’d also have to show that the meet is continuous in both
> its arguments, and that is currently not the case; it is not even
> continuous, as x ⊔ y might exist, but x' ⊔ y for x' ⊒ x not.

Hi Joachim,

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.

>
> 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"

Most instances of this class would need to have a bottom element. If
you really need a meet operation for unpointed cpo types, then you
might try defining the meet on the lifted cpo instead:

class meet_cpo' = cpo +
  fixes meet :: "'a u -> 'a u -> 'a u"
  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"

- Brian





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