書き直し

数学、コンピュータサイエンス、論理学において、書き換えとは、式の部分項を他の項に置き換える幅広い方法を指します。このような方法は、書き換えシステム（書き換えシステム、書き換えエンジン、^{[1] [2]}またはリダクションシステムとも呼ばれる）によって実現されます。書き換えシステムの最も基本的な形式は、オブジェクトのセットと、それらのオブジェクトを変換する方法に関する関係で構成されます。

書き換えは非決定的である可能性がある。項を書き換える1つの規則をその項にさまざまな方法で適用したり、複数の規則を適用したりできる。書き換えシステムは、ある項を別の項に変更するためのアルゴリズムではなく、一連の可能な規則適用を提供する。ただし、適切なアルゴリズムと組み合わせると、書き換えシステムはコンピュータプログラムと見なすことができ、いくつかの定理証明器^[3]と宣言型プログラミング言語は項の書き換えに基づいている。^{[4] [5]}

論理学では、式の連言正規形（CNF）を得るための手順は、書き換えシステムとして実装することができます。^[6]このようなシステムの例の規則は次のようになります。

${\displaystyle \neg \neg A\to A}$（二重否定除去）

${\displaystyle \neg (A\land B)\to \neg A\lor \neg B}$（ド・モルガンの法則）

${\displaystyle \neg (A\lor B)\to \neg A\land \neg B}$

${\displaystyle (A\land B)\lor C\to (A\lor C)\land (B\lor C)}$（分配性）

${\displaystyle A\lor (B\land C)\to (A\lor B)\land (A\lor C),}$^{[注 1]}

ここで、記号 ( ) は、規則の左側に一致する式が右側で形成される式に書き換えられることを示し、記号はそれぞれ部分式を表します。このようなシステムでは、各規則は左側が右側と等しくなるように選択され、その結果、左側が部分式に一致する場合、その部分式を左から右に書き換えることで、論理的な一貫性と式全体の値が維持されます。 ${\displaystyle \to}$

項書き換えシステムは、自然数の算術演算を計算するために使用できます。このためには、各数を項としてエンコードする必要があります。最も単純なエンコードは、定数 0 (ゼロ) と後継関数Sに基づくペアノ公理で使用されるものです。たとえば、数 0、1、2、3 は、それぞれ項 0、S(0)、S(S(0))、S(S(S(0))) で表されます。次の項書き換えシステムを使用して、与えられた自然数の和と積を計算できます。^[7]

${\displaystyle {\begin{aligned}A+0&\to A&{\textrm {(1)}},\\A+S(B)&\to S(A+B)&{\textrm {(2)}},\\A\cdot 0&\to 0&{\textrm {(3)}},\\A\cdot S(B)&\to A+(A\cdot B)&{\textrm {(4)}}.\end{aligned}}}$

たとえば、2 + 2 の計算で結果が 4 になるという処理は、次のように項を書き換えることで再現できます。

${\displaystyle S(S(0))+S(S(0))}$ ${\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}$ ${\displaystyle S(\;S(S(0))+S(0)\;)}$ ${\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}$ ${\displaystyle S(S(\;S(S(0))+0\;))}$ ${\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}$ ${\displaystyle S(S(S(S(0)))),}$

ルール番号は書き換え先の矢印の上に示されています。

別の例として、2⋅2の計算は次のようになります。

${\displaystyle S(S(0))\cdot S(S(0))}$ ${\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))\cdot S(0)}$ ${\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))+S(S(0))\cdot 0}$ ${\displaystyle \;\;{\stackrel {(3)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))+0}$ ${\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))}$ ${\displaystyle \;\;{\stackrel {\textrm {s.a.}}{\to }}\;\;}$ ${\displaystyle S(S(S(S(0)))),}$

最後のステップは、前の例の計算で構成されます。

言語学では、句構造規則（書き換え規則とも呼ばれる）は、生成文法の一部のシステムで、言語の文法的に正しい文を生成する手段として使用されています^[8]。このような規則は通常、形式を取ります。ここで、Aは名詞句や文などの統語カテゴリラベル、Xはそのようなラベルまたは形態素のシーケンスであり、文の構成要素構造を生成する際にAをXに置き換えることができるという事実を表しています。たとえば、規則は、文が名詞句（NP）とそれに続く動詞句（VP）で構成できることを意味しています。さらに規則により、名詞句と動詞句がどのような構成要素で構成できるかが指定されるなどです。 ${\displaystyle {\rm {A\rightarrow X}}}$${\displaystyle {\rm {S\rightarrow NP\ VP}}}$

上記の例から、書き換えシステムを抽象的な方法で考えることができることは明らかです。オブジェクトのセットと、それらを変換するために適用できる規則を指定する必要があります。この概念の最も一般的な（一次元）設定は、抽象縮小システム^[9]または抽象書き換えシステム（略してARS）と呼ばれます。^[10] ARS は、オブジェクトのセットAと、A上の2 項関係→を組み合わせたもので、縮小関係、書き換え関係^[11]、または単に縮小と呼ばれます。^[9]

ARS の一般的な設定では、多くの概念や表記法を定義できます。は の反射的推移的閉包です。はの対称閉包です。はの反射的推移的対称閉包です。ARS の単語問題は、 xとy が与えられたときに、 かどうかを判断することです。 A内のオブジェクトx は、となる他のy がA内に存在する場合、既約であると呼ばれます。そうでない場合は、既約ではない、または正規形と呼ばれます。 、かつyが既約である場合、オブジェクトyは「 xの正規形」と呼ばれます。 xの正規形が一意である場合、これは通常 で示されます。すべてのオブジェクトに少なくとも 1 つの正規形がある場合、ARS は正規化と呼ばれます。または、という特性を持つz が存在する場合、xとyは結合可能であると言われます。 がを意味する場合、 ARS はChurch–Rosser 特性を持っていると言われます。A内のすべてのw、x、yに対して がを意味する場合、 ARS は合流性があると言われます。 ARS が局所的に合流性を持つの は、 A内のすべてのw、x、yに対して が成り立つ場合のみです。無限連鎖 がない場合、 ARS は終了性またはネーター性を持つと言われます。合流性があり終了する ARS は収束性または標準的と呼ばれます。 ${\displaystyle {\overset {*}{\rightarrow }}}$${\displaystyle \rightarrow }$${\displaystyle \leftrightarrow }$${\displaystyle \rightarrow }$${\displaystyle {\overset {*}{\leftrightarrow }}}$${\displaystyle \rightarrow }$${\displaystyle x{\overset {*}{\leftrightarrow }}y}$${\displaystyle x\rightarrow y}$${\displaystyle x{\stackrel {*}{\rightarrow }}y}$${\displaystyle x{\downarrow }}$${\displaystyle x\downarrow y}$${\displaystyle x{\overset {*}{\rightarrow }}z{\overset {*}{\leftarrow }}y}$${\displaystyle x{\overset {*}{\leftrightarrow }}y}$${\displaystyle x\downarrow y}$${\displaystyle x{\overset {*}{\leftarrow }}w{\overset {*}{\rightarrow }}y}$${\displaystyle x\downarrow y}$${\displaystyle x\leftarrow w\rightarrow y}$${\displaystyle x{\mathbin {\downarrow }}y}$${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }$

抽象書き換えシステムの重要な定理は、ARS が合流性を持つ ためにはChurch-Rosser 特性が必要であること、ニューマンの補題(終了 ARS が合流性を持つのは、局所的に合流する場合のみである)、およびARS の単語問題が一般に 決定不可能であることです。

文字列書き換えシステム( SRS) は、半 Thue システムとも呼ばれ、アルファベット上の文字列(単語)の自由モノイド構造を利用して、書き換え関係 を、いくつかの規則 の左側と右側をそれぞれ部分文字列として含むアルファベットのすべての文字列に拡張します。正式には、半 Thue システム は、 が(通常は有限の) アルファベット、 がアルファベット内のいくつかの (固定の) 文字列間の 2 項関係 (書き換え規則の集合 と呼ばれます) であるタプルです。上のによって誘導される1 ステップ書き換え関係 は、次のように定義されます。が任意の文字列である場合、 、、 となるが存在する場合。は 上の関係であるため、このペアは抽象書き換えシステムの定義に適合します。 には空の文字列があるため、は のサブセットです。関係が対称 である場合、このシステムはThue システムと呼ばれます。 ${\displaystyle R}$ ${\displaystyle (\Sigma ,R)}$${\displaystyle \Sigma }$${\displaystyle R}$ ${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle R}$${\displaystyle \Sigma ^{*}}$${\displaystyle s,t\in \Sigma ^{*}}$${\displaystyle s{\underset {R}{\rightarrow }}t}$${\displaystyle x,y,u,v\in \Sigma ^{*}}$${\displaystyle s=xuy}$${\displaystyle t=xvy}$${\displaystyle uRv}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle \Sigma ^{*}}$${\displaystyle (\Sigma ^{*},{\underset {R}{\rightarrow }})}$${\displaystyle \Sigma ^{*}}$${\displaystyle R}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle R}$

SRS では、簡約関係はモノイド演算と互換性があり、つまりすべての文字列 に対して が成り立つことを意味します。同様に、 の反射的推移対称閉包( と表記)は合同であり、つまり同値関係(定義により)であり、文字列連結とも互換性があります。この関係は、によって生成されるThue 合同と呼ばれます。Thue システム、つまり が対称である場合、書き換え関係はThue 合同 と一致します。 ${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$${\displaystyle x{\overset {*}{\underset {R}{\rightarrow }}}y}$${\displaystyle uxv{\overset {*}{\underset {R}{\rightarrow }}}uyv}$${\displaystyle x,y,u,v\in \Sigma ^{*}}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle R}$${\displaystyle R}$${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$

半Thueシステムの概念は、本質的にモノイド の表現と一致します。は合同なので、 Thue合同によって自由モノイド の因子モノイドを定義できます。 モノイドがと同型である場合、半Thueシステムはのモノイド表現と呼ばれます。 ${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$ ${\displaystyle {\mathcal {M}}_{R}=\Sigma ^{*}/{\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle \Sigma ^{*}}$${\displaystyle {\mathcal {M}}}$${\displaystyle {\mathcal {M}}_{R}}$${\displaystyle (\Sigma ,R)}$${\displaystyle {\mathcal {M}}}$

すぐに、代数の他の分野との非常に有用なつながりがいくつか得られます。たとえば、という規則を持つアルファベット(ここでは空文字列 )は、1 つの生成子上の自由群の表現です。代わりに規則が だけであれば、双環モノイドの表現が得られます。したがって、半 Thue システムは、モノイドとグループの単語問題を解くための自然なフレームワークを構成します。実際、すべてのモノイドは という形式の表現を持ちます。つまり、常に半 Thue システムで表現でき、無限のアルファベットにわたる場合もあります。 ${\displaystyle \{a,b\}}$${\displaystyle \{ab\rightarrow \varepsilon ,ba\rightarrow \varepsilon \}}$${\displaystyle \varepsilon }$${\displaystyle \{ab\rightarrow \varepsilon \}}$${\displaystyle (\Sigma ,R)}$

半Thueシステムの単語問題は一般に決定不可能であり、この結果はポストマルコフ定理と呼ばれることもあります。^[12]

項書き換えシステム( TRS ) は、ネストされたサブ式を持つ式である項をオブジェクトとする書き換えシステムです。たとえば、上記の § ロジック で示したシステムは項書き換えシステムです。このシステムの項は、二項演算子とおよび単項演算子で構成されています。また、ルールには変数があり、これは任意の可能な項を表します (ただし、単一の変数は単一のルール全体で常に同じ項を表します)。 ${\displaystyle (\vee )}$${\displaystyle (\wedge )}$${\displaystyle (\neg )}$

文字列書き換えシステムのオブジェクトがシンボルのシーケンスであるのに対し、項書き換えシステムのオブジェクトは項代数を形成します。項はシンボルのツリーとして視覚化でき、許容されるシンボルの集合は与えられた署名によって固定されます。形式的には、項書き換えシステムはチューリングマシンの全機能を備えており、つまり、計算可能なすべての関数は項書き換えシステムによって定義できます。^[13]

いくつかのプログラミング言語は項の書き換えに基づいています。その一例が、数学アプリケーションのための関数型プログラミング言語であるPureです。^{[14] [15]}

書き換え規則は、一般に と表記される一対の項で、左辺l を右辺rで置き換えることができることを示します。項書き換えシステムとは、このような規則の集合Rのことです。項sに規則を適用できるのは、左項l がsの一部の項に一致する場合、つまり、ある置換があり、ある位置pを根とするの一部の項が項lに置換を適用した結果である場合です。規則の左辺に一致する部分項は、リデックスまたは可約式と呼ばれます。^[16]この規則適用の結果の項t は、 sの位置pにある部分項を、置換を適用した項 で 置き換えた結果です(図 1 を参照)。この場合、は1 ステップ で書き換えられる、またはシステム によってに直接 に書き換えられると言われます。これは、一部の著者によって正式に、、または と表記されます。 ${\displaystyle l\rightarrow r}$${\displaystyle l\rightarrow r}$ ${\displaystyle \sigma }$${\displaystyle s}$ ${\displaystyle \sigma }$${\displaystyle r}$${\displaystyle \sigma }$${\displaystyle s}$${\displaystyle t}$${\displaystyle R}$${\displaystyle s\rightarrow _{R}t}$${\displaystyle s{\underset {R}{\rightarrow }}t}$${\displaystyle s{\overset {R}{\rightarrow }}t}$

項がいくつかのステップで項 に書き換えられる場合、つまり の場合、項はに書き換えられると言われ、正式には と表記されます。言い換えると、関係 は関係 の推移閉包です。また、表記 はの反射推移閉包を表すためにもよく使用されます。つまり、または の場合です。^[17]規則の集合によって与えられる項書き換えは、上で定義したように、項 をそのオブジェクト、 をその書き換え関係とする 抽象書き換えシステムと見なすことができます。${\displaystyle t_{1}}$${\displaystyle t_{n}}$${\displaystyle t_{1}{\underset {R}{\rightarrow }}t_{2}{\underset {R}{\rightarrow }}\cdots {\underset {R}{\rightarrow }}t_{n}}$${\displaystyle t_{1}}$${\displaystyle t_{n}}$${\displaystyle t_{1}{\overset {+}{\underset {R}{\rightarrow }}}t_{n}}$${\displaystyle {\overset {+}{\underset {R}{\rightarrow }}}}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle s{\overset {*}{\underset {R}{\rightarrow }}}t}$${\displaystyle s=t}$${\displaystyle s{\overset {+}{\underset {R}{\rightarrow }}}t}$${\displaystyle R}$${\displaystyle {\underset {R}{\rightarrow }}}$

たとえば、は書き換え規則であり、 の結合法則に関する正規形を確立するためによく使用されます。 この規則は、対応する置換 を用いて項 の分子に適用できます (図 2 を参照^{)。 [注 2]}この置換を規則の右側に適用すると項 が生成され、分子をこの項で置き換えると が生成されます。これが書き換え規則を適用した結果の項です。 全体として、書き換え規則を適用することで、初等代数で「 の結合法則を に適用する」と呼ばれることが達成されます。 あるいは、この規則を元の項の分母に適用して を生成することもできます。 ${\displaystyle x*(y*z)\rightarrow (x*y)*z}$${\displaystyle *}$${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$${\displaystyle \{x\mapsto a,\;y\mapsto a+1,\;z\mapsto a+2\}}$${\displaystyle (a*(a+1))*(a+2)}$${\displaystyle {\frac {(a*(a+1))*(a+2)}{1*(2*3)}}}$${\displaystyle *}$${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$${\displaystyle {\frac {a*((a+1)*(a+2))}{(1*2)*3}}}$

一般的な書き換えシステムの停止性の問題は、抽象書き換えシステム#停止性と収束で扱われます。特に項書き換えシステムの場合、以下の追加の微妙な点を考慮する必要があります。

線形左辺を持つ1つの規則からなるシステムであっても、終了性は決定不可能である。 ^{[18] [19]単項関数記号のみを使用するシステムでは終了性も決定不可能であるが、有限}基底システム では終了性は決定可能である。 ^[20]

次の項書き換えシステムは正規化^{[注3]であるが、停止性[注4]}がなく、合流性もない: ^[21] $${\displaystyle {\begin{aligned}f(x,x)&\rightarrow g(x),\\f(x,g(x))&\rightarrow b,\\h(c,x)&\rightarrow f(h(x,c),h(x,x)).\\\end{aligned}}}$$

終了項書き換えシステムの次の2つの例は、外山によるものである: ^[22]

${\displaystyle f(0,1,x)\rightarrow f(x,x,x)}$

そして

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

${\displaystyle g(x,y)\rightarrow y.}$

それらの結合は非終了システムである。

$${\displaystyle {\begin{aligned}&f(g(0,1),g(0,1),g(0,1))\\\rightarrow &f(0,g(0,1),g(0,1))\\\rightarrow &f(0,1,g(0,1))\\\rightarrow &f(g(0,1),g(0,1),g(0,1))\\\rightarrow &\cdots \end{aligned}}}$$ この結果は、²つの終了項書き換えシステムの和集合とが再び終了するためには、 のすべての左辺と の右辺が線形であり、の左辺と の右辺の間に「重なり」がないと主張したダーショウィッツの予想[23]を反証するものである。これらの特性はすべて、外山の例によって満たされている。 ${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$

項書き換えシステムの停止性証明で使用される順序関係については、 「書き換え順序」および「パス順序 (項書き換え)」を参照してください。

高階書き換えシステムは、1階項書き換えシステムをラムダ項に一般化したものであって、高階関数と束縛変数を許容する。^[24] 1階TRSに関する様々な結果は、HRSに対しても同様に再定式化できる。^[25]

グラフ書き換えシステムは、項書き換えシステムの別の一般化であり、 （基底）項または対応するツリー表現の代わりにグラフに対して動作します。

トレース理論は、トレースモノイドや履歴モノイドなどを通じて、より形式的な用語でマルチプロセッシングを議論する手段を提供します。トレースシステムでは書き換えも実行できます。

• クリティカルペア（ロジック）
• コンパイラ
• クヌース・ベンディックス補完アルゴリズム
• L-systems は並列で実行される書き換えを指定します。
• コンピュータサイエンスにおける参照の透明性
• 規制された書き換え
• 相互作用ネット

• バーダー、フランツ、ニプコウ、トビアス（1999）。用語の書き換えとそのすべて。ケンブリッジ大学出版局。ISBN 978-0-521-77920-3。316ページ。
• Marc Bezem、Jan Willem Klop、Roel de Vrijer ("Terese")、Term Rewriting Systems ("TeReSe")、Cambridge University Press、2003 年、ISBN 0-521-39115-6。これは最新の包括的なモノグラフです。ただし、まだ標準ではない表記法や定義をかなり使用しています。たとえば、Church-Rosser プロパティは合流と同じであると定義されています。 
• Nachum DershowitzとJean-Pierre Jouannaud の「Rewrite Systems」、Jan van Leeuwen (編) 著『Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics』の第 6 章。Elsevierおよび MIT Press、1990 年、ISBN 0-444-88074-7、243～ 320 ページ。この章のプレプリントは著者から無料で入手できますが、図が欠落しています。 
• Nachum Dershowitz およびDavid Plaisted。「Rewriting」、John Alan RobinsonおよびAndrei Voronkov (編)、『Handbook of Automated Reasoning』第 1 巻、第9 章。
• Gérard Huetと Derek Oppen、方程式と書き換えルール、調査 (1980) スタンフォード検証グループ、レポート番号 15 コンピュータ サイエンス部門レポート番号 STAN-CS-80-785
• Jan Willem Klop . 「項書き換えシステム」、Samson Abramsky、Dov M. Gabbay、Tom Maibaum (編)、『コンピュータサイエンスにおける論理ハンドブック、第 2 巻: 背景: 計算構造』の第 1 章。
• David Plaisted. 「等式推論と項書き換えシステム」、Dov M. Gabbay、CJ Hogger、John Alan Robinson (編)、『人工知能と論理プログラミングにおける論理ハンドブック』第 1 巻。
• Jürgen Avenhaus および Klaus Madlener。「項の書き換えと方程式による推論」。Ranan B. Banerji (編)、『人工知能における形式的手法: ソースブック』、Elsevier (1990)。

文字列の書き換え

• Ronald V. Bookと Friedrich Otto、「String-Rewriting Systems」、Springer (1993)。
• ベンジャミン・ベニングホーフェン、スザンヌ・ケンメリッヒ、マイケル・M・リヒター、「システム・オブ・リダクション」。LNCS 277、Springer-Verlag (1987)。

他の

• Martin Davis、Ron Sigal、Elaine J. Weyuker、(1994)計算可能性、複雑性、言語：理論計算機科学の基礎 - 第2版、Academic Press、ISBN 0-12-206382-1。 

無料辞書のウィクショナリーで「rewriting」を調べてください。

• ホームページの書き換え
• IFIP ワーキンググループ 1.6
• 書き直しの研究者、アート・ミデルドルプ、インスブルック大学
• 終了ポータル
• Maudeシステム — 一般的な用語書き換えシステムのソフトウェア実装。^[5]