Tiny Ollibot Example Server - Call-by-need functions

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 d16eval(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) d17eval(app (lam(λy. y)) d17)
¡susp (app (lam(λy. y)) d17) d17comp(app1(d17))eval(lam(λy. y))
¡susp (app (lam(λy. y)) d17) d17comp(app1(d17))return(lam(λx. x))
¡susp (app (lam(λy. y)) d17) d17comp(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)) d18comp(app1(lam(λz. z)))eval(lam(λx. app d18 x))
¡susp (lam(λx. app d18 x)) d18comp(app1(lam(λz. z)))return(lam(λx. app d18 x))
¡susp (lam(λx. app d18 x)) d18comp(app2(lam(λx. app d18 x)))eval(lam(λz. z))
¡susp (lam(λx. app d18 x)) d18comp(app2(lam(λx. app d18 x)))return(lam(λx. x))
¡susp (lam(λx. app d18 x)) d18eval(app d18 (lam(λx. x)))
¡susp (lam(λx. app d18 x)) d18comp(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)) d18comp(app1(lam(λx. x)))return(lam(λx. app d18 x))
!bind (lam(λx. app d18 x)) d18comp(app2(lam(λx. app d18 x)))eval(lam(λx. x))
!bind (lam(λx. app d18 x)) d18comp(app2(lam(λx. app d18 x)))return(lam(λx. x))
!bind (lam(λx. app d18 x)) d18eval(app d18 (lam(λx. x)))
!bind (lam(λx. app d18 x)) d18comp(app1(lam(λx. x)))eval(d18)
!bind (lam(λx. app d18 x)) d18comp(app1(lam(λx. x)))return(lam(λx. app d18 x))
!bind (lam(λx. app d18 x)) d18comp(app2(lam(λx. app d18 x)))eval(lam(λx. x))
!bind (lam(λx. app d18 x)) d18comp(app2(lam(λx. app d18 x)))return(lam(λx. x))
!bind (lam(λx. app d18 x)) d18eval(app d18 (lam(λx. x)))