transformation correctness

[Matthew Fluet]

> It would be nice to have something about correctness (and type correctness) of
> the transformation, but I haven't thought about it enough to feel comfortable
> saying anything.

I don't know about type correctness, but I wanted to say something about
correctness.  I'd want to say something along the lines of the following,
which might not be totally true, but that's the intuition I want.

The correctness of the contification transformation can be argued by
noting that for each transition in the original program

<exp,rho,kappa> -> <exp',rho',kappa'>

there are one or more transitions in the transformed program

<Texp,Trho,Tkappa> ->+ <Texp',Trho',Tkappa'>

where rho \subset Trho and rho' \subset Trho', Tkappa is a tail of kappa
and Tkappa' is a tail of kappa', and exp ~= Texp and exp' ~= Texp',
where ~= means equal except possibly in transfer possitions and rhs might
have more cont declarations.  (The more cont declarations is the reason
the transformed program might need more than one step to match a step in
the untransformed program.)

The relations between rho's and Trho's and between kappa's and Tkappa's
captures the result of contification: the program can make more steps
without building up frames.

This reminds me of something else: should we say anything about the
intial and terminal states of the CPS operational semantics.