[Prev][Next][Index][Thread]

CPS-conversion and reasoning


You are asking a good question about the "origin" of the context that
distinguishes the terms in the counterexample.  For those who are
listening to the conversation, the terms in the counterexample are
(once again)
    M1 = \a.\b.\c. (\x. (b a) x) (c a)
    M2 = \a.\b.\c. (b a) (c a)
The context that distinguishes their cps-versions is
    C[ ] = [ ] c0
    c0   = \f. f 1 c1
    c1   = \g. g (\x.\y.1) c2
    c2   = \h. h (\x.\y.Omega) (\x.x)

Fortunately for those using the cps-conversion algorithm, the above
context CANNOT come from the transform of some context; more precisely,
(see end of this note for a proof)
REMARK:  The above context cannot equal "cps(D[ ]) (\x.x)"  for any context
         D[ ].

I don't agree completely with your assessment (correct me if I
misparaphrase you) that there are practically no optimizations one can
make on cps-terms: certain optimizations are "safe," namely beta
conversions and probably others.  But many optimizations, as you point
out, are not safe when one uses traditional observational congruence
reasoning to verify them.

Should we then abandon attempts to optimize cps-converted code?  I don't
believe so; in light of Fischer's result, namely
       Eval(M) = c   iff   Eval(cps(M) (\x.x)) = c
optimizations may be "safe" as long as we consider only CONTINUIZED
contexts.  The question is, what is a continuized context?  We don't
want to restrict ourselves to only those contexts that pattern-match
some continuized context, for we may wish to perform optimizations on
the contexts themselves.

There seems to be some intuition about the continuations that get
passed to cps'ed terms---the challenge, I feel, is to make this
intuition formal (if possible), and so verify that certain
optimizations are really safe.  We may not get around your problem
with overflows, but we do avoid reasoning in the "worst case"---
namely, reasoning that the code will do things that it cannot do in
continuized contexts.

Finally, here is the proof of the above remark:
PROOF:  Suppose, by way of contradiction, that C[ ] = cps(D[ ]) (\x.x).
We then conclude that, by Fischer's result,
       Eval(D[M1]) = c   iff   Eval(cps(D[M1]) (\x.x)) = c,
       Eval(D[M2]) = c   iff   Eval(cps(D[M2]) (\x.x)) = c.
Since M1 and M2 are observationally congruent, 
       Eval(cps(D[M1]) (\x.x)) = c  iff  Eval(cps(D[M2]) (\x.x)) = c,
a contradiction since 
       cps(D[M1]) (\x.x) = C[cps(M1)] diverges and 
       cps(D[M2]) (\x.x) = C[cps(M2)] converges.
END-OF-PROOF.


-Jon