Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] HOLCF's continuity with partially defined oper...

Email Gateway (Aug 19 2022 at 07:50):

From: Joachim Breitner <breitner@kit.edu>
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.

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?

Thanks,
Joachim

¹ I already had to do that for the lemmas and definitions in Fix.thy, as
due to restrictions from Nominal, the environments need to have finite
support. But the type of maps with finite domain (which I introduced) is
not a pcpo, just a cpo, so I now have the notion of a least fixed point
“above a certain value”. If someone has use for that type, help yourself
at http://darcs.nomeata.de/isa-launchbury/, theories FMap, FMap-Nominal,
FMap-HOLCF and FMap-Nominal-HOLCF.
signature.asc

Email Gateway (Aug 19 2022 at 07:51):

From: Brian Huffman <huffman@in.tum.de>
On Mon, Jul 23, 2012 at 10:44 AM, Joachim Breitner <breitner@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

Email Gateway (Aug 19 2022 at 07:51):

From: Joachim Breitner <breitner@kit.edu>
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
signature.asc

Email Gateway (Aug 19 2022 at 07:51):

From: Brian Huffman <huffman@in.tum.de>
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

Email Gateway (Aug 19 2022 at 07:53):

From: Joachim Breitner <breitner@kit.edu>
Dear Brian,

I am trying this path, now that my class-related issues are resolved
(thanks for that).

I introduced a type class Top_cpo for cpo’s with top¹. Then I created a
dual of HOLCF/Up.thy, e.g. a type "'a d" that adjoins a top element²,
with an instance for Top_cpo and the necessary setup to use it in domain
equations (is this generally useful? Feel free to include it in
HOLCF/Library).

Finally I introduced type classes for cpo where meets of non-empty sets,
arbitrary Meets and arbitrary Joins, respectively, exists, and showed
that a type with top and arbitrary meets has arbitrary joins. I also
shows that if 'a has non-empty meets, then "'a d" has.

Then I defined
domain Value_ = Fn (lazy "Value_ d → Value_ d")
type_synonym Value = "Value_ d"
and it seems that instantiating Nonempty_Meet_cpo for Value_ is what is
left to do.

Morally, things look clear to me: Either the set has a bottom, the the
meet is bottom, or all elements are of the form "Fn _", then I take the
meet pointwise. But this recurses, so I’m not sure how to define it.

Because of the indirect recursion in the definition of Value_, no
“normal” induction rules are available. My first approach would be to
show that for every nonempty S, I find a meet of "Value__take i `
S" (and I am hoping that I can show this by induction on i, but I’m not
sure yet). Then the lub of these seems to be the meet of M. I am a bit
worried about the use of cfun_map in Value__take and whether it behaves
well in the inductive step of the proof.

Thanks,
Joachim

¹ http://darcs.nomeata.de/isa-launchbury/HOLCF-Top.thy
² http://darcs.nomeata.de/isa-launchbury/Down.thy
signature.asc

Email Gateway (Aug 19 2022 at 07:54):

From: Joachim Breitner <breitner@kit.edu>
Dear Brian,

I’m having a hard time showing that there are meets for my data type.
For the inductive proof of
∃ u. {Value__take i ⋅ x | x . x ∈ S } >>| u
in the case where I know that all elements of S have the form "Fn⋅_", I
need to show the existence of a meet of the image of set of continuous
functions ("S :: (Value_ d → Value_ d) set"), under cfun_map⋅f⋅g (where
f and g involve "Value__take i").

By induction, I know that "⨅ (g ` S')" exists for any S' of type
"Value_ d set", so pointwise, the meet exists. My hope was to show the
following lemma, which would then give me the existence of the meet of
the set of function:

lemma has_glb_cfunI:
assumes "(!! x. ∃ l. (λ f. f⋅x) ` S >>| l)"
shows "(∃ l. S >>| l)"

I did not manage to proof that, though, and I am worried that it might
not hold. By analogy from analysis, the set of functions on [0,2] given
by {x^n | n ∈ [1..∞]} has pointwise infimums, but itself none.

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
signature.asc

Email Gateway (Aug 19 2022 at 07:55):

From: Brian Huffman <huffman@in.tum.de>
On Wed, Jul 25, 2012 at 4:44 PM, Joachim Breitner <breitner@kit.edu> wrote:

Dear Brian,

Am Mittwoch, den 25.07.2012, 13:54 +0200 schrieb Joachim Breitner:

Then I defined
domain Value_ = Fn (lazy "Value_ d → Value_ d")
type_synonym Value = "Value_ d"
and it seems that instantiating Nonempty_Meet_cpo for Value_ is what is
left to do.

Morally, things look clear to me: Either the set has a bottom, the the
meet is bottom, or all elements are of the form "Fn _", then I take the
meet pointwise. But this recurses, so I’m not sure how to define it.

Because of the indirect recursion in the definition of Value_, no
“normal” induction rules are available. My first approach would be to
show that for every nonempty S, I find a meet of "Value__take i `
S" (and I am hoping that I can show this by induction on i, but I’m not
sure yet). Then the lub of these seems to be the meet of M. I am a bit
worried about the use of cfun_map in Value__take and whether it behaves
well in the inductive step of the proof.
[...]
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.

• Brian

Email Gateway (Aug 19 2022 at 07:55):

From: Joachim Breitner <breitner@kit.edu>
Dear Brian,

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,
Joachim
signature.asc

Email Gateway (Aug 19 2022 at 07:56):

From: Brian Huffman <huffman@in.tum.de>
On Thu, Jul 26, 2012 at 11:25 AM, Joachim Breitner <breitner@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

Last updated: Nov 21 2024 at 12:39 UTC