# CWS paper

**Matthew Fluet
**
Matthew Fluet <fluet@CS.Cornell.EDU>

*Wed, 6 Dec 2000 16:00:54 -0500 (EST)*

>* I'm a bit confused by your analysis. Here's what I understand after the latest
*>* modification.
*>*
*>* RCont = Func U Jump U {bot}
*>* REnv = Func -> RCont
*
I think it will be
REnv = (Func U Jump) -> RCont
because you want the rule:
R[let fun k <xi>* = e in e']p = R[e]p' V Gamma
where Gamma = R[e']p and p' = Gamma(k)
>* Here is your latest definition of <=l, which is a reflexive, transitive binary
*>* relation on RCont.
*>*
*>* > bot <=l l' <=l l forall l' in Label
*>*
*>* I'm afraid I don't understand what this means. Where is "l" quantified? As
*>* best as I can make out, this says that every label is <=l every other label.
*>* I.E. the relation is pretty trivial.
*>*
*>* Can you define <=l again for me?
*>*
*>* Do you mean for <=l to be a partial order?
*
I want <=l to the partial order imposed on RCont when interpreted relative
to the label l. The partial order on REnv is "pointwise" in the sense
that it's defined as:
Gamma1 <= Gamma2
iff
forall l in Label. Gamma1(l) <=l Gamma2(l)
where
bot <=l l' <=l l forall l' in Label
So, (Func U Jump U {bot}, <=l) corresponds to the squashed powerset
domain, with bot for {}, l' for {l'} (where l' <> l), and l for everything
else.