|
A Concrete Framework for Environment Machines
Magorzata Biernacka
February 2006 |
Abstract:
We materialize the common understanding that calculi with
explicit substitutions provide an intermediate step between an abstract
specification of substitution in the lambda-calculus and its concrete
implementations. To this end, we go back to Curien's original calculus of
closures (an early calculus with explicit substitutions), we extend it
minimally so that it can also express one-step reduction strategies, and we
methodically derive a series of environment machines from the specification
of two one-step reduction strategies for the lambda-calculus: normal order
and applicative order. The derivation extends Danvy and Nielsen's
refocusing-based construction of abstract machines with two new steps: one
for coalescing two successive transitions into one, and the other for
unfolding a closure into a term and an environment in the resulting abstract
machine. The resulting environment machines include both the Krivine machine
and the original version of Krivine's machine, Felleisen et al.'s CEK
machine, and Leroy's Zinc abstract machine.
Available as PostScript, PDF, DVI. |