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