cps & contification
Stephen Weeks
MLton@sourcelight.com
Wed, 17 Jan 2001 14:42:34 -0800 (PST)
> > 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.