Assume a lambda calculus (LCi) with side effects/impure function
calls: LCi = v | \v . LCi | (LCi LCi) | call LCi*. * is a sequence of terms.
An example term: (\x. \y. call (+) x y) 2 3. For convenience, I assume 2 and 3 are lambda encodings of the integers 2 and 3, similarly for +.
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 impure Haskell. That could be done similarly with the e_to_l function.
3. Conversely, you might want to translate Lisp to Haskell.
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.
(Unbelievably all my posts end up on the wrong blog.)
010610: There's an addendum to it. During rewriting, one of the properties I want is that whenever a call is rewritten, all arguments are constants, i.e. normalized.
