文章問題（数学）

計算数学において、語問題とは、与えられた 2 つの式が書き換え恒等式の集合に関して同値であるかどうかを判定する問題である。典型的な例は群の語問題であるが、他にも多くの例がある。計算理論のいくつかの重要な結果は、多くの重要なケースでこの問題が決定不可能であることに関係している。^{[ 1 ]}

コンピュータ代数では、数式を式木を使って符号化したい場合がよくあります。しかし、多くの場合、同等の式木が複数存在します。そこで、2つの式を入力として与えられたときに、それらが同じ要素を表しているかどうかを判定するアルゴリズムが存在するかどうかという疑問が自然に生じます。このようなアルゴリズムは、単語問題の解と呼ばれます。例えば、次のような場合を考えてみましょう。${\displaystyle x,y,z}$は実数を表す記号です。入力が与えられた場合、単語問題に対する適切な解決策は次のようになります。${\displaystyle (x\cdot y)/z\mathrel {\overset {?}{=}} (x/z)\cdot y}$出力を生成しEQUAL、同様NOT_EQUALにから生成する${\displaystyle (x\cdot y)/z\mathrel {\overset {?}{=}} (x/x)\cdot y}$。

語句問題に対する最も直接的な解決策は、正規形定理とアルゴリズムの形をとります。これは、式の同値類のすべての要素を正規形と呼ばれる単一の符号化にマッピングし、構文的等価性によってこれらの正規形を比較することで語句問題を解決します。^{[ 1 ]}例えば、次のように判断するかもしれません。${\displaystyle x\cdot y\cdot z^{-1}}$は標準形です${\displaystyle (x\cdot y)/z}$、${\displaystyle (x/z)\cdot y}$、 そして${\displaystyle (y/z)\cdot x}$そして、それらの式をその形式に書き換える変換システムを考案し、その過程で、すべての同等の式が同じ正規形に書き換えられることを証明する。^{[ 2 ]}しかし、この文章問題の解法はすべて正規形定理を使用しているわけではなく、アルゴリズムの存在を間接的に示唆する代数的性質が存在する。^{[ 1 ]}

単語問題は定数を含む 2 つの項が等しいかどうかを問うものですが、統一問題として知られる単語問題の適切な拡張では、2 つの項が等しいかどうかを問うものです。$t_1,t_2$含まれる変数には等しいインスタンスがある、言い換えれば方程式が$t_1=t_2$解決策はありますか。一般的な例として、${\displaystyle 2+3\mathrel {\overset {?}{=}} 8+(-3)}$は整数群の文章問題です${\displaystyle \mathbb {Z} }$、 その間${\displaystyle 2+x\mathrel {\overset {?}{=}} 8+(-x)}$これは同じグループ内の統一問題です。前の項はたまたま等しいので${\displaystyle \mathbb {Z} }$後者の問題では、置換が行われます。${\displaystyle \{x\mapsto 3\}}$解決策として。

語の問題で最も深く研究されているケースの 1 つは、半群と群の理論です。ノビコフ・ブーンの定理に関連する論文のタイムラインは次のとおりです。^{[ 3 ] [ 4 ]}

• 1910年 （1910年）：アクセル・トゥーは、木構造上の項書き換えの一般的な問題を提起した。彼は「最も一般的な場合におけるこの問題の解決は、おそらく克服不可能な困難を伴うだろう」と述べている。^{[ 5 ] [ 6 ]}
• 1911年 （1911年）：マックス・デーンは有限表示群の語問題を提起した。^{[ 7 ]}
• 1912年 ( 1912 ) :デーンがデーンのアルゴリズムを発表し、種数が2以上の閉じた向き付け可能な2次元多様体の基本群の単語問題を解決することを証明した。 ^{[ 8 ]}後続の著者は、これを群論的決定問題の幅広い範囲に大幅に拡張した。 ^{[ 9 ] [ 10 ] [ 11 ]}
• 1914年 （1914年）：アクセル・トゥーは有限表示半群の語問題を提起した。^{[ 12 ]}
• 1930年 （1930年） ～1938年 （1938年）：計算可能性と決定不能性の形式的概念を定義するチャーチ＝チューリングのテーゼが登場する。^{[ 13 ]}
• 1947年 （1947）：エミール・ポストとアンドレイ・マルコフ・ジュニアは、それぞれ独立に、解けない語問題を持つ有限表示半群を構成した。^{[ 14 ] [ 15 ]}ポストの構成はチューリングマシンに基づいているのに対し、マルコフの構成はポストの正規システムを使用している。^{[ 3 ]}
• 1950年 （1950）：アラン・チューリングは、ポストの構成法をさらに発展させることで、消去半群の語問題は解けないことを示した^{[ 16 ]}。証明は理解しにくいが、群の語問題における転換点となった^{[ 3 ]： 342}
• 1955年 （1955）：ピョートル・ノヴィコフは、チューリングの半群消去結果を用いて、群の語問題が解けないことを初めて公表した証明を与えた。^{[ 17 ] [ 3 ]： 354}この証明には、ブリットンの補題と同等の「主補題」が含まれている。^{[ 3 ]： 355}
• 1954年 （1954年） ～1957年 （1957年）：ウィリアム・ブーンは、ポストの半群構成を用いて、群に関する語句問題は解けないことを独自に示した。^{[ 18 ] [ 19 ]}
• 1957年 （1957年） －1958年 （1958年）：ジョン・ブリットンは、チューリングの半群の消去結果とブリットン自身の初期の研究に基づいて、群の語問題が解けないことを別の形で証明した。^{[ 20 ]}ブリットンの補題の初期バージョンが登場する。^{[ 3 ]： 355}
• 1958年 （1958年） ～1959年 （1959年）：ブーンは自身の構成の簡略版を発表した。^{[ 21 ] [ 22 ]}
• 1961年 （1961）：グラハム・ヒグマンは、ヒグマンの埋め込み定理^{[ 23 ]}を用いて有限表示群の部分群を特徴づけ、再帰理論と群論を予想外の方法で結びつけ、語問題の解決不可能性について全く異なる証明を与えた。^{[ 3 ]}
• 1961年 （1961年） ～1963年 （1963年）：ブリットンは、群の語問題は解けないというブーンの1959年の証明を大幅に簡略化したバージョンを発表した。^{[ 24 ]}これは群論的アプローチ、特にブリットンの補題を使用している。この証明は大学院の講義で使用されているが、より現代的で簡潔な証明も存在する。^{[ 25 ]}
• 1977年 （1977）：ゲンナジー・マカニンは、自由モノイド上の方程式の存在理論が解けることを証明した。^{[ 26 ]}

文字列書き換えシステム（半テューシステムまたは半群）のアクセス可能性問題は次のように述べることができる。${\displaystyle T:=(\Sigma ,R)}$そして2つの単語（文字列）${\displaystyle u,v\in \Sigma ^{*}}$、 できる${\displaystyle u}$に変化する${\displaystyle v}$ルールを適用することによって${\displaystyle R}$? ここでの書き換えは一方向であることに注意してください。単語の問題は、対称書き換え関係、つまりThueシステムに対するアクセス可能性の問題です。^{[ 27 ]}

アクセシビリティ問題と単語問題は決定不能であり、つまり、この問題を解決するための一般的なアルゴリズムは存在しない。^{[ 28 ]}これは、システムを有限表現、つまり有限個の記号とそれらの記号上の有限個の関係に限定した場合でも成り立つ。^{[ 27 ]}基底項に限定された単語問題でさえ、特定の有限表現半群に対しては決定不能である。^{[ 29 ] [ 30 ]}

プレゼンテーションを受ける${\displaystyle \langle S\mid {\mathcal {R}}\rangle }$群Gの場合、単語問題とは、入力として与えられたS内の 2 つの単語がGの同じ要素を表しているかどうかを判定するアルゴリズム問題です。単語問題は、 1911 年にMax Dehnによって提案された群に関する 3 つのアルゴリズム問題の 1 つです。1955年にPyotr Novikovによって、 Gの単語問題が決定不能となるような有限表示群Gが存在することが示されました。^{[ 31 ]}

単語問題が決定不能であることの最も初期の証明の 1 つは組み合わせ論理に関するものでした。2 つのコンビネータ列が等価になるのはどのような場合でしょうか? コンビネータはすべての可能なチューリング マシンを符号化し、2 つのチューリング マシンの等価性は決定不能であるため、2 つのコンビネータ列の等価性も決定不能であることがわかります。アロンゾ チャーチは1936 年にこのことを指摘しました。 ^{[ 32 ]}

同様に、（型なし）ラムダ計算においても本質的に同じ問題が生じる。すなわち、2つの異なるラムダ式が与えられた場合、それらが等価であるか否かを判別できるアルゴリズムは存在しない。等価性は判定不能である。ただし、いくつかの型付きラムダ計算においては、正規形の比較によって等価性を判定できる。

抽象書き換えシステム（ARS）の単語問題は非常に簡潔です。オブジェクトxとyが与えられたとき、それらは以下の条件の下で同等でしょうか。${\displaystyle {\stackrel {*}{\leftrightarrow }}}$[ ^{29 ]} ARSの単語問題は一般には決定不能である。しかし、すべてのオブジェクト^が有限ステップで一意の正規形に還元される（つまりシステムが収束する）特定の場合には、単語問題の計算可能な解が存在する。2つのオブジェクトは、以下の条件の下で同等である。${\displaystyle {\stackrel {*}{\leftrightarrow }}}$それらが同じ正規形に還元される場合に限ります。^{[ 33 ]} クヌース・ベンディックス補完アルゴリズムは、一連の方程式を収束項書き換えシステムに変換するために使用できます。

普遍代数では、生成集合A 、 A上の有限アリティの演算の集合、およびこれらの演算が満たさなければならない有限個の恒等式の集合からなる代数構造を研究します。代数に関する語句問題は、生成元と演算を含む 2 つの式 (語句) が与えられたときに、それらが恒等式を法として代数の同じ要素を表しているかどうかを判定することです。群と半群に関する語句問題は、代数に関する語句問題として表現できます。^{[ 1 ]}

自由ハイティング代数に関する語句問題は難しい。^{[ 34 ]} 知られている唯一の結果は、1 つの生成元上の自由ハイティング代数は無限であること、および 1 つの生成元上の自由完全ハイティング代数が存在すること（そして自由ハイティング代数よりも 1 つ多い要素を持つこと）である。

自由束、より一般的には自由有界束における語句問題には、決定可能な解が存在する。有界束は、2 つの二項演算∨ と ∧、および 2 つの定数 (零項演算) 0 と 1 を持つ代数構造である。与えられた生成元集合Xの要素に対してこれらの演算を用いて定式化できるすべての整形式の式の集合をW ( X )と呼ぶ。この語句の集合には、どの束においても等しい値を表す式が多数含まれている。例えば、aがXの要素である場合、a ∨ 1 = 1 およびa ∧ 1 = aとなる。自由有界束における語句問題とは、W ( X ) のこれらの要素のうちどれが自由有界束FXにおいて、ひいてはすべての有界束において同じ要素を表すかを決定する問題である。

語句の問題は次のように解決できます。W ( X )上の関係 ≤ _~は、以下のいずれかが成り立つ場合に限りw ≤ _~ vと設定することにより帰納的に定義できます。

1.  w = v (これは、 wとv がXの要素である場合に限定できます)、
2.  w = 0、
3.  v = 1、
4.  w = w ₁ ∨ w _2かつw ₁ ≤ _~ vおよびw ₂ ≤ _~ vの両方が成り立つ。
5.  w = w ₁ ∧ w _2かつw ₁ ≤ _~ vまたはw ₂ ≤ _~ vのいずれかが成り立つ。
6.  v = v ₁ ∨ v ₂かつw ≤ _~ v ₁またはw ≤ _~ v ₂のいずれかが成り立つ。
7.  v = v ₁ ∧ v _{2であり、} w ≤ _~ v ₁およびw ≤ _~ v ₂の両方が成り立つ。

これはW ( X )上に前順序≤ _~を定義するので、同値関係はw ≤ _~ vかつv ≤ _~ wの場合にw ~ vによって定義できます。次に、部分的に順序付けられた商集合W ( X )/~ が自由有界束FXであることを示すことができます。^{[ 35 ] [ 36 ]} W ( X )/~の同値類は、 w ≤ _~ vかつv ≤ _~ wであるすべての単語wとvの集合です。W ( X )内の2 つの整形式単語vとw は、 w ≤ _~ vかつv ≤ _~ wの場合に限り、すべての有界束で同じ値を表します。後者の条件は、上記の帰納的定義を使用して効果的に決定できます。表は、単語x ∧ zとx ∧ z ∧( x ∨ y ) がすべての有界束で同じ値を表すことを示す計算例を示しています。有界でない格子の場合も同様に扱われ、上記の ≤ _~の構成における規則 2 と 3 は省略されます。

BläsiusとBürckert ^{[ 37 ]}は、群の公理集合上でKnuth–Bendixアルゴリズム を実証した。このアルゴリズムは、すべての項を一意の正規形に変換する、合流的でネーター的な項書き換えシステムを生成する^{[ 38 ]}。 書き換え規則は、アルゴリズムの実行中に冗長になった規則が削除されたため、連続していない番号が付けられている。2つの項の等価性は、両方の項が文字通り同じ正規形項に変換される場合に限り、公理から導かれる。例えば、次の項は、

${\displaystyle ((a^{-1}\cdot a)\cdot (b\cdot b^{-1}))^{-1}\mathrel {\overset {R2}{\rightsquigarrow }} (1\cdot (b\cdot b^{-1}))^{-1}\mathrel {\overset {R13}{\rightsquigarrow }} (1\cdot 1)^{-1}\mathrel {\overset {R1}{\rightsquigarrow }} 1^{-1}\mathrel {\overset {R8}{\rightsquigarrow }} 1}$、 そして

${\displaystyle b\cdot ((a\cdot b)^{-1}\cdot a)\mathrel {\overset {R17}{\rightsquigarrow }} b\cdot ((b^{-1}\cdot a^{-1})\cdot a)\mathrel {\overset {R3}{\rightsquigarrow }} b\cdot (b^{-1}\cdot (a^{-1}\cdot a))\mathrel {\overset {R2}{\rightsquigarrow }} b\cdot (b^{-1}\cdot 1)\mathrel {\overset {R11}{\rightsquigarrow }} b\cdot b^{-1}\mathrel {\overset {R13}{\rightsquigarrow }} 1}$

同じ正規形を共有する。${\displaystyle 1}$;したがって、両方の項はどのグループでも等しい。別の例として、項${\displaystyle 1\cdot (a\cdot b)}$そして${\displaystyle b\cdot (1\cdot a)}$通常の形式を持つ${\displaystyle a\cdot b}$そして${\displaystyle b\cdot a}$それぞれ、正規形は文字通り異なるため、元の項はすべての群で等しくなることはありません。実際、非可換群では通常異なります。

• 共役問題
• 群同型性の問題