1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University 2 Teoretisk naturvidenskab, Aarhus University, Aarhus University 3 Department of Computer Science, Science and Technology, Aarhus University 4 Department of Computer Science, Science and Technology, Aarhus University
We show how Ohori and Sasano’s recent lightweight fusion by fixed-point promotion provides a simple way to prove the equivalence of the two standard styles of specification of abstract machines: (1) in small-step form, as a state-transition function together with a ‘driver loop’, i.e., a function implementing the iteration of this transition function; and (2) in big-step form, as a tail-recursive function that directly maps a given configuration to a final state, if any. The equivalence hinges on our observation that for abstract machines, fusing a small-step specification yields a big-step specification. We illustrate this observation here with a recognizer for Dyck words, the CEK machine, and Krivine’s machine with call/cc. The need for such a simple proof is motivated by our current work on small-step abstract machines as obtained by refocusing a function implementing a reduction semantics (a syntactic correspondence), and big-step abstract machines as obtained by CPStransforming and then defunctionalizing a function implementing a big-step semantics (a functional correspondence). © 2007 Elsevier B.V. All rights reserved.
Information Processing Letters, 2008, Vol 106, Issue 3, p. 100-109
Program derivation; Programming calculi; Programming languages; Abstract machines; Warm fusion; Refocusing
Main Research Area: