|
A Simple Application of Lightweight Fusion to Proving the Equivalence of
Abstract Machines
Olivier Danvy
March 2007 |
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
Available as PostScript, PDF, DVI. |