セミチューシステム

理論計算機科学および数理論理学において、文字列書き換えシステム（SRS ）は、歴史的には半Thueシステムと呼ばれ、(通常は有限の)アルファベットからの文字列に対する書き換えシステムである。二項関係が与えられた場合、${\displaystyle R}$アルファベット上の固定文字列間の書き換えルールは、次のように表される。$s→t$SRSは、ルールの左辺と右辺が部分文字列として現れるすべての文字列に書き換え関係を拡張します。${\displaystyle usv\rightarrow utv}$、 どこ${\displaystyle s}$、${\displaystyle t}$、${\displaystyle u}$、 そして${\displaystyle v}$文字列です。

半テュー系の概念は、本質的にモノイドの表現と一致する。したがって、これらはモノイドと群に関する語問題を解決するための自然な枠組みを構成する。

SRS は、抽象書き換えシステムとして直接定義できます。また、すべての関数シンボルのアリティが最大 1 である制限されたタイプの項書き換えシステムと見なすこともできます。形式体系として、文字列書き換えシステムはチューリング完全です。^{[ 1 ]}セミ チューという名前は、 1914 年の論文で文字列書き換えシステムの体系的な扱いを導入したノルウェーの数学者Axel Thueに由来します。 ^{[ 2 ]} Thue はこの概念を、有限表示半群の単語問題を解決することを期待して導入しました。この問題が決定不能であることが示されたのは 1947 年になってからで、この結果はEmil PostとAA Markov Jr.によって独立に得られました。^{[ 3 ] [ 4 ]}

文字列書き換えシステムまたはセミ・テューシステムはタプルである${\displaystyle (\Sigma ,R)}$どこ

• ${\displaystyle \Sigma }$はアルファベットであり、通常は有限であると仮定される。^{[ 5 ]}集合の要素$\displaystyle \Sigma ^{*}}$(* はここでクリーネ星) は有限 (空文字列の場合もある) 文字列です。${\displaystyle \Sigma }$形式言語では単語と呼ばれることもありますが、ここでは単に文字列と呼びます。
• ${\displaystyle R}$は文字列の二項関係です${\displaystyle \Sigma }$つまり、${\displaystyle R\subseteq \Sigma ^{*}\times \Sigma ^{*}.}$各要素${\displaystyle (u,v)\in R}$これは（書き換え）ルールと呼ばれ、通常は次のように書かれます。${\displaystyle u\rightarrow v}$。

関係が${\displaystyle R}$が対称である場合、そのシステムはチューシステムと呼ばれます。

書き換えルール${\displaystyle R}$他の文字列にも自然に拡張できます$\displaystyle \Sigma ^{*}}$部分文字列を書き換えることを可能にすることで${\displaystyle R}$より厳密には、1段階書き換え関係${\displaystyle {\xrightarrow[{R}]{}}}$誘発される${\displaystyle R}$の上$\displaystyle \Sigma ^{*}}$任意の文字列に対して${\displaystyle s,t\in \Sigma ^{*}}$:

${\displaystyle s{\xrightarrow[{R}]{}}t}$存在する場合に限り${\displaystyle x,y,u,v\in \Sigma ^{*}}$そのため${\displaystyle s=xuy}$、${\displaystyle t=xvy}$、 そして${\displaystyle u\rightarrow v}$。

以来${\displaystyle {\xrightarrow[{R}]{}}}$は関係です${\displaystyle \Sigma ^{*}}$ペア${\displaystyle (\Sigma ^{*},{\xrightarrow[{R}]{}})}$抽象書き換えシステムの定義に合致する。明らかに${\displaystyle R}$は、${\displaystyle {\xrightarrow[{R}]{}}}$. 一部の著者は矢印に別の表記法を使用しています。${\displaystyle {\xrightarrow[{R}]{}}}$（例えば${\displaystyle {\underset {R}{\Rightarrow }}}$) と区別するために${\displaystyle R}$それ自体（${\displaystyle \rightarrow }$なぜなら、後で添え字を削除しても、混乱を避けることができるようにしたいからです。${\displaystyle R}$そして、によって誘発される1ステップの書き換え${\displaystyle R}$。

明らかに、セミ・トゥーシステムでは、初期文字列から始めて、（有限または無限の）文字列のシーケンスを形成できます。${\displaystyle s_{0}\in \Sigma ^{*}}$そして、部分文字列を一つずつ置換しながら繰り返し書き換えていく。

${\displaystyle s_{0}\ {\xrightarrow[{R}]{}}\ s_{1}\ {\xrightarrow[{R}]{}}\ s_{2}\ {\xrightarrow[{R}]{}}\ \ldots }$

このようなゼロステップ以上の書き換えは、反射的推移閉包によって捉えられます。${\displaystyle {\xrightarrow[{R}]{}}}$、で示される${\displaystyle {\xrightarrow[{R}]{*}}}$（抽象書き換えシステム#基本概念を参照）。これは書き換え関係または還元関係と呼ばれます。${\displaystyle \Sigma ^{*}}$誘発される${\displaystyle R}$。

一般的に、セット${\displaystyle \Sigma ^{*}}$アルファベット上の文字列は、文字列連結の二項演算（と表記される）とともに自由モノイドを形成する。${\displaystyle \cdot }$そして、記号を削除して乗法的に記述します。SRSでは、還元関係${\displaystyle {\xrightarrow[{R}]{*}}}$モノイド演算と互換性がある、つまり${\displaystyle x{\xrightarrow[{R}]{*}}y}$暗示する${\displaystyle uxv{\xrightarrow[{R}]{*}}uyv}$すべての文字列に対して${\displaystyle x,y,u,v\in \Sigma ^{*}}$。 以来${\displaystyle {\xrightarrow[{R}]{*}}}$定義上、先行順序である。${\displaystyle \left(\Sigma ^{*},\cdot ,{\xrightarrow[{R}]{*}}\right)}$モノイド前順序を形成する。

同様に、反射的推移的対称閉包${\displaystyle {\xrightarrow[{R}]{}}}$、と表記される${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$（抽象書き換えシステム#基本概念を参照）は合同関係であり、定義上同値関係であり、文字列連結とも互換性があります。${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$これはRによって生成されるThue 合同式と呼ばれます。Thue システム、つまりRが対称である場合、書き換え関係は次のようになります。${\displaystyle {\xrightarrow[{R}]{*}}}$トゥエの合同条件と一致する${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$。

以来${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$合同式であるならば、因子モノイドを定義できる。${\displaystyle {\mathcal {M}}_{R}=\Sigma ^{*}/{\overset {*}{\underset {R}{\leftrightarrow }}}}$自由モノイドの${\displaystyle \Sigma ^{*}}$通常の方法でThue合同式により。モノイドが${\displaystyle {\mathcal {M}}}$は同型である${\displaystyle {\mathcal {M}}_{R}}$すると、セミ・トゥーシステム${\displaystyle (\Sigma ,R)}$はモノイド表現と呼ばれます${\displaystyle {\mathcal {M}}}$。

代数学の他の分野との非常に有用なつながりがすぐに得られます。たとえば、空文字列εを持つ規則 { ab → ε, ba → ε } を持つアルファベット { a , b } は、1 つの生成元上の自由群の表示です。代わりに規則が単に { ab → ε } である場合、双環モノイドの表示が得られます。

モノイドの表現としてのセミ・テュー系の重要性は、以下の点によってさらに強まる。

定理：すべてのモノイドは、次の形式の表現を持つ。${\displaystyle (\Sigma ,R)}$したがって、それは常に半テューシステムによって表現される可能性があり、無限のアルファベット上で表現される可能性がある。^{[ 6 ]}

この文脈では、セット${\displaystyle \Sigma }$は、​${\displaystyle {\mathcal {M}}}$、 そして${\displaystyle R}$定義関係の集合と呼ばれる${\displaystyle {\mathcal {M}}}$モノイドは、その表示に基づいてすぐに分類できます。${\displaystyle {\mathcal {M}}}$と呼ばれる

• 有限生成の場合${\displaystyle \Sigma }$有限である。
• 有限表示可能${\displaystyle \Sigma }$そして${\displaystyle R}$有限である。

ポストは、チューリングマシンの停止問題^{[ 7 ]}を単語問題の一例に還元することによって、（半群の）単語問題が一般に決定不能であることを証明した（ポストの対応問題を参照）。

具体的には、ポストはチューリングマシンの状態とテープを有限文字列として符号化する方法を考案し、この文字列符号化に対して作用する文字列書き換えシステムによって、このマシンの動作を実行できるようにした。この符号化のアルファベットは1組の文字から構成される。${\displaystyle S_{0},S_{1},\dotsc ,S_{m}}$テープ上のシンボルについて（${\displaystyle S_{0}}$（空白を意味する）、別の文字のセット${\displaystyle q_{1},\dotsc ,q_{r}}$チューリングマシンの状態を表す記号、そして最後に3文字${\displaystyle q_{r+1},q_{r+2},h}$それらは符号化において特別な役割を担っている。${\displaystyle q_{r+1}}$そして${\displaystyle q_{r+2}}$は、チューリングマシンが停止したときに遷移する直感的に追加の内部状態であるが、${\displaystyle h}$テープの空白でない部分の終わりを示します。機械が${\displaystyle h}$そこに空白がある場合と同じように動作するはずであり、${\displaystyle h}$次のセルにありました。チューリングマシンの状態の有効なエンコードである文字列は、${\displaystyle h}$、続いて0個以上の記号文字、続いてちょうど1つの内部状態文字${\displaystyle q_{i}}$（機械の状態を符号化する）に続いて1つ以上の記号文字、最後に終了文字が続く${\displaystyle h}$記号文字はテープの内容からそのまま引用されており、内部状態文字はヘッドの位置を示しています。内部状態文字の後の記号は、チューリングマシンのヘッドの下にあるセル内の記号です。

機械が状態にあるときに遷移する${\displaystyle q_{i}}$そしてそのシンボルを見る${\displaystyle S_{k}}$シンボルを書き戻す${\displaystyle S_{l}}$右に移動し、状態に移行します${\displaystyle q_{j}}$書き換えによって実装される

${\displaystyle q_{i}S_{k}\to S_{l}q_{j}}$

一方、左へ移動する遷移は書き換えによって実装される

${\displaystyle S_{p}q_{i}S_{k}\to q_{j}S_{p}S_{l}}$

各シンボルにつき1つのインスタンス${\displaystyle S_{p}}$左側のセルで。テープの訪問済み部分の終わりに達した場合は、代わりに

${\displaystyle hq_{i}S_{k}\to hq_{j}S_{0}S_{l}}$、

文字列を1文字長くする。すべての書き換えには1つの内部状態文字が含まれるため。${\displaystyle q_{i}}$有効な符号化にはそのような文字が1つしか含まれておらず、各書き換えによって生成される文字も正確に1つだけであるため、書き換えプロセスは符号化されたチューリングマシンの実行と完全に一致する。これは、文字列書き換えシステムがチューリング完全であることを証明する。

停止記号が2つある理由${\displaystyle q_{r+1}}$そして${\displaystyle q_{r+2}}$我々が望むのは、停止するすべてのチューリングマシンが特定の内部状態だけでなく、同じ全体状態で終了することです。これには停止後にテープをクリアする必要があるため、${\displaystyle q_{r+1}}$左側のシンボルを食べ、${\displaystyle h}$そこから${\displaystyle q_{r+2}}$代わりに、右側の記号が消費されます。（この段階では、文字列書き換えシステムはチューリングマシンをシミュレートしなくなります。チューリングマシンはテープからセルを取り出すことができないためです。）すべての記号がなくなると、終端文字列に到達します。${\displaystyle hq_{r+2}h}$。

単語問題に対する判定手順は、特定の全状態から開始されたチューリングマシンが終了するかどうかを判定する手順も生み出すことになる。${\displaystyle t}$をテストすることによって${\displaystyle t}$そして${\displaystyle hq_{r+2}h}$これらは、この文字列書き換えシステムに関して同じ合同クラスに属します。技術的には、次のようになります。

補題。${\displaystyle M}$決定論的チューリングマシンであり、${\displaystyle R}$文字列書き換えシステムを実装する${\displaystyle M}$上記のとおりです。${\displaystyle M}$エンコードされた全状態から開始すると停止します${\displaystyle t}$かつその場合に限り${\displaystyle t\mathrel {\overset {*}{\underset {R}{\leftrightarrow }}} hq_{r+2}h}$（つまり、${\displaystyle t}$そして${\displaystyle hq_{r+2}h}$Thue は合同です${\displaystyle R}$)

それ${\displaystyle t\mathrel {\overset {*}{\underset {R}{\rightarrow }}} hq_{r+2}h}$もし${\displaystyle M}$開始時に停止します${\displaystyle t}$建設からすぐに${\displaystyle R}$（単に走る）${\displaystyle M}$停止するまで証明を構築します${\displaystyle t\mathrel {\overset {*}{\underset {R}{\rightarrow }}} hq_{r+2}h}$）、 しかし${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$チューリングマシンも可能${\displaystyle M}$後退する。ここで重要なのは、${\displaystyle M}$決定論的である。なぜなら、前進ステップはすべて一意だからである。${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$歩いて${\displaystyle t}$に${\displaystyle hq_{r+2}h}$最後の後退ステップの後には、対応する前進ステップが続く必要があるため、これら2つは相殺され、帰納法により、そのような歩行からすべての後退ステップを排除することができます。したがって、${\displaystyle M}$開始時に停止しない${\displaystyle t}$つまり、もし私たちが持っていないなら${\displaystyle t\mathrel {\overset {*}{\underset {R}{\rightarrow }}} hq_{r+2}h}$そうすれば、私たちにも${\displaystyle t\mathrel {\overset {*}{\underset {R}{\leftrightarrow }}} hq_{r+2}h}$したがって、決定する${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$停止問題の答えを教えてくれる${\displaystyle M}$。

この議論の明らかな限界は、半群を生成するために${\displaystyle \Sigma ^{*}{\big /}{\overset {*}{\underset {R}{\leftrightarrow }}}}$決定不能な単語問題では、まずチューリングマシンの具体的な例を用意する必要がある。${\displaystyle M}$停止問題が決定不能なチューリングマシンは存在するが、一般的な停止問題の決定不能性の証明に登場する様々なチューリングマシンはすべて、停止問題を解く仮想のチューリングマシンを構成要素として持っているため、それらのマシンは実際には存在し得ない。証明されるのは、決定問題が決定不能なチューリングマシンが存在するということだけである。しかし、停止問題が決定不能なチューリングマシンが存在するということは、普遍チューリングマシンの停止問題も決定不能であることを意味し（普遍チューリングマシンは任意のチューリングマシンをシミュレートできるため）、普遍チューリングマシンの具体的な例が構築されている。

セミ・テュー・システムもまた項書き換えシステムであり、左辺と右辺の項と同じ変数で終わる単項語（関数）を持つシステムである^{[ 8 ]。}例えば項規則など。${\displaystyle f_{2}(f_{1}(x))\rightarrow g(x)}$文字列ルールと同等${\displaystyle f_{1}f_{2}\rightarrow g}$。

半Thueシステムはポストカノニカルシステムの特殊なタイプでもあるが、すべてのポストカノニカルシステムはSRSに還元することもできる。どちらの形式体系もチューリング完全であり、したがってノーム・チョムスキーの非制限文法（半Thue文法と呼ばれることもある）と同等である。^{[ 9 ]}形式文法は、アルファベットを終端記号と非終端記号に分離し、非終端記号の中に開始記号を固定するという点で、半Thueシステムと異なる。少数の著者は、半Thueシステムを実際には3つ組として定義している。${\displaystyle (\Sigma ,A,R)}$、 どこ${\displaystyle A\subseteq \Sigma ^{*}}$は公理の集合と呼ばれます。この「生成」的な半テュー体系の定義の下では、無制限文法は、アルファベットを終端記号と非終端記号に分割し、公理を非終端記号とする単一の公理を持つ半テュー体系にすぎません。^{[ 10 ]}アルファベットを終端記号と非終端記号に分割するという単純な技巧は強力です。これにより、規則に含まれる終端記号と非終端記号の組み合わせに基づいてチョムスキー階層を定義することができます。これは形式言語理論における重要な発展でした。

量子コンピューティングでは、量子Thueシステムの概念を発展させることができる。^{[ 11 ]} 量子計算は本質的に可逆であるため、書き換え規則はアルファベットに対して適用される。${\displaystyle \Sigma }$双方向である必要があります（つまり、基盤となるシステムはThueシステムであり、セミThueシステムではありません）。アルファベット文字のサブセットについて${\displaystyle Q\subseteq \Sigma }$ヒルベルト空間を付加することができる${\displaystyle \mathbb {C} ^{d}}$また、部分文字列を別の部分文字列に変換する書き換え規則は、文字列に付随するヒルベルト空間のテンソル積に対してユニタリ演算を実行できます。これは、文字列が元の文字列セットの文字数を保持することを意味します。${\displaystyle Q}$古典的な場合と同様に、量子チューシステムは量子計算のための普遍的な計算モデルであることを示すことができる。これは、実行される量子操作が均一な回路クラス（例えば、入力サイズに対して多項式回数ステップ内で文字列書き換え規則の終了を保証するBQPの場合など）に対応する、あるいは同等に量子チューリングマシンに対応するという意味である。

セミ・チューシステムは、論理に新たな構成要素を追加し、命題論理のようなシステムを構築するためのプログラムの一環として開発されました。これにより、一般的な数学定理を形式言語で表現し、自動的かつ機械的に証明・検証することが可能になります。定理証明の行為は、一連の文字列に対する一連の定義済み操作に還元できると期待されていました。その後、セミ・チューシステムは無制限文法と同型であり、無制限文法はチューリングマシンと同型であることが認識されました。この研究方法は成功し、現在ではコンピュータを用いて数学的および論理的定理の証明を検証することが可能になっています。

アロンゾ・チャーチの提案により、エミール・ポストは1947年に発表した論文で、「あるチューの問題」が解けないことを初めて証明した。マーティン・デイビスはこれを「古典数学の問題に対する最初の解けないことの証明、この場合は半群の語の問題」と述べている。^{[ 12 ]}

デイビスはまた、その証明はAAマルコフによって独自に提示されたと主張している。^{[ 13 ]}

• Lシステム
• マルコフアルゴリズム―文字列書き換えシステムの変種
• MUパズル