cps & contification

[Stephen Weeks]

> > Claim: For all f in Fun, there is a path in G from Root to f.
> 
> Do you have a quick proof for this?  I've been trying to work one out, but
> it keeps getting overly complicated.  It seems to me that the fact that A'
> is the least fixed point of C must be used.  Otherwise, functions which
> should be Uncalled could be assigned Unknown and lead to a disconnected
> graph.

Here's a proof.  I didn't look at yours yet, so I hope I didn't miss something
that yours makes obvious.  The proof does rely on A' being a lfp.  In
particular, it relies on the following claim.

Claim: A'(f) = Uncalled iff there is no path of calls from fm to f

Now define a directed graph G = (Node, Edge) where 
	Node = Fun U {Root}
	Edge = {(f, g) | (f, g) in T and A'(g) = Unknown}
		U {(Root, f) | A'(f) <> Unknown}
                U {(Root, f) | A'(f) = Unknown and exists (g, f, j) in N}
		U {(Root, fm)}

Claim: For all f in Fun, there is a path in G from Root to f.
Proof:
	If A'(f) = <> Unknown, then there is (Root, f) in Edge
	If A'(f) = Unknown,
		then there is a path of calls from fm to f since A' = lfp(C).
		If the last call on this path is a nontail call, we are done
		by the third clause in the definition of Edge.  Otherwise,
		consider longest suffix of this path that consists of all tail
		calls.  So we have something like
			(f0, f1) (f1, f2) ... (fn-1, f)
		If forall fi, A'(fi) = Unknown, 
			then there is a path from f0 to f in G
				if f0 = fm 
					then there is a path from Root to f in G
						since (Root, fm) in Edge
				else the previous element of the path from
					fm to f is a nontail call (g, f0, j) in N
					and hence (Root, f0) in Edge
			else Let fk be the last fi on the path such that
				A(fi) <> Unknown.  Then, (Root, fk) in Edge
				and there is a path from fk to f in G.