Operational Semantics Preserving Translations

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

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

Note that * is a sequence of terms.

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

A call models an impure/non-referentially transparent system call. For simplicity, we assume that if two programs are run, and they have made identical calls, that any two new identical calls will return identical results.

I.e.: if two programs made (precisely) two calls to some function "tick" resulting in values 1 and 2, then the third call to tick will return the same value.

Assume the functions EAGER and LAZY, eager and lazy operational semantics for closed terms in LCi, respectively. They both map an LCi term into a value of type (LCi := call LCi*)* LCi, the collection of made calls in temporal order followed, possibly, by the term in strong normal form - fully reduced. I'll handwave termination concerns away for the time being. EAGER and LAZY are called the operational semantics since it tracks the system calls made and returns the evaluated term, if any. Note that I assume that a call only accepts an LCi term in strong normal form (fully reduced), and returns a term in strong normal form.

Examples:

EAGER((\x. \y. call (+) x y) 2 3) = (5 := call 2 3), 5.
During the evaluation of the term we made one call to +, returned 5, and the whole program reduces to 5.

and

EAGER( (\x . call tick) (call tick) ) = (1 := call tick), (2 := call tick), 2.
Two calls to tick returned constants 1 and 2, the whole program reduces to 2.

moreover

LAZY ( (\x. call (+) 2 3) (call tick) ) = (5 := call 2 3), 5.

whereas

EAGER ( (\x. call (+) 2 3) (call tick) ) = (1 := call tick), (5 := call 2 3), 5.

Two terms are assumed to be operationally equal if they made exactly the same systems calls in temporal order, and possibly reduce to the same term, BUT two identical terms may return a similar result under the two impure operational semantics, but are not equal since they didn't make the same series of system calls.

Needed: two functions e_to_l and l_to_e such that

EAGER(l) = LAZY(e_to_l l),
LAZY(l) = EAGER(l_to_e l), 
EAGER(l) = EAGER(l_to_e(e_to_l l)), and  
LAZY(l) = LAZY(e_to_l (l_to_e l)).

I.e., operational semantics preserving functions between eager and lazily evaluated impure LC terms where = is the alpha equivalence on series of terms.

Rationale: I want to implement some lazy features in Hi, this seems to be one good solution.

Moreover:

1. Say you would like to implement a Haskell compiler but you only have a Lisp compiler. Solution: translate Haskell to a corresponding LCi term l, translate that term to l' = l_to_e l, translate l' to Lisp. Hereby solving the problem once and for all.
2. Say you want to have eager semantics in Haskell. That could be done similarly with the e_to_l function.

I didn't think it through too much, a simple CPS transform probably doesn't do it, but may be a good starting point.

Funny thing is that this is a totally opposing view to normal interpretations of operational semantics of LC since I am only interested in observational equivalence with respect to side effects. Which makes sense for someone who builds compilers since the only interesting quality of a program is what it does to the system and the result is often uninteresting.