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

<math>f(\vec{x},\vec{y},\vec{z})\rightarrow g(\vec{x},h(\vec{y}),\vec{z})</math>

Return

<math>f(x)\rightarrow x</math>

Match

<math>f(\vec{x},g(\vec{y}),\vec{z})\rightarrow h(\vec{x},\vec{y},\vec{z})</math>

Add

<math>f(\vec{x},\vec{z})\rightarrow g(\vec{x},y,\vec{z}) -

{\rm for }~y\in\vec{x}\cup\vec{z}</math>

Delete

<math>f(\vec{x},\vec{y},\vec{z})\rightarrow g(\vec{x},\vec{z})</math>

Ident

<math>f(\vec{x})\rightarrow g(\vec{x})</math>

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.