Simulation of Biernacka-Biernacki-Danvy's abstract machine into λ-bar-μμ̃
------------------------------------------------------------------------
written in April 2005

This is an example of the well-suitedness of λ-bar to express abstract
machines. We take Biernacka-Biernacki-Danvy's machine in
BRICS-RS-05-11.pdf, page 19 as an example.

I used λ-bar extended with an ad hoc calculus of explicit
substitution, with integers and an add-one continuation, and with a
dynamic mu binder written mu'.

  v ++= m                     (values)
  t ++= mu' a.(t|e) | t[e]    (terms)
  C ++= +1 . C                (evaluation contexts)
  [e]::= [] | [e;x->v] | [^e]


I rephrase Fig 7 inside this extended lambdar-bar. Only closed
expressions are evaluated. The special name tp is a dynamically bound,
hence global, variable. Note that S (shift) does not syntactically
differ of C, only its reduction rule differs.

t::=[m] | x | \x.t | t t'          | t+1           | <t>          | Sk.t
t::= m  | x | \x.t | mu a.(t|t'.a) | mu a.(t|+1.a) | mu'tp.(t|tp) | mu k.(t|tp)

v::= m | [x,t,e]   | C1
v::= m | \x.(t[e]) | C1

C1::= [] | ARG((t,e),C1) | SUCC(C1) | FUN(V,C1)
C1::= tp | t[e].C1 | +1.C1 | mu~ x.(v|x.C1)

C2::= * | C2.C1
C2::= tp | C1[tp->C2]

Machine states (eval)

S1::= (t,e,C1,C2)
S1::= (t[e]|C1) [tp->C2]

Machine states (cont)

S2::= (C1,v,C2)
S2::= (v|C1) [tp->C2]

where the notation [tp->C2] expresses that the store tp is bound to context C2


Initial transition (the rightmost tp is free):

t                    =>  (t|tp) [tp->tp]

Eval transition rules (not a value on the left)

(m[e]|C1)              [tp->C2] => (m|C1)            [tp->C2]
(x[e]|C1)              [tp->C2] => (e(x)|C1)         [tp->C2]
((\x.t)[e]|C1)         [tp->C2] => (\x.(t[^e])|C1)   [tp->C2]
(mu a. (t|t'.a)[e]|C1) [tp->C2] => (t[e]|t'[e].C1)   [tp->C2]
(mu a. (t|+1.a)[e]|C1) [tp->C2] => (t[e]|+1.C1)      [tp->C2]
(mu'tp.(t|tp)[e]  |C1) [tp->C2] => (t[e]|tp)         [tp->C1[tp->C2]]
(mu k. (t|tp)[e]  |C1) [tp->C2] => (t[e;k->\x.mu'tp.(x|C1)]|tp) [tp->C2]  (**)

Cont transition rules (a value on the left, cont2 rules have been inlined) 

(v|tp)       [tp->tp]         => v    (final transition)
(v|tp)       [tp->C1[tp->C2]] => (v|C1)                      [tp->C2]     (***)
(v|t'[e].C1) [tp->C2]         => (t'[e]|mu~ x.(v|x.C1))      [tp->C2]     (*)
(m|+1.C)                          [tp->C2] => (m+1,C1)       [tp->C2]
(v|mu~ x.(\x.(t[^e])|x.C1))       [tp->C2] => (t[e;x->v]|C1) [tp->C2]
(v|mu~ x.(\x.mu'tp.(x|C1')|x.C1)) [tp->C2] => (v|C1')        [tp->C1[tp->C2]]

Remarks:
1) transition (*) is an expansion in λ-bar
2) replace "mu'tp" by "mu _" in (**) to get C semantics
3) if we constrain (***) so that the value v is not an integer m, then
   we can rephrase it and the last two rules into

(\x.t|t'[e].C1)              [tp->C2] => (t'[e]|mu~ x.(t|C1)) [tp->C2]  (*)
(v|mu~ x.(t[^e]|C1))         [tp->C2] => (t[e;x->v]|C1)       [tp->C2]
(v|mu~ x.(mu'tp.(x|C1')|C1)) [tp->C2] => (v|C1')              [tp->C1[tp->C2]]

and the (*) is no longer an expansion

4) replace dynamic "mu'tp" by a static "mu tp" to get the semantics of F, 
indeed, the last rule then becomes

(v|mu~ x.(mu tp.(x|C1')|C1)) [tp->C2] => (v|C1'[tp->C1])      [tp->C2]


Proposition: if S --> S' in the abstract machine then S* -->> S'* in
λ-bar-μμ̃-calculus extended with a continuation store.