Abstract rewriting machine

The Abstract Rewriting Machine (ARM) is a virtual machine which implements term rewriting for minimal term rewriting systems.

Minimal term rewriting systems are left-linear term rewriting systems in which each rule takes on one of six forms:

Continuation

$f({\vec {x}},{\vec {y}},{\vec {z}})\rightarrow g({\vec {x}},h({\vec {y}}),{\vec {z}})$

Return

$f(x)\rightarrow x$

Match

$f({\vec {x}},g({\vec {y}}),{\vec {z}})\rightarrow h({\vec {x}},{\vec {y}},{\vec {z}})$

Add

$f({\vec {x}},{\vec {z}})\rightarrow g({\vec {x}},y,{\vec {z}})-{\rm {for}}~y\in {\vec {x}}\cup {\vec {z}}$

Delete

$f({\vec {x}},{\vec {y}},{\vec {z}})\rightarrow g({\vec {x}},{\vec {z}})$

Ident

$f({\vec {x}})\rightarrow g({\vec {x}})$

Each of these six forms is mapped (in ARM) to one or a few processor instructions on most contemporary micro processors. Accordingly, minimal term rewriting is achieved at tens to hundreds of clock cycles per reduction step -- milions of reduction steps per second.

ARM implements general term rewriting, in that every single-sorted unconditional left-linear term rewriting system can be transformed (compiled) into a minimal term rewriting system that gives rise to the same normal form relation.

An overview with references to this compilation process for innermost rewriting, as well as a detailed overview of ARM, can be found in "Within ARM's reach: compilation of left-linear rewrite systems via minimal rewrite systems". A description for lazy (non-innermost) rewriting can be found in "Lazy rewriting on eager machinery".

A documented implementation of ARM (with the term rewriting language Epic) is available here. Note that site and software are no longer being actively maintained.