cps & contification

[Matthew Fluet]

> > ... but if F is not monotone,
> > then I don't know of any correct and efficient method of calculating it.
> ...
> > Note: a solution to this does exist; Gamma = {l |--> l} will always be a
> > solution.  Since there is an ordering on Gamma, then a least fixed point
> > does exist as well, although not necessarily unique.
> 
> This last point does not follow.  

You're right.  What I had in mind was the fact that a solution Gamma where
Gamma(f) = l' and l' <> f is always better than a solution Gamma' where
Gamma'(f) = f; the actual l' don't really matter from the point of view of
determining that f is contifiable, although they do matter from the point
of view of determining where f should be contified.  This touches on the
issue of how deep lexically to insert the contified function.

> > It finally hit me: in the new analysis, REnv is not a continuous function
> > domain, so Gamma(fi) is not a continuous operation; that clearly keeps F
> > from being a continuous function.  But in the old analysis, REnv was a
> > continuous function domain, so Gamma(fi) is a continuous operation. 
> 
> I don't understand this last paragraph.  In both analyses, REnv is a complete
> lattice of functions, ordered pointwise.  What does it mean for REnv to be a
> continuous function domain?  I have a feeling we were brought up with different
> terminology :-)  I think you're basically saying what I was about the fact that 
> propagating RConts from one label to another causes nonmonotonicity in the new
> analysis while it does not in the old analysis (recall that monotonicity is a
> necessary condition for continuity).
> 
> Anyways, feel free to ignore my last paragraph if you think we're on the same
> wavelength.

I think we pretty much are.  Basically, I think it comes down to the fact
that  Gamma(fi)  by itself is not the element of a cpo, because RCont is
not a cpo.  That's causing the sidewise movement that you noted and is
causing the non-monotonicity.