imported>Headbomb: /* References */ | Add: journal, title. | Use this tool. Report bugs. | #UCB_Gadget

2025-06-12T18:16:25Z

References: | Add: journal, title. | Use this tool. Report bugs. | #UCB_Gadget

New page

{{external links |date=April 2024}}
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 system]]s in which each rule takes on one of six forms:

{{block indent| em = 1.5 |
;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—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 [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 [https://web.archive.org/web/20070327185702/http://www.babelfish.nl/epicarm.html here]. Note that site and software are no longer being actively maintained.

== References ==
* {{Cite journal | last1 = Giesl | first1 = J. R.| last2 = Middeldorp | first2 = A.| doi = 10.1017/S0956796803004945 | title = Transformation techniques for context-sensitive rewrite systems | url = http://cl-informatik.uibk.ac.at/users/ami/research/publications/journals/04jfp.pdf| journal = [[Journal of Functional Programming]]| volume = 14 | issue = 4 | pages = 379–427| date=July 2004 | citeseerx = 10.1.1.127.2817}}
* {{Cite journal | last1 = Lucas | first1 = Salvador | doi = 10.1016/S1571-0661(04)80353-0 | title = Lazy Rewriting and Context-Sensitive Rewriting | journal = [[Electronic Notes in Theoretical Computer Science]] | volume = 64 | pages = 234–254 | year = 2002 | citeseerx = 10.1.1.14.3470 | url = http://www.dsic.upv.es/users/elp/berlanga/slucas/entcsV64/entcsV64.pdf | access-date = 2015-08-29 | archive-url = https://web.archive.org/web/20060516192924/http://www.dsic.upv.es/users/elp/berlanga/slucas/entcsV64/entcsV64.pdf | archive-date = 2006-05-16 | url-status = dead }}
* {{Cite journal | last1 = Nguyen | first1 = Quang-Huy| doi = 10.1016/S1571-0661(04)00269-5 | title = Compact Normalisation Trace via Lazy Rewriting | journal = [[Electronic Notes in Theoretical Computer Science]]| volume = 57 | pages = 87–108| year = 2001 | url = http://hal.inria.fr/docs/00/10/78/74/PDF/A01-R-139.pdf| citeseerx = 10.1.1.24.771| s2cid = 38634432}}
* {{Cite journal | last1 = Schernhammer | first1 = F.| last2 = Gramlich | first2 = B.| doi = 10.1016/j.entcs.2008.03.052 | title = Termination of Lazy Rewriting Revisited | journal = [[Electronic Notes in Theoretical Computer Science]]| volume = 204 | pages = 35–51| date=April 2008 | citeseerx = 10.1.1.142.1957| url = http://www.logic.at/staff/gramlich/papers/wrs07-techrep.pdf}}
* {{Cite journal | last1 = Kirchner | first1 = C. | last2 = Kirchner | first2 = H.| doi = 10.1016/B978-0-444-51624-4.50006-X | title = Equational Logic and Rewriting | journal = [[Handbook of the History of Logic]]| volume = 9 | pages = 255–282| date=2014 | isbn = 9780444516244 | url = https://hal.inria.fr/hal-01183817/file/eqLogicRw.pdf}}
* {{Cite journal | last1 = Antoy | first1 = S.| last2 = Johannsen | first2 = J.| last3 = Libby | first3 = S.| title = Needed Computations Shortcutting Needed Steps| journal = Electronic Proceedings in Theoretical Computer Science| doi = 10.4204/EPTCS.183.2 | volume = 183 | date=2015 | pages = 18–32| arxiv = 1505.07162v1| doi-access = free }}

[[Category:Virtual machines]]
[[Category:Term-rewriting programming languages]]

{{Computer science stub}}

Abstract rewriting machine - Revision history

imported>Headbomb: /* References */ | Add: journal, title. | Use this tool. Report bugs. | #UCB_Gadget