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



Dear Brian,

Am Montag, den 23.07.2012, 13:47 +0200 schrieb Brian Huffman:
> 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.

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


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