*LCi*) with side effects/impure function calls:

Note that * is a sequence of terms.LCi ::= c | v | \v . LCi | (LCi LCi) | call LCi*

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+, returned5, and the whole program reduces to5.

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

I.e., operational semantics preserving functions between eager and lazily evaluated impure LC terms where = is the alpha equivalence on series of terms.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)).

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

Moreover:

- 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. - 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.

## No comments:

## Post a Comment