A Simple Application of Lightweight Fusion to Proving the Equivalence of Abstract Machines
AbstractWe 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.
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
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.