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).
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.
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 d21•eval(d21)
¡susp d21 d21•comp(bind1(d21))•eval(d21)
¡susp d21 d21•comp(bind1(d21))•comp(bind1(d21))•eval(d21)
¡susp d21 d21•comp(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) d22•eval(app (lam(λy. y)) d22)
¡susp (app (lam(λy. y)) d22) d22•comp(app1(d22))•eval(lam(λy. y))
¡susp (app (lam(λy. y)) d22) d22•comp(app1(d22))•return(lam(λx. x))
¡susp (app (lam(λy. y)) d22) d22•comp(app2(lam(λx. x)))•eval(d22)
¡susp (app (lam(λy. y)) d22) d22•comp(app2(lam(λx. x)))•comp(bind1(d22))•eval(app (lam(λy. y)) d22)
¡susp (app (lam(λy. y)) d22) d22•comp(app2(lam(λx. x)))•comp(bind1(d22))•comp(app1(d22))•eval(lam(λy. y))
¡susp (app (lam(λy. y)) d22) d22•comp(app2(lam(λx. x)))•comp(bind1(d22))•comp(app1(d22))•return(lam(λx. x))
¡susp (app (lam(λy. y)) d22) d22•comp(app2(lam(λx. x)))•comp(bind1(d22))•comp(app2(lam(λx. x)))•eval(d22)
¡susp (app (lam(λy. y)) d22) d22•comp(app2(lam(λx. x)))•comp(bind1(d22))•comp(app2(lam(λx. x)))•comp(bind1(d22))•eval(app (lam(λy. y)) d22)