Rephrasing Thunks

Assume a lambda calculus with side effects/impure function calls:

   M ::= c | v | \v . M | (M M) | call c

An example term: (\x. \y. call (+) x y) 2 3.

The operational semantics of a term is the series of calls made to the system during the evaluation under a certain rewrite strategy. Two terms evaluated under two rewrite strategies are considered operationally equal if they made exactly the same calls in exactly the same order.

The standard naive technique for transforming a call-by-need term to a call-by-value term is called thunkification:

1. An abstraction \x.e translates into \x.T(e);
2. An application (e1 e2) translates into T(e1)(\x.T(e2 )), where x is a fresh variable.
   That is, the evaluation of the argument is suspended (thunkified);
3. A variable x translates into (x d) (where d is a dummy argument)
   Thus, x is bound to a suspension and x must be dethunkified.

I suspect that for this impure calculus, it is sufficient to thunkify lazy terms and optimize the corresponding term according to partial evaluation under a call-by-value semantics. Possibly, arguments to calls can be fully reduced by just supplying them their dummy argument, forcing evaluation. That would make strictness analysis superfluous, I wonder what I missed here?

It seems trivial, but it probably isn't. I have the feeling that there is a generalizing pattern if you would supply operational semantics preserving functions between the two/four mostly known reduction strategies, with the addendum that for impure LC, you might need to 'patch' rewriting such that all calls receive fully reduced terms to mimic behaviour of 'real' down-to-earth programming languages, or assume all calls receive constants as arguments. Of course, translating call-by-need to call-by-value is the most obviously wanted function, but it might be worth it to study and prove correct those other semantic preserving functions in order to gain some better understanding in rewrite semantics for impure LC.

References:

1. Paul Steckler, Mitchell Wand, Selective Thunkification, Proceedings of the 1st International Static Analysis Symposium. 1994.
   ftp://ftp.ccs.neu.edu/pub/people/steck/sas94.ps.
2. Torben Amtoft, Minimal Thunkification, Proceedings of the Third International Workshop on Static Analysis WSA'93, volume 724 of Lecture Notes in Computer Science. 1993.
   http://www.daimi.aau.dk/~tamtoft/Papers/WSA93.ps.Z
   http://www.cis.ksu.edu/~tamtoft/Papers/Amt:MT-1993
3. Alan Mycroft, The theory of transforming call-by-need to call-by-value. International Symposium on Programming, Paris. 1980.