Tiny Ollibot Example Server - Call-by-need functions

Problems with combining parallel evaluation and exceptions

Robert J. Simmons, Frank Pfenning

These examples are derived from Figures 5 and 10 in Substructural Operational Semantics as Ordered Logic Programming.

Exceptions as presented in the paper rely on a global property of the operational semantics, essentially that there is only one control stack per process. However, the parallel evaluation of pairs creates multiple control stacks that are related by juxtoposition in the ordered context. Therefore, the two cannot be combined without problems, as demonstrated in this example.

One possibility for addressing this problem is given in par-exn2.olf.

Parallel evaluation for pairs (Figure 5), 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).

Exceptions (Figure 10)

etry   : eval(try E1 E2) ->> catch(E2) • eval(E1).
eraise : eval(raise) ->> fail.
epop   : comp(F) • fail ->> fail.
ecatch : catch(E2) • fail ->> eval(E2).
eret   : catch(E2) • return(V) ->> return(V).

If there is an exception in the first branch of a pair's evaluation, then the error will "abandon" the stack belonging to the second branch, eagerly propogating the error before the second branch has even necessarily finished evaluating.

%trace * eval(try (pair raise (pair unit unit)) unit).
eval(try (pair raise (pair unit unit)) unit)
catch(unit)eval(pair raise (pair unit unit))
catch(unit)comp(pair1)eval(raise)eval(pair unit unit)
catch(unit)comp(pair1)faileval(pair unit unit)
catch(unit)faileval(pair unit unit)
eval(unit)eval(pair unit unit)
return(unit)eval(pair unit unit)
return(unit)return(pair unit unit)

If there is an exception in the second branch, it will be "blocked" by the return in the first branch and execution will become stuck.

%trace * eval(try (pair (pair unit unit) raise) unit).
eval(try (pair (pair unit unit) raise) unit)
catch(unit)eval(pair (pair unit unit) raise)
catch(unit)comp(pair1)eval(pair unit unit)eval(raise)
catch(unit)comp(pair1)return(pair unit unit)eval(raise)
catch(unit)comp(pair1)return(pair unit unit)fail