Абстрактная переписывающая машина

Абстрактная машина перезаписи (ARM) — это виртуальная машина , которая реализует переписывание терминов для систем минимального переписывания терминов.

Минимальные системы переписывания терминов — это леволинейные системы переписывания терминов , в которых каждое правило принимает одну из шести форм:

Продолжение

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

Возвращаться

$f(x)\rightarrow x$

Соответствовать

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

Добавлять

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

Удалить

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

Идентификатор

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

Каждая из этих шести форм отображается (в ARM) в одну или несколько инструкций процессора большинства современных микропроцессоров. Соответственно, минимальная перезапись термов достигается при десятках и сотнях тактовых циклов на шаг сокращения — миллионы шагов сокращения в секунду.

ARM реализует общее переписывание терминов, поскольку каждая односортная безусловная леволинейная система переписывания терминов может быть преобразована (скомпилирована) в минимальную систему переписывания терминов, которая приводит к тому же отношению нормальной формы.

Обзор со ссылками на этот процесс компиляции для самой внутренней перезаписи, а также подробный обзор ARM можно найти в разделе «В пределах досягаемости ARM: компиляция систем леволинейной перезаписи с помощью систем минимальной перезаписи» . Описание ленивого (невнутреннего) переписывания можно найти в разделе «Ленивое переписывание на нетерпеливых машинах» .

Документированная реализация ARM (с термином «язык переписывания Epic») доступна здесь . Обратите внимание, что сайт и программное обеспечение больше не обслуживаются.

Ссылки

• Гизл, младший; Мидделдорп, А. (июль 2004 г.). «Методы преобразования контекстно-зависимых систем перезаписи» (PDF) . Журнал функционального программирования . 14 (4): 379–427. CiteSeerX   10.1.1.127.2817 . дои : 10.1017/S0956796803004945 .
• Лукас, Сальвадор (2002). «Ленивое переписывание и контекстно-зависимое переписывание» (PDF) . Электронные заметки по теоретической информатике . 64 : 234–254. CiteSeerX   10.1.1.14.3470 . дои : 10.1016/S1571-0661(04)80353-0 . Архивировано из оригинала (PDF) 16 мая 2006 г. Проверено 29 августа 2015 г.
• Нгуен, Куанг-Хай (2001). «Компактная трассировка нормализации посредством ленивого переписывания» (PDF) . Электронные заметки по теоретической информатике . 57 : 87–108. CiteSeerX   10.1.1.24.771 . дои : 10.1016/S1571-0661(04)00269-5 . S2CID   38634432 .
• Шернхаммер, Ф.; Грамлих, Б. (апрель 2008 г.). «Возвращение к прекращению ленивого переписывания» (PDF) . Электронные заметки по теоретической информатике . 204 : 35–51. CiteSeerX   10.1.1.142.1957 . дои : 10.1016/j.entcs.2008.03.052 .
• Киршнер, К.; Киршнер, Х. (2014). «Эквациональная логика и переписывание» (PDF) . Справочник по истории логики . 9 : 255–282. дои : 10.1016/B978-0-444-51624-4.50006-X . ISBN  9780444516244 .
• Антой, С.; Йоханнсен, Дж.; Либби, С. (2015). «Необходимые вычисления, сокращающие необходимые шаги» . Материалы 8-го международного семинара по вычислениям с помощью термов и графов . 183 : 18–32. arXiv : 1505.07162v1 . дои : 10.4204/EPTCS.183.2 .