cps & contification

[Matthew Fluet]

> 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

p = (fm, {(g,f,K1),(g,f,K2)}, {(fm,h)})

There is no path of calls from fm to f, but A'(f) = 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.  We could run
the contification-based analysis repeatedly until there are no Uncalled
functions.  That might even simplify thinking about the second analysis.


Anyways, here's an alternative (but more complicated) version of the
proof that G is connected.

Lemma: Let h in Fun.
       Suppose !Path(Root,h).
       Then h <> fm,
        and !exists (g, h, j) in N
        and forall (g, h) in T. !Path(Root, g).
Proof:
Suppose !Path(Root, g).
 Then h <> fm (else (Root, h) in Edge).
 Then A'(h) = Unknown (else (Root, h) in Edge).
 Then !exists (g, h, j) in N (else (Root, h) in Edge).
 Then, forall (g, h) in T. !Path(Root, g).


Define: Pred(S) = { g | (g,f) in T, f in S }.
        Pred*(S) = U_{n >= 0) Pred^n(S).
        Pr(f) = Pred*({f}).
        (Pr(f) is the transitive closure of the tail callers of f.)

Claim: Let f in Fun.
       Suppose !Path(Root, f).
       Then forall h in Pr(f). h <> fm
                           and !exists (g, h, j) in N
                           and forall (g, h) in T. !Path(Root, g)
                           and forall (g, h) in T. g in Pr(f).
Proof:
Note forall h in Pr(f). forall (g, h) in T. g in Pr(f)
 follows from the definition of Pr(f).
Note Pr(f) = Pred*({f}) = U_{n >= 0) Pred^n({f}).
Proceed by induction on n.
n = 0: Let h in Pred^0({f}) = {f}.
       Then h = f and !Path(Root, f).
       By previous claim, f <> fm
                      and !exists (g, f, j) in N
                      and forall (g, f) in T. !Path(Root, f)
n > 0: Let h in Pred^n({f}).
       Then (h, i) in T, i in Pred^{n-1}({f}).
       By IndHyp, i <> fm
              and there does not exist (g, i, j) in N
              and forall (g, i) in T. !Path(Root, g).
       Hence, !Path(Root, h).
       By previous claim, h <> fm
                      and !exists (g, h, j) in N
                      and forall (g, h) in T. !Path(Root, g)


Claim: Let H subset Fun.
       Suppose forall h in H. h <> fm
                          and there does not exist (g, h, j) in N
                          and forall (g, h) in T, g in F.
       Then forall h in H. A'(h) = Uncalled.
Proof: 
Let B(f) = if f in H 
             then Uncalled 
           else Unknown.
Suppose h in H.
Then C(B)(h) = if h = fm
                 then Unknown
               else if exists j such that forall (g, h, j') in N. j = j'
                                          and forall (g, h) in T. B(g) = j
                 then j
               else Unknown
             = if exists j such that forall (g, h) in T. B(g) = j
                 then j
                 else Unknown
             (because h <> fm and there does not exist (g, h, j) in N)
             = Uncalled
             (because forall (g, h) in T, g in F and B(g) = Uncalled)
             = B(h)
             (because h in H)
Suppose f notin H.
Then C(B)(f) <= Unknown
             (upper bound)
             = B(f) 
             (because f notin H)
Hence, C(B) <= B.
Therefore, lfb(C) <= B (by Fixed-Point Theorem).
Hence, forall h in H. A'(h) = lfb(C)(h) = Uncalled.


Claim: Forall f in Fun, there exists a path from Root to f in G.
Proof: (by contradiction)
Suppose there does not exist a path from Root to f in G.
 By previous claim, forall h in Pr(f). h <> fm
                                   and there does not exist (g, h, j) in N
                                   and forall (g, h) in T. !Path(Root, g)
                                   and forall (g, h) in T, g in Pr(f).
 By previous claim, forall h in Pr(f). A'(h) = Uncalled.
 Hence, A'(f) = Uncalled.
 Therefore, (Root, f) in Edge. 
 But there does not exist a path from Root to f in G. ==><==
Hence, forall f in Fun, there exists a path from Root to f in G.