Tiny Ollibot Example Server - Call-by-need functions

Call-by-value functions

Robert J. Simmons, Frank Pfenning

This examples is derived from Figure 3 in Substructural Operational Semantics as Ordered Logic Programming.

Call-by-value functions

r1 : eval(lam λx. E x) ->> return(lam E).
r2 : eval(app E1 E2) ->> comp(app1 E2) • eval(E1).
r3 : comp(app1 E2) • return(V1) ->> comp(app2 V1) • eval(E2).
r4 : comp(app2 (lam λx.E0 x)) • return(V2) ->> eval(E0 V2).

Example trace

%trace * eval(app (lam λx.x) (app (lam λy.y) (lam λz.c))).
eval(app (lam(λx. x)) (app (lam(λy. y)) (lam(λz. c))))
comp(app1(app (lam(λy. y)) (lam(λz. c))))eval(lam(λx. x))
comp(app1(app (lam(λy. y)) (lam(λz. c))))return(lam(λx. x))
comp(app2(lam(λx. x)))eval(app (lam(λy. y)) (lam(λz. c)))
comp(app2(lam(λx. x)))comp(app1(lam(λz. c)))eval(lam(λy. y))
comp(app2(lam(λx. x)))comp(app1(lam(λz. c)))return(lam(λx. x))
comp(app2(lam(λx. x)))comp(app2(lam(λx. x)))eval(lam(λz. c))
comp(app2(lam(λx. x)))comp(app2(lam(λx. x)))return(lam(λx. c))
comp(app2(lam(λx. x)))eval(lam(λx. c))
comp(app2(lam(λx. x)))return(lam(λx. c))
eval(lam(λx. c))
return(lam(λx. c))