On the Equivalence between Small-Step and Big-Step Abstract Machines: A Simple Application of Lightweight Fusion

Authors

  • Olivier Danvy
  • Kevin Millikin

DOI:

https://doi.org/10.7146/brics.v14i16.21935

Abstract

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 CPS-transforming and then defunctionalizing a function implementing a big-step semantics (a functional correspondence).

Downloads

Published

2007-11-12

How to Cite

Danvy, O., & Millikin, K. (2007). On the Equivalence between Small-Step and Big-Step Abstract Machines: A Simple Application of Lightweight Fusion. BRICS Report Series, 14(16). https://doi.org/10.7146/brics.v14i16.21935