[TYPES] Operational Semantics Preserving Translations

[M.C.A. (Marco) Devillers]

I am looking for operational semantics preserving translations
regarding eager and lazily evaluated LC, where operational semantics
is purely defined on the side effects during the evaluation of a term.
I assume this shouldn't be too hard since one may assume these
functions exists since lambda evaluators can be written for each LC
with a certain operational semantics in each LC with a certain
semantics. At least, I hope I am correct in assuming so.

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

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

Note that * is a sequence of terms. An example term: (\x. \y. call (+) x y) 2 3.

I define the operational semantics of a term as 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.

What I am looking for are translation functions between lambda terms
of given form which map a lambda term given a certain rewrite strategy
to an operationally equivalent lambda term given another rewrite
strategy. I.e. say l makes a number of calls when lazily evaluated,
then I am looking for a translation function which gives a term l'
which, when evaluated eagerly, makes exactly the same calls in exactly
the same order. Of course, I am hoping for a linear translation.

Strangely, this is an opposing view to normal operational semantics of
LC, where that is usually viewed as a mapping into a resulting value,
where I, as a compiler writer, am mostly interested in what a term
sequentially does to a system, and have hardly any interest in the
resulting term.

Rationale, with some hand waving: say you want a compiler for an
(impure) variant of Haskel but you only have a Lisp compiler. Given an
operational semantics preserving translation f, one could translate
Haskell to a 'lazy' LC term l, translate that to an 'eager' LC term
f(l), and translate that f(l) to Lisp.

Thanks anyway, best wishes and a merry Christmas, Marco