cps & contification

[Stephen Weeks]

> > Claim: A'(f) = Uncalled iff there is no path of calls from fm to f
> 
> p = (fm, {(g,f,K1),(g,f,K2)}, {(fm,h)})
> 
> There is no path of calls from fm to f, but A'(f) = Unknown.

You're right.  That was due to a bug in the definition of C, not a bug in the
claim :-).  Here's the new definition of C (which I think now corresponds to the 
continuation-based analysis as implemented).

Define the function C: Analysis -> Analysis by
	C(A)(g) =
	     if g = fm
	       then Unknown
	     else lub ({j | (f, g, j) in N and A(f) = Uncalled}
                       U {A(f) | (f, g) in T})

This definition also makes monotonicity of C more obvious.

With this defintion of C, here is A' for the above p, and the claim holds.

	f	A'(f)
	---	-----
	fm	Unknown
	g	Uncalled
	f	Uncalled
	h	Unknown

> Ideally, we'd like to say that A(f) = Uncalled, but I don't think that
> will come out of this analyis.  In a similar vein, we could have
> 
> p = (fm, {(g,f,K1),(g,f,K2)}, {(fm,f)})
> 
> We'd like A(f) = fm, but we'll end up with A(f) = Unknown.  

I believe that with the new C this will be correct (i.e. A(f) = fm) as well.