Tiny Ollibot Example Server - Call-by-need functions

Parallel evaluation for pairs

Robert J. Simmons, Frank Pfenning

This example is derived from Figure 5 in Substructural Operational Semantics as Ordered Logic Programming.

Parallel evaluation for pairs, plus unit

eunit : eval(unit) ->> return unit.

epair1 : eval(pair E1 E2) ->> comp(pair1) • eval(E1) • eval(E2).
epair2 : comp(pair1) • return(V1) • return(V2) ->> return(pair V1 V2).

elet1 : eval(split E (λx1.λx2. E' x1 x2)) ->> comp(split1 E') • eval(E).
elet2 : eval(split1 (λx1.λx2. E' x1 x2)) • return(pair V1 V2) ->> eval(E' V1 V2).

Example traces

The is no real computation to do in the language fragment described here; however, the fact way in which the evaluation of pairs produces multiple active eval predicates is apparent.

These traces also reveal something about the fact that the underlying operational semantics of the programming language we have implemented works; the interpreter attempts to apply rules starting at the left-hand side of the context and working towards the right-hand side. This means that, in this example, the left half of the pair is always evaluated first.

%trace * eval(pair unit (pair unit unit)).
eval(pair unit (pair unit unit))
comp(pair1)eval(unit)eval(pair unit unit)
comp(pair1)return(unit)eval(pair unit unit)
comp(pair1)return(unit)comp(pair1)eval(unit)eval(unit)
comp(pair1)return(unit)comp(pair1)return(unit)eval(unit)
comp(pair1)return(unit)comp(pair1)return(unit)return(unit)
comp(pair1)return(unit)return(pair unit unit)
return(pair unit (pair unit unit))
%trace * eval(pair (pair unit unit) (pair unit unit)).
eval(pair (pair unit unit) (pair unit unit))
comp(pair1)eval(pair unit unit)eval(pair unit unit)
comp(pair1)comp(pair1)eval(unit)eval(unit)eval(pair unit unit)
comp(pair1)comp(pair1)return(unit)eval(unit)eval(pair unit unit)
comp(pair1)comp(pair1)return(unit)return(unit)eval(pair unit unit)
comp(pair1)return(pair unit unit)eval(pair unit unit)
comp(pair1)return(pair unit unit)comp(pair1)eval(unit)eval(unit)
comp(pair1)return(pair unit unit)comp(pair1)return(unit)eval(unit)
comp(pair1)return(pair unit unit)comp(pair1)return(unit)return(unit)
comp(pair1)return(pair unit unit)return(pair unit unit)
return(pair (pair unit unit) (pair unit unit))