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