Abstract rewriting machine


The Abstract Rewriting Machine 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:
;Return:
;Match:
;Add:
;Delete:
;Ident:

Each of these six forms is mapped 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 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 . A description for lazy rewriting can be found in .
A documented implementation of ARM is available . Note that site and software are no longer being actively maintained.