抽象書き換えマシン

抽象書き換えマシン(ARM) は、最小限の項書き換えシステムの項書き換えを実装する仮想マシンです。

最小項書き換えシステムは、各規則が次の 6 つの形式のいずれかをとる左線形項書き換えシステムです。

継続: $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}})$

これら 6 つの形式はそれぞれ、（ARM では）最新のマイクロプロセッサの 1 つまたは少数のプロセッサ命令にマッピングされます。したがって、最小限の項の書き換えは、1 つの削減ステップにつき数十から数百のクロックサイクル、つまり 1 秒あたり数百万の削減ステップで実現されます。

ARM は、すべての単一ソートされた無条件左線形項書き換えシステムを、同じ正規形関係を生成する最小限の項書き換えシステムに変換 (コンパイル) できるという点で、一般的な項書き換えを実装します。

最も内側の書き換えのコンパイルプロセスに関する参照を含む概要と、ARM の詳細な概要については、「ARM の範囲内: 最小限の書き換えシステムによる左線形書き換えシステムのコンパイル」を参照してください。遅延 (非内側) 書き換えの説明については、「熱心な機械での遅延書き換え」を参照してください。

ARM の文書化された実装 (用語書き換え言語 Epic を使用) は、こちらで入手できます。サイトとソフトウェアは、現在積極的にメンテナンスされていないことに注意してください。

参考文献

Giesl, JR; Middeldorp, A. (2004 年 7 月). 「文脈依存書き換えシステムの変換手法」(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. 2006-05-16 にオリジナル(PDF)からアーカイブ。2015-08-29に取得。
Nguyen, Quang-Huy (2001). 「Lazy Rewriting による Compact Normalisation Trace」(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. (2008 年 4 月). 「遅延書き換えの終了の再考」(PDF) .理論計算機科学の電子ノート. 204 : 35–51. CiteSeerX 10.1.1.142.1957 . doi :10.1016/j.entcs.2008.03.052.
キルヒナー、C .;キルヒナー、H. (2014) 「等式論理と書き換え」(PDF)。論理史ハンドブック。9 : 255–282。doi : 10.1016 /B978-0-444-51624-4.50006- X。ISBN 9780444516244。
Antoy, S.; Johannsen, J.; Libby, S. (2015). 「必要な計算、必要なステップのショートカット」。第 8 回用語とグラフによるコンピューティングに関する国際ワークショップの議事録。183 : 18–32。arXiv : 1505.07162v1。doi : 10.4204/ EPTCS.183.2 。