26 lines
2.8 KiB
Markdown
26 lines
2.8 KiB
Markdown
---
|
||
title: "Abstract rewriting machine"
|
||
chunk: 1/1
|
||
source: "https://en.wikipedia.org/wiki/Abstract_rewriting_machine"
|
||
category: "reference"
|
||
tags: "science, encyclopedia"
|
||
date_saved: "2026-05-05T11:30:38.694759+00:00"
|
||
instance: "kb-cron"
|
||
---
|
||
|
||
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:
|
||
|
||
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.
|
||
|
||
|
||
== References ==
|
||
Giesl, J. R.; Middeldorp, A. (July 2004). "Transformation techniques for context-sensitive rewrite systems" (PDF). Journal of Functional Programming. 14 (4): 379–427. CiteSeerX 10.1.1.127.2817. doi:10.1017/S0956796803004945.
|
||
Lucas, Salvador (2002). "Lazy Rewriting and Context-Sensitive Rewriting" (PDF). Electronic Notes in Theoretical Computer Science. 64: 234–254. CiteSeerX 10.1.1.14.3470. doi:10.1016/S1571-0661(04)80353-0. Archived from the original (PDF) on 2006-05-16. Retrieved 2015-08-29.
|
||
Nguyen, Quang-Huy (2001). "Compact Normalisation Trace via Lazy Rewriting" (PDF). Electronic Notes in Theoretical Computer Science. 57: 87–108. CiteSeerX 10.1.1.24.771. doi:10.1016/S1571-0661(04)00269-5. S2CID 38634432.
|
||
Schernhammer, F.; Gramlich, B. (April 2008). "Termination of Lazy Rewriting Revisited" (PDF). Electronic Notes in Theoretical Computer Science. 204: 35–51. CiteSeerX 10.1.1.142.1957. doi:10.1016/j.entcs.2008.03.052.
|
||
Kirchner, C.; Kirchner, H. (2014). "Equational Logic and Rewriting" (PDF). Handbook of the History of Logic. 9: 255–282. doi:10.1016/B978-0-444-51624-4.50006-X. ISBN 9780444516244.
|
||
Antoy, S.; Johannsen, J.; Libby, S. (2015). "Needed Computations Shortcutting Needed Steps". Electronic Proceedings in Theoretical Computer Science. 183: 18–32. arXiv:1505.07162v1. doi:10.4204/EPTCS.183.2. |