Abstract Rewriting Machine

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

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

;Continuation:$f(vec\{x\},vec\{y\},vec\{z\})\; ightarrow\; g(vec\{x\},h(vec\{y\}),vec\{z\})$;Return:$f(x)\; ightarrow\; x$;Match:$f(vec\{x\},g(vec\{y\}),vec\{z\})\; ightarrow\; h(vec\{x\},vec\{y\},vec\{z\})$;Add:$f(vec\{x\},vec\{z\})\; ightarrow\; g(vec\{x\},y,vec\{z\})\; -\{\; m\; for\; \}~yinvec\{x\}cupvec\{z\}$;Delete:$f(vec\{x\},vec\{y\},vec\{z\})\; ightarrow\; g(vec\{x\},vec\{z\})$;Ident:$f(vec\{x\})\; ightarrow\; g(vec\{x\})$

Each of these six forms is mapped (in ARM) to one ora few processor instructions on most contemporary microprocessors. Accordingly, minimal term rewriting is achieved at tens tohundreds of clock cycles per reduction step -- millions of reductionsteps per second.

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

An overview with references to this compilation process for innermostrewriting, as well as a detailed overview of ARM, can be found in [http://portal.acm.org/citation.cfm?id=291903&dl=GUIDE&coll=&CFID=15151515&CFTOKEN=6184618 "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 [http://portal.acm.org/citation.cfm?id=345102&dl=ACM&coll=ACM&CFID=15151515&CFTOKEN=6184618 "Lazy rewriting on eager machinery"] .

A documented implementation of ARM (with the term rewriting language Epic) is available [http://www.babelfish.nl/epicarm.html here] . Note that site and software are no longer being actively maintained.