ニューマンの補題

理論計算機科学、特に項書き換えにおいて、ニューマンの補題（一般にダイヤモンド補題とも呼ばれる）は、抽象書き換えシステムが合流性を持つことを証明するための基準である。この補題は、システムが終了性を持つ場合、局所的な合流性が合流性の十分条件であることを述べている。局所的な合流性は、通常、合流性よりも検証しやすいため、これは有用である。

この補題はもともと1942年にマックス・ニューマンによって証明されました。 ^{[ 1 ]}^{[ 2 ]}ジェラール・ユエは、より簡潔な証明（以下に示す）を提案しました。^{[ 3 ]}他にも多くの証明が存在します。^{[ 4 ]}

声明と証拠

この補題は純粋に組み合わせ論的なものであり、あらゆる関係に適用できます。一般的に適用される文脈を考慮して、以下では抽象書き換えシステムの用語で記述します（これは単に、要素が項と呼ばれる集合であり、関係を備えています）。 $\to$ 還元と呼ばれる（終結、合流、局所合流、正規形の定義については、対応する記事を参照のこと）。

ニューマンの補題（^[⁵^]^[⁶^]^[⁷^]^[⁸^]）—抽象書き換えシステムが停止し、かつ局所的に合流性を持つならば、それは合流性であり、すべての項は一意の正規形を持つ。

証拠

なぜなら $\to$ 終了するので、に根拠のある帰納法を実行できます $u$ 平行 $\to$ 我々は、すべての図が

{\displaystyle u\to ^{*}v,u\to ^{*}w} — 矢印付き図 $u\to ^{*}v,u\to ^{*}w$ （矢印は点線で示されているが、これは任意の数の還元ステップのシーケンスを表している。）

図に拡張できる

{\displaystyle u\to ^{*}v\to ^{*}t,u\to ^{*}w\to ^{*}t} — 矢印付き図 $u\to ^{*}v\to ^{*}t,u\to ^{*}w\to ^{*}t$

ここで、点線の矢印は、任意の数の還元のシーケンスを表します。 $\to$ 。

基本ケース: もし $u=v$ または $u=w$ これは些細なことだ。

帰納的ステップ：そうでない場合、各辺に少なくとも1つの還元があります。

{\displaystyle u\to v_{0}\to ^{*}v,u\to w_{0}\to ^{*}w} — alt=矢印付き図 $u\to v_{0}\to ^{*}v,u\to w_{0}\to ^{*}w$

局所的な合流により、この図は以下のように拡張できます。

{\displaystyle u\to v_{0}\to ^{*}v,u\to w_{0}\to ^{*}w,v_{0}\to ^{*}t,w_{0}\to ^{*}t} — alt=矢印付き図 $u\to v_{0}\to ^{*}v,u\to w_{0}\to ^{*}w,v_{0}\to ^{*}t,w_{0}\to ^{*}t$

そして帰納仮説により $v_{0}$ :

{\displaystyle u\to v_{0}\to ^{*}v\to ^{*}v_{1},u\to w_{0}\to ^{*}t\to ^{*}v_{1},v_{0}\to ^{*}t,w_{0}\to ^{*}w} — alt=矢印付き図 $u\to v_{0}\to ^{*}v\to ^{*}v_{1},u\to w_{0}\to ^{*}t\to ^{*}v_{1},v_{0}\to ^{*}t,w_{0}\to ^{*}w$

そして最後に、帰納仮説によって $w_{0}$ :

{\displaystyle u\to v_{0}\to ^{*}v\to ^{*}v_{1}\to ^{*}w_{1},u\to w_{0}\to ^{*}t\to ^{*}v_{1},v_{0}\to ^{*}t,w_{0}\to ^{*}w\to ^{*}w_{1}} — alt=矢印付き図 $u\to v_{0}\to ^{*}v\to ^{*}v_{1}\to ^{*}w_{1},u\to w_{0}\to ^{*}t\to ^{*}v_{1},v_{0}\to ^{*}t,w_{0}\to ^{*}w\to ^{*}w_{1}$

エリクソンの多角形性質補題

関連する結果は、1993 年に Kimmo Eriksson によって示されました。^{[ 9 ]}^{[ 10 ]} 抽象書き換えシステムは、任意の 2 つの還元に対して、 $a\to b$ そして $a\to c$ 存在する $d$ そのため $b\to ^{*}d$ そして $c\to ^{*}d$ さらに、還元チェーンが必要とされる場合 $b\to ^{*}d$ そして $c\to ^{*}d$ 長さが同じである場合、そのシステムは多角形特性を持つと言われます。多角形特性を持つ書き換えシステムの例としては、バブルソートやチップ発射ゲームなどがあります。

エリクソンの多角形特性補題（^[⁹^]^[¹⁰^]）—抽象書き換えシステムが終了し、多角形特性を持つ場合、それは合流的であり、与えられた状態からの終了する還元チェーンはすべて同じ長さになります。

証拠

ニューマンの補題により、システムは合流性であり、すべての要素は一意の正規形を持つ。各要素について $u$ 、定義する $rl(u)$ 最短還元鎖の長さは $u$ 通常の形態に戻す。

入学 $rl(u)$ 。もし $rl(u)=0$ 、それから $u$ は既に通常の形式です。そうでない場合は、 $rl(u)\geq 1$ そして、多角形の性質と帰納法の仮説を適用する。

参考文献

↑ニューマン、マックス（1942）。「同値性の組み合わせ論的定義による理論について」「.数学年報. 43 (2): 223– 243.
↑ van Oostrom, Vincent. 「ニューマンの補題のニューマンによる証明」（PDF）。 2024年4月15日にオリジナル（PDF）からアーカイブされました。
↑ Huet, Gérard (1980). "合流的還元: 抽象特性と項書き換えシステムへの応用" . Journal of the ACM . 27 (4): 797– 821. doi : 10.1145/322217.322230 .
↑ Klop, Jan Willem (1990). "項書き換えシステム：チャーチ＝ロッサーからクヌース＝ベンディックス、そしてその先へ".オートマタ、言語、プログラミング：第17回国際コロキウム. Lecture Notes in Computer Science . Vol. 443. ウォーリック大学、イギリス：Springer. pp. 350–369 . doi : 10.1007/BFb0032044 . ISBN 978-3-540-52826-5。
↑ Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That . Cambridge University Press. doi : 10.1017/CBO9781139172752 . ISBN 0-521-77920-0。
↑ Terese (2003). Term Rewriting Systems . Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
↑ハリソン、ジョン（2009）。実践論理と自動推論のハンドブック。ケンブリッジ大学出版局。p. 260。ISBN 978-0-521-89957-4。
↑コーン、ポール・モリッツ( 1980 )。普遍代数。D. ライデル出版。pp. 25–26。ISBN 90-277-1254-9。
1 2エリクソン、キンモ (1993)。強収束ゲームとコクセター群(Takn.dr 論文)。ストックホルム: KTH。
1 2 Eriksson, Kimmo (1996). "強い収束と数のゲーム". European Journal of Combinatorics . 17 (4): 379–390 . doi : 10.1006/eujc.1996.0031 .

外部リンク

PlanetMathのダイヤモンド補題。

[newman-1] ニューマン、マックス（1942）。「同値性の組み合わせ論的定義による理論について」「.数学年報. 43 (2): 223– 243.

[van-oostrom-2] van Oostrom, Vincent. 「ニューマンの補題のニューマンによる証明」（PDF）。 2024年4月15日にオリジナル（PDF）からアーカイブされました。

[huet-3] Huet, Gérard (1980). "合流的還元: 抽象特性と項書き換えシステムへの応用" . Journal of the ACM . 27 (4): 797– 821. doi : 10.1145/322217.322230 .

[klop-4] Klop, Jan Willem (1990). "項書き換えシステム：チャーチ＝ロッサーからクヌース＝ベンディックス、そしてその先へ".オートマタ、言語、プログラミング：第17回国際コロキウム. Lecture Notes in Computer Science . Vol. 443. ウォーリック大学、イギリス：Springer. pp. 350–369 . doi : 10.1007/BFb0032044 . ISBN 978-3-540-52826-5。

[trat-5] Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That . Cambridge University Press. doi : 10.1017/CBO9781139172752 . ISBN 0-521-77920-0。

[terese-6] Terese (2003). Term Rewriting Systems . Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.

[harrison-7] ハリソン、ジョン（2009）。実践論理と自動推論のハンドブック。ケンブリッジ大学出版局。p. 260。ISBN 978-0-521-89957-4。

[cohn-8] コーン、ポール・モリッツ( 1980 )。普遍代数。D. ライデル出版。pp. 25–26。ISBN 90-277-1254-9。

[eriksson-thesis-9] 1 2エリクソン、キンモ (1993)。強収束ゲームとコクセター群(Takn.dr 論文)。ストックホルム: KTH。

[eriksson-journal-10] 1 2 Eriksson, Kimmo (1996). "強い収束と数のゲーム". European Journal of Combinatorics . 17 (4): 379–390 . doi : 10.1006/eujc.1996.0031 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[

[

[

[

[ 9 ]

[ 10 ]

声明と証拠

エリクソンの多角形性質補題

参考文献

外部リンク

関連するトピック

計算機科学

項書き換え

抽象書き換えシステムが

性を持つ