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