Call-by-name functions
Robert J. Simmons, Frank Pfenning
This examples is derived from Figure 7 in Substructural Operational Semantics as Ordered Logic Programming.
Call-by-name 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(lam (λx. E1' x)) ->> eval(E1' E2).
r2 : eval(app E1 E2) ->> comp(app1 E2) • eval(E1).
r3 : comp(app1 E2) • return(lam (λx. E1' x)) ->> eval(E1' E2).
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))
eval(app (lam(λy. y)) (lam(λz. c)))
comp(app1(lam(λz. c)))•eval(lam(λy. y))
comp(app1(lam(λz. c)))•return(lam(λx. x))
eval(lam(λz. c))
return(lam(λx. c))