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