cps & contification

[Matthew Fluet]

> Let A' = lfp(C).  
> 
> 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 and exists (g, f, j) in N}
> 		U {(Root, f) | A'(f) <> Unknown}
> 		U {(Root, fm)}
> 
> 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.

E.g. p = (fm, {(f, g), (g, f), (g, g)}, {})
Then A''(f) = A''(g) = Unknown is a fixed point of C,
 but yields a disconnected graph.


Here's where I've gotten:

Lemma: Let f in Fun.
       Suppose there does not exist a path from Root to f in G.
       Then f <> fm
	and A'(f) = Unknown
        and there does not exist (g, f, j) in N
        and there exists (g, f) in T
        and forall (g, f) in T,
            there does not exist a path from Root to f in G.
Proof:
Suppose there does not exist a path from Root to f in G.
 Then f <> fm (else (Root, f) in Edge).
 Then A'(f) = Unknown (else (Root, f) in Edge).
 Then there does not exist (g, f, j) in N (else (Root, f) in Edge).
 Suppose there does not exist (g, f) in T.
  Then f <> fm and
       there does not exist (g, f, j) in N and
       there does not exist (g, f) in T.
  Hence, A'(f) = lfp(C)(f) = Uncalled.
  But A'(f) = Unknown. ==><==
 Hence, there exists (g, f) in T.
 Then, (g, f) in Edge.
 Hence, forall (g, f) in T, there does not exist a path from Root to f in G.


By repeated application of the above lemma, we get

Claim: Let f in Fun.
       Suppose there does not exist a path from Root to f in G.
       Then forall g in the transitive closure of the set of callers of f,
            g <> fm
        and there does not exist (h, g, j) in N
        and there exists (h, g) in T

Now there's the step I'm having problems formalizing:

Claim: Let f in Fun.
       Suppose there does not exist a path from Root to f in G.
       Then forall g in the transitive closure of the set of callers of f,
        A'(g) = Uncalled.
Proof: Essentially, the above claim guarantees that there does not
        exist (h, g, j) in N for any g.
       So, A'(g) = j such that forall (h, g) in T. A'(h) = j.
       But all h satisfying (h, g) are also in the transitive closure
        of the set of callers of f.
       So, the least fixed point must have A'(g) = Uncalled

Finally, you get the contradiction:
If there does not exist a path from Root to f in G,
then A'(f) = Uncalled,
then (Root, f) in Edge,
then there exists a path from Root to f in G. ==><==