Abstract Rewriting Machine

From Wikipedia, the free encyclopedia

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 -- millions 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.