A Simple Application of Lightweight Fusion to Proving the Equivalence of Abstract Machines

Authors

  • Olivier Danvy
  • Kevin Millikin

DOI:

https://doi.org/10.7146/brics.v14i8.21931

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) as a transition function together with a `driver loop' implementing the iteration of this transition function; and (2) as a function directly iterating upon a configuration until reaching a final state, if ever. The equivalence hinges on the fact that the latter style of specification is a fused version of the former one. The need for such a simple proof is motivated by our recent work on syntactic correspondences between reduction semantics and abstract machines, using refocusing.

Downloads

Published

2007-03-12

How to Cite

Danvy, O., & Millikin, K. (2007). A Simple Application of Lightweight Fusion to Proving the Equivalence of Abstract Machines. BRICS Report Series, 14(8). https://doi.org/10.7146/brics.v14i8.21931