Call-by-name functions with destinations for binding
Robert J. Simmons, Frank Pfenning
This examples is derived from Figure 8 in Substructural Operational Semantics as Ordered Logic Programming.
Call-by-name functions with destinations for binding
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) ->> ∃D2. eval(E1' D2) • !bind D2 E2.
r4 : eval(D) • !bind D E ->> eval(E).
r2 : eval(app E1 E2) ->> comp(app1 E2) • eval(E1).
r3 : comp(app1 E2) • return(lam λx. E1' x) ->> ∃D2. eval(E1' D2) • !bind D2 E2.
r4 : eval(D) • !bind D E ->> eval(E).
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))
!bind d4 (app (lam(λy. y)) (lam(λz. c)))•eval(d4)
!bind d4 (app (lam(λy. y)) (lam(λz. c)))•eval(app (lam(λy. y)) (lam(λz. c)))
!bind d4 (app (lam(λy. y)) (lam(λz. c)))•comp(app1(lam(λz. c)))•eval(lam(λy. y))
!bind d4 (app (lam(λy. y)) (lam(λz. c)))•comp(app1(lam(λz. c)))•return(lam(λx. x))
!bind d5 (lam(λz. c))•!bind d4 (app (lam(λy. y)) (lam(λz. c)))•eval(d5)
!bind d5 (lam(λz. c))•!bind d4 (app (lam(λy. y)) (lam(λz. c)))•eval(lam(λz. c))
!bind d5 (lam(λz. c))•!bind d4 (app (lam(λy. y)) (lam(λz. c)))•return(lam(λx. c))