Call-by-need functions
Robert J. Simmons, Frank Pfenning
This example is derived from Figure 9 in Substructural Operational Semantics as Ordered Logic Programming.
This specification of call-by-need functions is a modification of call-by-name with destinations for binding that enforces that a function argument will be evaluated at most once, and only when it is needed. The rules for evaluating lambdas and applications are the same as in call-by-name with binding, with the exception that the rule eapp2 that returns a function to the application associates the function's argument not with the persistent atomic propostion !bind D2 E2 but with the linear atomic proposition ¡susp D2 E2.
elam : eval(lam λx. E x) ->> return(lam λx. E x).
eapp1 : eval(app E1 E2) ->> comp(app1 E2) • eval(E1).
eapp2 : comp(app1 E2) • return(lam λx. E1' x)
->> ∃D2. eval(E1' D2) • ¡susp D2 E2.
eapp2 : comp(app1 E2) • return(lam λx. E1' x)
->> ∃D2. eval(E1' D2) • ¡susp D2 E2.
The real interesting action happens with binding.
evar1 : eval(D) • ¡susp D E ->> comp(bind1 D) • eval(E).
evar2 : comp(bind1 D) • return(V) ->> return(V) • !bind D V.
evar3 : eval(D) • !bind D V ->> return(V).
evar2 : comp(bind1 D) • return(V) ->> return(V) • !bind D V.
evar3 : eval(D) • !bind D V ->> return(V).
Evaluation examples
We first show the evaluation of the simple term (λx.x)((λy.y)(λz.z)), which evaluates to a value in 11 steps.
%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))
¡susp d6 (app (lam(λy. y)) (lam(λz. c)))•eval(d6)
comp(bind1(d6))•eval(app (lam(λy. y)) (lam(λz. c)))
comp(bind1(d6))•comp(app1(lam(λz. c)))•eval(lam(λy. y))
comp(bind1(d6))•comp(app1(lam(λz. c)))•return(lam(λx. x))
¡susp d7 (lam(λz. c))•comp(bind1(d6))•eval(d7)
comp(bind1(d6))•comp(bind1(d7))•eval(lam(λz. c))
comp(bind1(d6))•comp(bind1(d7))•return(lam(λx. c))
!bind d7 (lam(λx. c))•comp(bind1(d6))•return(lam(λx. c))
!bind d6 (lam(λx. c))•!bind d7 (lam(λx. c))•return(lam(λx. c))
Call-by-need has a particular interesting behavior: some non-termination that happens due to recursion can be detected at runtime! The particular type of non-termination
%trace * eval (app (lam λx. app x x) (app (lam λy.y) (lam λz.z))).
eval(app (lam(λx. app x x)) (app (lam(λy. y)) (lam(λz. z))))
comp(app1(app (lam(λy. y)) (lam(λz. z))))•eval(lam(λx. app x x))
comp(app1(app (lam(λy. y)) (lam(λz. z))))•return(lam(λx. app x x))
¡susp d8 (app (lam(λy. y)) (lam(λz. z)))•eval(app d8 d8)
¡susp d8 (app (lam(λy. y)) (lam(λz. z)))•comp(app1(d8))•eval(d8)
comp(app1(d8))•comp(bind1(d8))•eval(app (lam(λy. y)) (lam(λz. z)))
comp(app1(d8))•comp(bind1(d8))•comp(app1(lam(λz. z)))•eval(lam(λy. y))
comp(app1(d8))•comp(bind1(d8))•comp(app1(lam(λz. z)))•return(lam(λx. x))
¡susp d9 (lam(λz. z))•comp(app1(d8))•comp(bind1(d8))•eval(d9)
comp(app1(d8))•comp(bind1(d8))•comp(bind1(d9))•eval(lam(λz. z))
comp(app1(d8))•comp(bind1(d8))•comp(bind1(d9))•return(lam(λx. x))
!bind d9 (lam(λx. x))•comp(app1(d8))•comp(bind1(d8))•return(lam(λx. x))
!bind d8 (lam(λx. x))•!bind d9 (lam(λx. x))•comp(app1(d8))•return(lam(λx. x))
!bind d8 (lam(λx. x))•!bind d9 (lam(λx. x))•¡susp d10 d8•eval(d10)
!bind d8 (lam(λx. x))•!bind d9 (lam(λx. x))•comp(bind1(d10))•eval(d8)
!bind d8 (lam(λx. x))•!bind d9 (lam(λx. x))•comp(bind1(d10))•return(lam(λx. x))
!bind d10 (lam(λx. x))•!bind d8 (lam(λx. x))•!bind d9 (lam(λx. x))•return(lam(λx. x))
%trace 10 eval(
app (app
(lam λf . app (lam λx . app f (app x x)) (lam λx. app f (app x x)))
(lam λx. x))
unknown).
app (app
(lam λf . app (lam λx . app f (app x x)) (lam λx. app f (app x x)))
(lam λx. x))
unknown).
eval(app (app (lam(λf. app (lam(λx. app f (app x x))) (lam(λx. app f (app x x))))) (lam(λx. x))) unknown)
comp(app1(unknown))•eval(app (lam(λf. app (lam(λx. app f (app x x))) (lam(λx. app f (app x x))))) (lam(λx. x)))
comp(app1(unknown))•comp(app1(lam(λx. x)))•eval(lam(λf. app (lam(λx. app f (app x x))) (lam(λx. app f (app x x)))))
comp(app1(unknown))•comp(app1(lam(λx. x)))•return(lam(λx. app (lam(λx1. app x (app x1 x1))) (lam(λx1. app x (app x1 x1)))))
¡susp d11 (lam(λx. x))•comp(app1(unknown))•eval(app (lam(λx. app d11 (app x x))) (lam(λx. app d11 (app x x))))
¡susp d11 (lam(λx. x))•comp(app1(unknown))•comp(app1(lam(λx. app d11 (app x x))))•eval(lam(λx. app d11 (app x x)))
¡susp d11 (lam(λx. x))•comp(app1(unknown))•comp(app1(lam(λx. app d11 (app x x))))•return(lam(λx. app d11 (app x x)))
¡susp d12 (lam(λx. app d11 (app x x)))•¡susp d11 (lam(λx. x))•comp(app1(unknown))•eval(app d11 (app d12 d12))
¡susp d12 (lam(λx. app d11 (app x x)))•¡susp d11 (lam(λx. x))•comp(app1(unknown))•comp(app1(app d12 d12))•eval(d11)
¡susp d12 (lam(λx. app d11 (app x x)))•comp(app1(unknown))•comp(app1(app d12 d12))•comp(bind1(d11))•eval(lam(λx. x))
¡susp d12 (lam(λx. app d11 (app x x)))•comp(app1(unknown))•comp(app1(app d12 d12))•comp(bind1(d11))•return(lam(λx. x))
%trace 13 eval(app (lam λx. app x x) (lam λy. app y y)).
eval(app (lam(λx. app x x)) (lam(λy. app y y)))
comp(app1(lam(λy. app y y)))•eval(lam(λx. app x x))
comp(app1(lam(λy. app y y)))•return(lam(λx. app x x))
¡susp d13 (lam(λy. app y y))•eval(app d13 d13)
¡susp d13 (lam(λy. app y y))•comp(app1(d13))•eval(d13)
comp(app1(d13))•comp(bind1(d13))•eval(lam(λy. app y y))
comp(app1(d13))•comp(bind1(d13))•return(lam(λx. app x x))
!bind d13 (lam(λx. app x x))•comp(app1(d13))•return(lam(λx. app x x))
!bind d13 (lam(λx. app x x))•¡susp d14 d13•eval(app d14 d14)
!bind d13 (lam(λx. app x x))•¡susp d14 d13•comp(app1(d14))•eval(d14)
!bind d13 (lam(λx. app x x))•comp(app1(d14))•comp(bind1(d14))•eval(d13)
!bind d13 (lam(λx. app x x))•comp(app1(d14))•comp(bind1(d14))•return(lam(λx. app x x))
!bind d14 (lam(λx. app x x))•!bind d13 (lam(λx. app x x))•comp(app1(d14))•return(lam(λx. app x x))
!bind d14 (lam(λx. app x x))•!bind d13 (lam(λx. app x x))•¡susp d15 d14•eval(app d15 d15)