On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion |
| |
Authors: | Olivier Danvy Kevin Millikin |
| |
Affiliation: | Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark |
| |
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). |
| |
Keywords: | Program derivation Programming calculi Programming languages Abstract machines Warm fusion Refocusing |
本文献已被 ScienceDirect 等数据库收录! |
|