Tiny Ollibot Example Server - Call-by-need functions
{- Part 1: Turing machines -}

rR: hR * tR  ->>  hR * t0 * tR.
rL: tL * hL  ->>  tL * t0 * hL.
r1: ¡s1 * t0 * hL  ->>  ¡s2 * t0 * hR.
r2: ¡s1 * hR * t0  ->>  ¡s2 * t0 * hR.
r3: ¡s2 * t1 * hL  ->>  ¡s1 * hL * t0.
r4: ¡s2 * hR * t1  ->>  ¡s1 * hR * t0.

{- Starting with the tape ..... 1 0 [ 1 ] 1 0 1 .... -}
%trace 10 ¡s2 * tL * t1 * t0 * t1 * hL * t1 * t0 * t1 * tR.
{- Part 2: Substructural operational semantics in ordered logic -}

e1: eval (lam λx. M x)  ->>  retn (lam λx. M x).
e2: eval (app M N)  ->>  eval M * cont (app1 N).
e3: retn (lam λx. M x) * cont (app1 N)  ->>  eval (M N).

{- Evaluate (λx.x)(λy.y) to a value -}
%trace * eval (app (lam λx. x) (lam λy. y)).
eval(app (lam(λx. x)) (lam(λy. y)))
eval(lam(λx. x))cont(app1(lam(λy. y)))
retn(lam(λx. x))cont(app1(lam(λy. y)))
eval(lam(λy. y))
retn(lam(λx. x))
{- Evaluate (λx.xx)(λy.yy) for a bit; it diverges -}
%trace 6 eval (app (lam λx. app x x) (lam λy. app y y)).
eval(app (lam(λx. app x x)) (lam(λy. app y y)))
eval(lam(λx. app x x))cont(app1(lam(λy. app y y)))
retn(lam(λx. app x x))cont(app1(lam(λy. app y y)))
eval(app (lam(λy. app y y)) (lam(λy. app y y)))
eval(lam(λy. app y y))cont(app1(lam(λy. app y y)))
retn(lam(λx. app x x))cont(app1(lam(λy. app y y)))
eval(app (lam(λy. app y y)) (lam(λy. app y y)))
{- Part 3: Substructural operational semantics in linear logic -}
 -- We write "leval," "lretn," and "lcont" to differentiate from the previous 
 -- examples

l1: ¡leval (lam λx. M x) D  ->>  ¡lretn (lam λx. M x) D.
l2: ¡leval (app M N) D  ->>  ∃d1. ¡leval M d1 * ¡lcont d1 (app1 N) D.
l3: ¡lretn (lam λx. M x) D1 * ¡lcont D1 (app1 N) D  ->>  ¡leval (M N) D.

{- Evaluate (λx.x)(λy.y) to a value -}
%trace * ¡leval (app (lam λx. x) (lam λy. y)) d.
¡leval (app (lam(λx. x)) (lam(λy. y))) d
¡leval (lam(λx. x)) d1¡lcont d1 (app1(lam(λy. y))) d
¡lretn (lam(λx. x)) d1¡lcont d1 (app1(lam(λy. y))) d
¡leval (lam(λy. y)) d
¡lretn (lam(λx. x)) d
{- Evaluate (λx.xx)(λy.yy) for a bit; it diverges -}
%trace 6 ¡leval (app (lam λx. app x x) (lam λy. app y y)) d.
¡leval (app (lam(λx. app x x)) (lam(λy. app y y))) d
¡leval (lam(λx. app x x)) d2¡lcont d2 (app1(lam(λy. app y y))) d
¡lretn (lam(λx. app x x)) d2¡lcont d2 (app1(lam(λy. app y y))) d
¡leval (app (lam(λy. app y y)) (lam(λy. app y y))) d
¡leval (lam(λy. app y y)) d3¡lcont d3 (app1(lam(λy. app y y))) d
¡lretn (lam(λx. app x x)) d3¡lcont d3 (app1(lam(λy. app y y))) d
¡leval (app (lam(λy. app y y)) (lam(λy. app y y))) d
{- Part 4: Suspending expressions in the persistent context, adding numbers -}
 -- We write "teval" and "tretn" to differentiate from the previous examples
 -- To encode the linear lambda calculus, we could have used ¡thunk M X
 -- instead of !thunk M X

t1: teval (lam λx. M x)  ->>  tretn (lam λx. M x).
t2: teval (app M N)  ->>  teval M * cont (app1 N).
t3: tretn (lam λx. M x) * cont (app1 N)  ->>  ∃x. teval (M x) * !thunk N x.
t4: teval X * !thunk M X  ->>  teval M.

 -- We'll extend this one with numbers
t5: teval (num N)  ->>  tretn (num N).
t7: teval (plus M N)  ->>  teval M * cont (plus1 N).
t6: tretn (num V) * cont (plus1 N)  ->>  teval N * cont (plus2 V).
t9: tretn (num W) * cont (plus2 V)  ->>  add V W * cont (num1).
tA: tretn N * cont (num1)  ->>  tretn (num N).

 -- The addition subroutine
t8: add ε N  ->>  tretn N.
t9: add N ε  ->>  tretn N.
t00: add (zero N) (zero K)  ->>  add N K * cont(addzero).
t10: add (one N)  (zero K)  ->>  add N K * cont(addone).
t01: add (zero N) (one K)   ->>  add N K * cont(addone).
t11: add (one N)  (one K)   ->>  add N K * cont(inc) * cont(addzero).

ta0: tretn N * cont(addzero)  ->>  tretn (zero N).
ta1: tretn N * cont(addone)  ->>  tretn (one N).
tiε: tretn ε * cont(inc)  ->>  tretn (one ε).
ti0: tretn (zero N) * cont(inc)  ->>  tretn (one N).
ti1: tretn (one N) * cont(inc)  ->>  tretn N * cont(inc) * cont(addzero).

{- Evaluate (λx.x)(λy.y) to a value -}
%trace * teval (app (lam λx. x) (lam λy. y)).
teval(app (lam(λx. x)) (lam(λy. y)))
teval(lam(λx. x))cont(app1(lam(λy. y)))
tretn(lam(λx. x))cont(app1(lam(λy. y)))
!thunk (lam(λy. y)) d4teval(d4)
!thunk (lam(λy. y)) d4teval(lam(λy. y))
!thunk (lam(λy. y)) d4tretn(lam(λx. x))
{- Evaluate (λx.xx)(λy.yy) for a bit; it diverges -}
%trace 12 teval (app (lam λx. app x x) (lam λy. app y y)).
teval(app (lam(λx. app x x)) (lam(λy. app y y)))
teval(lam(λx. app x x))cont(app1(lam(λy. app y y)))
tretn(lam(λx. app x x))cont(app1(lam(λy. app y y)))
!thunk (lam(λy. app y y)) d5teval(app d5 d5)
!thunk (lam(λy. app y y)) d5teval(d5)cont(app1(d5))
!thunk (lam(λy. app y y)) d5teval(lam(λy. app y y))cont(app1(d5))
!thunk (lam(λy. app y y)) d5tretn(lam(λx. app x x))cont(app1(d5))
!thunk d5 d6!thunk (lam(λy. app y y)) d5teval(app d6 d6)
!thunk d5 d6!thunk (lam(λy. app y y)) d5teval(d6)cont(app1(d6))
!thunk d5 d6!thunk (lam(λy. app y y)) d5teval(d5)cont(app1(d6))
!thunk d5 d6!thunk (lam(λy. app y y)) d5teval(lam(λy. app y y))cont(app1(d6))
!thunk d5 d6!thunk (lam(λy. app y y)) d5tretn(lam(λx. app x x))cont(app1(d6))
!thunk d6 d7!thunk d5 d6!thunk (lam(λy. app y y)) d5teval(app d7 d7)
{- Evaluate (λx.λy.xy)(λz.z) - final state refers to environment -}
%trace * teval (app (lam λx. lam λy. app x y) (lam λz. z)).
teval(app (lam(λx. lam(λy. app x y))) (lam(λz. z)))
teval(lam(λx. lam(λy. app x y)))cont(app1(lam(λz. z)))
tretn(lam(λx. lam(λy. app x y)))cont(app1(lam(λz. z)))
!thunk (lam(λz. z)) d8teval(lam(λy. app d8 y))
!thunk (lam(λz. z)) d8tretn(lam(λx. app d8 x))
{- Evaluate (1 + (61 + (λf.λy.f(f(fy))) (λx.x+20) 6)) = 128 -}
%exec * teval (plus 
                 (num (one ε))
                   (num (one (zero (one (one (one (one ε)))))))
                   ((app (app 
                     (lam λf. lam λy. app f (app f (app f y))) 
                     (lam λx. plus x (num (zero (zero (one (zero (one ε)))))))) 
                     (num (zero (one (one ε)))))))).
!thunk d10 d13!thunk (app d9 d10) d12!thunk (app d9 (app d9 d10)) d11!thunk (num(zero(one(one(ε))))) d10!thunk (lam(λx. plus x (num(zero(zero(one(zero(one(ε))))))))) d9tretn(num(zero(zero(zero(zero(zero(zero(zero(one(ε))))))))))