Máquina de reescritura abstracta

La Abstract Rewriting Machine (ARM) es una máquina virtual que implementa la reescritura de términos para sistemas de reescritura de términos mínimos.

Los sistemas de reescritura de términos mínimos son sistemas de reescritura de términos lineales por la izquierda en los que cada regla adopta una de seis formas:

Continuación

${\displaystyle f({\vec {x}},{\vec {y}},{\vec {z}})\rightarrow g({\vec {x}},h({\vec {y}}),{\vec {z}})}$

Devolver

${\displaystyle f(x)\rightarrow x}$

Fósforo

${\displaystyle f({\vec {x}},g({\vec {y}}),{\vec {z}})\rightarrow h({\vec {x}},{\vec {y}},{\vec {z}})}$

Agregar

${\displaystyle f({\vec {x}},{\vec {z}})\rightarrow g({\vec {x}},y,{\vec {z}})-{\rm {for}}~y\in {\vec {x}}\cup {\vec {z}}}$

Borrar

${\displaystyle f({\vec {x}},{\vec {y}},{\vec {z}})\rightarrow g({\vec {x}},{\vec {z}})}$

Identidad

${\displaystyle f({\vec {x}})\rightarrow g({\vec {x}})}$

Cada una de estas seis formas está asignada (en ARM) a una o varias instrucciones de procesador en la mayoría de los microprocesadores contemporáneos. En consecuencia, la reescritura de términos mínima se logra entre decenas y cientos de ciclos de reloj por paso de reducción: millones de pasos de reducción por segundo.

ARM implementa la reescritura de términos generales, en el sentido de que cada sistema de reescritura de términos lineales a la izquierda incondicional de orden único se puede transformar (compilar) en un sistema de reescritura de términos mínimos que da lugar a la misma relación de forma normal.

Se puede encontrar una descripción general con referencias a este proceso de compilación para la reescritura más interna, así como una descripción detallada de ARM, en "Dentro del alcance de ARM: compilación de sistemas de reescritura lineal izquierda mediante sistemas de reescritura mínima". Se puede encontrar una descripción de la reescritura diferida (no más interna) en "Reescritura diferida en maquinaria ansiosa".

Una implementación documentada de ARM (con el término lenguaje de reescritura Epic) está disponible aquí. Tenga en cuenta que el sitio y el software ya no reciben mantenimiento activo.

Referencias

• Giesl, JR; Middeldorp, A. (julio de 2004). "Técnicas de transformación para sistemas de reescritura sensibles al contexto" (PDF) . Revista de programación funcional . 14 (4): 379–427. CiteSeerX  10.1.1.127.2817 . doi :10.1017/S0956796803004945.
• Lucas, Salvador (2002). "Reescritura diferida y reescritura sensible al contexto" (PDF) . Apuntes Electrónicos en Informática Teórica . 64 : 234–254. CiteSeerX  10.1.1.14.3470 . doi :10.1016/S1571-0661(04)80353-0. Archivado desde el original (PDF) el 16 de mayo de 2006 . Consultado el 29 de agosto de 2015 .
• Nguyen, Quang-Huy (2001). "Seguimiento de normalización compacto mediante reescritura diferida" (PDF) . Apuntes Electrónicos en Informática Teórica . 57 : 87-108. CiteSeerX  10.1.1.24.771 . doi :10.1016/S1571-0661(04)00269-5. S2CID  38634432.
• Schernhammer, F.; Gramlich, B. (abril de 2008). "Revisión de la terminación de la reescritura diferida" (PDF) . Apuntes Electrónicos en Informática Teórica . 204 : 35–51. CiteSeerX  10.1.1.142.1957 . doi :10.1016/j.entcs.2008.03.052.
• Kirchner, C.; Kirchner, H. (2014). "Lógica Ecuacional y Reescritura" (PDF) . Manual de Historia de la Lógica . 9 : 255–282. doi :10.1016/B978-0-444-51624-4.50006-X. ISBN 9780444516244.
• Antonio, S.; Johannsen, J.; Libby, S. (2015). "Cálculos necesarios, atajos de pasos necesarios". Actas del 8º Taller Internacional sobre Computación con Términos y Gráficos . 183 : 18–32. arXiv : 1505.07162v1 . doi : 10.4204/EPTCS.183.2 .