Mutable storage
Robert J. Simmons, Frank Pfenning
This examples is derived from Figures 3 and 4 in Substructural Operational Semantics as Ordered Logic Programming.
Call-by-value functions
vlam : 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(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).
Mutable storage
eref1 : eval(ref E) ->> comp(ref1) • eval(E).
eref2 : comp(ref1) • return(V) ->> ∃D. return(loc D) • ¡cell D V.
eget1 : eval(get E) ->> comp(get1) • eval(E).
eget2 : comp(get1) • return(loc D) • ¡cell D V ->> return(V) • ¡cell D V.
eset1 : eval(set E1 E2) ->> comp(set1 E2) • eval(E1).
eset2 : comp(set1 E2) • return(V1) ->> comp(set2 V1) • eval(E2).
eset3 : comp(set2 (loc D)) • return(V2) • ¡cell D V ->> return(V2) • ¡cell D V2.
vloc : eval(loc D) ->> return(loc D).
eref2 : comp(ref1) • return(V) ->> ∃D. return(loc D) • ¡cell D V.
eget1 : eval(get E) ->> comp(get1) • eval(E).
eget2 : comp(get1) • return(loc D) • ¡cell D V ->> return(V) • ¡cell D V.
eset1 : eval(set E1 E2) ->> comp(set1 E2) • eval(E1).
eset2 : comp(set1 E2) • return(V1) ->> comp(set2 V1) • eval(E2).
eset3 : comp(set2 (loc D)) • return(V2) • ¡cell D V ->> return(V2) • ¡cell D V2.
vloc : eval(loc D) ->> return(loc D).
Example trace
%trace * eval (set (ref (lam λx. lam λy. y)) (lam λx. lam λy. x)).
eval(set (ref(lam(λx. lam(λy. y)))) (lam(λx. lam(λy. x))))
comp(set1(lam(λx. lam(λy. x))))•eval(ref(lam(λx. lam(λy. y))))
comp(set1(lam(λx. lam(λy. x))))•comp(ref1)•eval(lam(λx. lam(λy. y)))
comp(set1(lam(λx. lam(λy. x))))•comp(ref1)•return(lam(λx. lam(λy. y)))
¡cell d1 (lam(λx. lam(λy. y)))•comp(set1(lam(λx. lam(λy. x))))•return(loc(d1))
¡cell d1 (lam(λx. lam(λy. y)))•comp(set2(loc(d1)))•eval(lam(λx. lam(λy. x)))
¡cell d1 (lam(λx. lam(λy. y)))•comp(set2(loc(d1)))•return(lam(λx. lam(λy. x)))
¡cell d1 (lam(λx. lam(λy. x)))•return(lam(λx. lam(λy. x)))