Loading article…
数学、言語学、コンピュータ科学、論理学において、書き換えは、式の部分項を他の項に置き換える幅広い方法を網羅しています。このような方法は、書き換えシステム（書き換えシステム、書き換えエンジン[ 1 ] [ 2 ]、または還元システムとも呼ばれる）によって実現できます。最も基本的な形式では、書き換えシステムは、オブジェクトの集合と、それらのオブジェクトを変換する方法に関する関係から構成されます。
書き換えは非決定論的である可能性がある。項を書き換える1つのルールは、その項に対してさまざまな方法で適用できる場合もあれば、複数のルールが適用できる場合もある。したがって、書き換えシステムは、ある項を別の項に変更するアルゴリズムを提供するのではなく、可能なルール適用のセットを提供する。しかし、適切なアルゴリズムと組み合わせると、書き換えシステムはコンピュータプログラムと見なすことができ、いくつかの定理証明器[ 3 ]や宣言型プログラミング言語は項書き換えに基づいている[ 4 ] [ 5 ] 。
論理学において、論理式の連言標準形（CNF）を得る手順は、書き換えシステムとして実装できる。[ 6 ]例えば、そのようなシステムの規則は次のようになる。
各ルールでは、各変数は部分式を表し、記号（) は、その左辺に一致する式を、その右辺に一致する式に書き換えることができることを示します。このようなシステムでは、各ルールは論理的同値性であるため、これらのルールによる式の書き換えを実行しても、その式の真理値は変わりません。論理における他の有用な書き換えシステムでは、真理値が保持されない場合があります。たとえば、等充足可能性を参照してください。
項書き換えシステムは、自然数に対する算術演算を計算するために使用できます。この目的のために、そのような各数は項としてエンコードする必要があります。最も単純なエンコードは、定数 0 (ゼロ) と後継関数Sに基づくペアノ公理で使用されるものです。たとえば、数 0、1、2、および 3 は、それぞれ項 0、S(0)、S(S(0))、および S(S(S(0))) で表されます。次の項書き換えシステムは、与えられた自然数の和と積を計算するために使用できます。[ 7 ]
例えば、2+2の計算結果が4になるという計算は、項の書き換えによって次のように再現できます。
各矢印の上にある表記は、各書き換えに使用された規則を示しています。
別の例として、2⋅2 の計算は次のようになります。
最後のステップは、前述の計算例で構成される。
言語学において、句構造規則（書き換え規則とも呼ばれる）は、生成文法のいくつかの体系[ 8 ]において、言語の文法的に正しい文を生成する手段として用いられる。このような規則は通常、次のような形式をとる。ここで、Aは名詞句や文などの統語範疇ラベルであり、Xはそのようなラベルまたは形態素のシーケンスであり、文の構成構造を生成する際にAをXに置き換えることができるという事実を表します。例えば、次の規則これは、文が名詞句（NP）の後に動詞句（VP）が続く構成で成り立つことを意味します。さらに、名詞句と動詞句がどのような下位構成要素から成り立つことができるかなど、追加の規則が規定されます。
上記の例から、書き換えシステムを抽象的に考えることができることは明らかです。オブジェクトのセットと、それらを変換するために適用できるルールを指定する必要があります。この概念の最も一般的な（一次元）設定は、抽象還元システム[ 9 ]または抽象書き換えシステム（略称ARS）[ 10 ]と呼ばれます。ARSは、オブジェクトのセットAと、A上の二項関係→ （還元関係、書き換え関係[ 11 ]、または単に還元[ 9 ]と呼ばれる）から構成されます。
ARSの一般的な設定においては、多くの概念や表記法を定義することができる。反射的推移閉包は。は対称閉包である。反射的推移的対称閉包はARS の文章問題は、xとyが与えられたときに、A内のオブジェクトxは、 A内に他のyが存在して、そうでなければ、既約または正規形と呼ばれる。オブジェクトyは、次の場合に「xの正規形」と呼ばれる。、そしてyは既約です。xの正規形が一意である場合、これは通常 で表されます。すべてのオブジェクトが少なくとも 1 つの正規形を持つ場合、ARS は正規化と呼ばれます。または、xとyは、ある性質を持つzが存在する場合に結合可能であると言われます。ARSは、以下の条件を満たす場合にチャーチ・ロッサー財産を保有すると言われます。暗示するARS は、Aのすべてのw、x、yに対して、 暗示するARS が局所的に合流するのは、 Aのすべてのw、x、yに対して、 暗示するARSは、無限連鎖が存在しない場合、終端的またはネーター的であると言われる。合流して終了するARSは、収束型または標準型と呼ばれます。
抽象書き換えシステムに関する重要な定理としては、ARSが合流性を持つのはチャーチ・ロッサー特性を持つ場合のみであること、ニューマンの補題（終端ARSは局所的に合流性を持つ場合に限り合流性を持つ）、そしてARSの単語問題は一般に決定不能であることなどが挙げられる。
文字列書き換えシステム（SRS）、別名セミ・テューシステムでは、アルファベット上の文字列（単語）の自由モノイド構造を利用して書き換え関係を拡張します。、アルファベット内のすべての文字列のうち、いくつかの規則の左辺と右辺を部分文字列として含むものに対して。形式的には、セミ・テューシステムはタプルである。どこは（通常は有限の）アルファベットであり、は、アルファベット内のいくつかの（固定された）文字列間の二項関係であり、書き換え規則の集合と呼ばれる。一段階書き換え関係誘発されるの上は次のように定義されます:文字列であれば、存在する場合そのため、、 そして。 以来関係ペア抽象書き換えシステムの定義に合致する。空文字列は、は、関係がが対称である場合、そのシステムはチューシステムと呼ばれます。
SRSでは、削減関係モノイド演算と互換性がある、つまり暗示するすべての文字列に対して同様に、反射的推移的対称閉包、と表記されるは合同関係であり、定義上同値関係であり、文字列連結とも互換性があります。これは、によって生成されるThue合同と呼ばれます。. チューシステムでは、つまり、対称性があり、書き換え関係トゥーの合同条件と一致する。
半Thueシステムの概念は、本質的にモノイドの提示と一致する。合同式であるため、因子モノイドを定義できます。自由モノイドのトゥエの合同式により。モノイドがは同型であるすると、セミ・トゥーシステムはモノイド表現と呼ばれます。
すぐに代数学の他の分野との非常に有用なつながりがいくつか得られます。例えば、アルファベットルールに従って、 どこは空文字列で、 は1つの生成元上の自由群の表示です。代わりにルールが単にすると、二環式モノイドの表示が得られます。したがって、半テュー系は、モノイドと群の語問題を解決するための自然な枠組みを構成します。実際、すべてのモノイドは、次の形式の表示を持ちます。つまり、それは常に半テューシステムによって表現される可能性があり、場合によっては無限のアルファベット上で表現される可能性がある。
半Thueシステムの単語問題は一般に決定不能である。この結果は、ポストマルコフ定理として知られることがある。[ 12 ]
項書き換えシステム（TRS ）とは、項をオブジェクトとする書き換えシステムであり、項は入れ子になった部分式を持つ式です。例えば、上記の§ ロジックで示されているシステムは項書き換えシステムです。このシステムの項は二項演算子で構成されています。そして単項演算子また、ルールには変数も含まれており、これはあらゆる可能な用語を表します（ただし、単一のルールでは、単一の変数は常に同じ用語を表します）。
文字列書き換えシステムでは対象が記号のシーケンスであるのに対し、項書き換えシステムでは対象が項代数を形成する。項は記号の木として視覚化でき、許容される記号の集合は与えられたシグネチャによって固定される。形式体系として、項書き換えシステムはチューリングマシンと同等の能力を持ち、すなわち、すべての計算可能な関数を項書き換えシステムで定義できる。[ 13 ]
プログラミング言語の中には項書き換えに基づいているものがある。その一例として、数学アプリケーション向けの関数型プログラミング言語である Pure が挙げられる。[ 14 ] [ 15 ]
書き換えルールは、一般的に次のように表記される2つの用語の組です。左辺l を右辺rに置き換えることができることを示す。項書き換えシステムは、このような規則の集合Rである。規則左項l がsの何らかの部分項と一致する場合、つまり何らかの置換がある場合、項sに適用できます。サブタームある位置pに根を置いたものは、置換を適用した結果である。項lに対して。規則の左辺に一致する部分項は、redexまたは還元式と呼ばれます。[ 16 ]この規則の適用結果項t は、 sの位置pの部分項を項で 置き換えた結果です。交代により適用済み、図1参照。この場合、は、 1ステップで書き換えられる、または直接書き換えられると言われている。システムによって正式には、、または一部の著者によって。
用語数ステップで書き換えて、つまり、、 用語書き換えられたと言われている正式には、言い換えれば、関係は関係の推移閉包である; 多くの場合、表記法もは、反射的推移的閉包を表すために用いられる。つまり、もしまたは[ 17 ]集合によって与えられる項の書き換えルールは、上記で定義した抽象的な書き換えシステムと見なすことができ、その対象は用語であり、書き換え関係として。
例えば、は、結合法則に関して正規形を確立するためによく使用される書き換え規則です。その規則は、項の分子に適用できます。一致する置換図2を参照。[注2 ]この置換を規則の右辺に適用すると、次の項が得られる。、そして分子をその項に置き換えると、これは書き換え規則を適用した結果の項です。全体として、書き換え規則を適用することで、「結合法則を適用する」と呼ばれることが達成されます。に初等代数では、この規則は元の項の分母に適用され、。
一般的に書き換えシステムの終了性に関する問題は、「抽象書き換えシステム#終了性と収束」で扱われています。特に項書き換えシステムについては、以下の追加的な注意点を考慮する必要があります。
線形左辺を持つ 1 つのルールからなるシステムの終了性も決定不能である。 [ 18 ] [ 19 ]単項関数記号のみを使用するシステムの場合も終了性は決定不能であるが、有限基底システム の場合は決定可能である。[ 20 ]
次の項書き換えシステムは正規化しますが、[注3 ]停止せず、[注4 ]合流しません。[ 21 ]
終端項書き換えシステムの次の 2 つの例は、Toyama によるものです。[ 22 ]
そして
彼らの結合は、非終了システムです。
この結果は、 2つの終端項書き換えシステムの和集合がそして左辺がすべてそして右側はは線形であり、左辺の間には「重なり」はありません。そして右側は富山氏の例は、これらの性質をすべて満たしている。
項書き換えシステムの停止性証明で使用される順序関係については、 「書き換え順序」および「パス順序（項書き換え）」を参照してください。
高階書き換えシステムは、ラムダ項への一次項書き換えシステムの一般化であり、高階関数と束縛変数を許容します。[ 24 ]一次項書き換えシステムに関するさまざまな結果は、HRSにも再定式化できます。[ 25 ]
グラフ書き換えシステムは、用語書き換えシステムのもう一つの一般化であり、 （基底）用語／それに対応するツリー表現ではなく、グラフ上で動作します。
トレース理論は、トレースモノイドや履歴モノイドなどを用いて、マルチプロセッシングをより形式的に議論する手段を提供する。トレースシステムにおいても書き換えは可能である。
