Call-by-need suspensions with a fixed point
Robert J. Simmons
This examples is derived from Figure 3 in Substructural Operational Semantics as Ordered Logic Programming.
This file describes the stuck behavior from the "black hole" when the
call-by-need specification is straightforwardly extended to a fixed point
operator. Two ways of dealing with this stuckness are
nontermination and
raising an error.
Call-by-value functions
elam : eval(lam λx. E x) ->> return(lam E).
eapp1 : eval(app E1 E2) ->> comp(app1 E2) • eval(E1).
eapp2 : comp(app1 E2) • return(V1) ->> comp(app2 V1) • eval(E2).
eapp3 : comp(app2 (lam λx.E0 x)) • return(V2) ->> eval(E0 V2).
Fixed point recursion (call-by-need)
efix : eval(fix λx. E x) ->> ∃D. eval(E D) • ¡susp (E D) D.
esusp : eval(D) • ¡susp E D ->> comp(bind1 D) • eval E.
ebind : comp(bind1 D) • return(V) ->> return(V) • !bind V D.
evar : eval(D) • !bind V D ->> return V.
Example traces
This is fix(x.x), which you can't write in ML, but which falls into the
limited set of expressions that "falls into a black hole" - evaluation gets
stuck when a destination is reached that is currently associated with
neither a susp nor a bind.
%trace * eval(fix λx. x).
eval(fix(λx. x))
¡susp d16 d16•eval(d16)
comp(bind1(d16))•eval(d16)
This is a slightly more complicated expression that you also can't write
in ML. It also falls into a black hole.
%trace * eval(fix λx. app (lam λy. y) x).
eval(fix(λx. app (lam(λy. y)) x))
¡susp (app (lam(λy. y)) d17) d17•eval(app (lam(λy. y)) d17)
¡susp (app (lam(λy. y)) d17) d17•comp(app1(d17))•eval(lam(λy. y))
¡susp (app (lam(λy. y)) d17) d17•comp(app1(d17))•return(lam(λx. x))
¡susp (app (lam(λy. y)) d17) d17•comp(app2(lam(λx. x)))•eval(d17)
comp(app2(lam(λx. x)))•comp(bind1(d17))•eval(app (lam(λy. y)) d17)
comp(app2(lam(λx. x)))•comp(bind1(d17))•comp(app1(d17))•eval(lam(λy. y))
comp(app2(lam(λx. x)))•comp(bind1(d17))•comp(app1(d17))•return(lam(λx. x))
comp(app2(lam(λx. x)))•comp(bind1(d17))•comp(app2(lam(λx. x)))•eval(d17)
This is fix(f.λx.f x), which you can (more or less) write in ML as
fun f x = f x, applied to the identity function.
It goes into an infinite loop instead of triggering the black hole;
it is easy to see that the last state is identical to the fifth-from-last
state; the trace would go forever if it was not ended by the 18 passed
as an argument to %trace.
%trace 18 eval(app (fix λf. lam λx. app f x) (lam λz.z)).
eval(app (fix(λf. lam(λx. app f x))) (lam(λz. z)))
comp(app1(lam(λz. z)))•eval(fix(λf. lam(λx. app f x)))
¡susp (lam(λx. app d18 x)) d18•comp(app1(lam(λz. z)))•eval(lam(λx. app d18 x))
¡susp (lam(λx. app d18 x)) d18•comp(app1(lam(λz. z)))•return(lam(λx. app d18 x))
¡susp (lam(λx. app d18 x)) d18•comp(app2(lam(λx. app d18 x)))•eval(lam(λz. z))
¡susp (lam(λx. app d18 x)) d18•comp(app2(lam(λx. app d18 x)))•return(lam(λx. x))
¡susp (lam(λx. app d18 x)) d18•eval(app d18 (lam(λx. x)))
¡susp (lam(λx. app d18 x)) d18•comp(app1(lam(λx. x)))•eval(d18)
comp(app1(lam(λx. x)))•comp(bind1(d18))•eval(lam(λx. app d18 x))
comp(app1(lam(λx. x)))•comp(bind1(d18))•return(lam(λx. app d18 x))
!bind (lam(λx. app d18 x)) d18•comp(app1(lam(λx. x)))•return(lam(λx. app d18 x))
!bind (lam(λx. app d18 x)) d18•comp(app2(lam(λx. app d18 x)))•eval(lam(λx. x))
!bind (lam(λx. app d18 x)) d18•comp(app2(lam(λx. app d18 x)))•return(lam(λx. x))
!bind (lam(λx. app d18 x)) d18•eval(app d18 (lam(λx. x)))
!bind (lam(λx. app d18 x)) d18•comp(app1(lam(λx. x)))•eval(d18)
!bind (lam(λx. app d18 x)) d18•comp(app1(lam(λx. x)))•return(lam(λx. app d18 x))
!bind (lam(λx. app d18 x)) d18•comp(app2(lam(λx. app d18 x)))•eval(lam(λx. x))
!bind (lam(λx. app d18 x)) d18•comp(app2(lam(λx. app d18 x)))•return(lam(λx. x))
!bind (lam(λx. app d18 x)) d18•eval(app d18 (lam(λx. x)))