{- Part 1: Turing machines -}

rR: hR * tR  ->>  hR * t0 * tR.
rL: tL * hL  ->>  tL * t0 * hL.
r1: ¡s₁ * t0 * hL  ->>  ¡s₂ * t0 * hR.
r2: ¡s₁ * hR * t0  ->>  ¡s₂ * t0 * hR.
r3: ¡s₂ * t1 * hL  ->>  ¡s₁ * hL * t0.
r4: ¡s₂ * hR * t1  ->>  ¡s₁ * hR * t0.

{- Starting with the tape ..... 1 0 [ 1 ] 1 0 1 .... -}

%trace 10 ¡s₂ * 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)).

{- Evaluate (λx.xx)(λy.yy) for a bit; it diverges -}

%trace 6 eval (app (lam λx. app x x) (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  ->>  ∃d₁. ¡leval M d₁ * ¡lcont d₁ (app1 N) D.
l3: ¡lretn (lam λx. M x) D₁ * ¡lcont D₁ (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.

{- 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.

{- 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)).

{- Evaluate (λx.xx)(λy.yy) for a bit; it diverges -}

%trace 12 teval (app (lam λx. app x x) (lam λy. app y y)).

{- Evaluate (λx.λy.xy)(λz.z) - final state refers to environment -}

%trace * teval (app (lam λx. lam λy. app x y) (lam λz. z)).

{- Evaluate (1 + (61 + (λf.λy.f(f(fy))) (λx.x+20) 6)) = 128 -}

%exec * teval (plus 
                 (num (one ε))
                 (plus 
                   (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 ε)))))))).