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 is a modification of cbneed-fix.olf that restores the susp when the value at a destination is first required; the only purpose for doing so is that cetrain traces that would become stuck in the specification from cbneed-fix.olf will ("correctly") fail to terminate here.

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 • ¡susp E D.
ebind : comp(bind1 D) • return(V) • ¡susp E D ->> return(V) • !bind V D.
evar  : eval(D) • !bind V D ->> return V.

Example traces

Both examples appeared in cbneed-fix.olf, where they got stuck. Here they fail to terminate, leaving multiple comp(bind1 D) frames on the stack for the same destination D.

%trace 4 eval(fix λx. x).
eval(fix(λx. x))
¡susp d21 d21eval(d21)
¡susp d21 d21comp(bind1(d21))eval(d21)
¡susp d21 d21comp(bind1(d21))comp(bind1(d21))eval(d21)
¡susp d21 d21comp(bind1(d21))comp(bind1(d21))comp(bind1(d21))eval(d21)
%trace 9 eval(fix λx. app (lam λy. y) x).
eval(fix(λx. app (lam(λy. y)) x))
¡susp (app (lam(λy. y)) d22) d22eval(app (lam(λy. y)) d22)
¡susp (app (lam(λy. y)) d22) d22comp(app1(d22))eval(lam(λy. y))
¡susp (app (lam(λy. y)) d22) d22comp(app1(d22))return(lam(λx. x))
¡susp (app (lam(λy. y)) d22) d22comp(app2(lam(λx. x)))eval(d22)
¡susp (app (lam(λy. y)) d22) d22comp(app2(lam(λx. x)))comp(bind1(d22))eval(app (lam(λy. y)) d22)
¡susp (app (lam(λy. y)) d22) d22comp(app2(lam(λx. x)))comp(bind1(d22))comp(app1(d22))eval(lam(λy. y))
¡susp (app (lam(λy. y)) d22) d22comp(app2(lam(λx. x)))comp(bind1(d22))comp(app1(d22))return(lam(λx. x))
¡susp (app (lam(λy. y)) d22) d22comp(app2(lam(λx. x)))comp(bind1(d22))comp(app2(lam(λx. x)))eval(d22)
¡susp (app (lam(λy. y)) d22) d22comp(app2(lam(λx. x)))comp(bind1(d22))comp(app2(lam(λx. x)))comp(bind1(d22))eval(app (lam(λy. y)) d22)