一般マグマの多項式の完備化
環の演算では書き換え規則の合成を行っているので、今までの議論で説明できるのですが、その説明では長くなるのでいったん
群の完備化の説明をしたいと思います。
群の完備化ではクヌース・ベンディックス完備化アルゴリズム - Wikipediaと同様のことをやろうとしているのですが、自動的にできるようになっているわけではないので環の演算とほぼ同様のやり方になっています。
クヌース・ベンディックス完備化アルゴリズム - Wikipediaでは等式の有限集合 から完備な書き換え規則の有限集合 を作る半アルゴリズムについて書かれています。しかし詳細は書かれていないようなので少し付け加えて説明を書いてみたいと思います。
書き換え規則の合成の記法
以前の記事で使った書き換え規則の合成の記法をここでも使います(少しわかりにくい気がしますが変更するとややこしくなるのでこのまま使うことにします)。
書き換え規則 に対して、 の部分項の位置全体の集合を 、 の部分項の位置全体の集合を とします。
書き換え規則の集合 と に対して と定義します。 のとき 、 のとき 、、 のとき のように書きます。任意の項 を に写す「恒等」書き換え規則を とし(後で と書くこともあります)、書き換え規則の集合 に対して \begin{cases}
R^0 & = & \{1\} \\
R^{n+1} & = & R^n \cdot R \\
\end{cases} と定義します。 と定義します。
書き換え規則 に対して、 とします。書き換え規則の集合 に対して とします。 が成り立ちます。 に対して とします。
完備化アルゴリズム
ここから「恒等」書き換え規則を と書きます。書き換え規則を等式と考えることができます。書き換え規則 を等式として見たものを とします。
、 とし、等式の有限集合の列 、書き換え規則の有限集合の列 、等式の列 () を以下のように帰納的に作ります( は任意の元で良い)。\begin{cases}
R_{n+1} & = & (R_n \cup rr(e_n \downarrow_{R_n})) \setminus \{0\} & (e_n \in E_n) \\
R_{n+1} & = & ⊥ & (E_n = \varnothing) \\
\end{cases} \begin{cases}
E_{n+1} & = & (E_n \setminus \{e_n\}) \cup (cp(R_{n+1}) \setminus cp(R_{n})) & (E_n \ne \varnothing) \\
E_{n+1} & = & \varnothing & (E_n = \varnothing) \\
\end{cases} のときは とします。
項全体の集合 は整列集合(任意の空ではない部分集合が最小元をもつ全順序集合)であるとします( という記号はこの順序を表すものとして使います)。 を一般マグマの準同型、、 ならば が成り立つとします。
上の定義で使った記法 、、 について以下で説明します。
を書き換え規則とします。
- 、 を満たす が存在するとき とします。
- 、 を満たす が存在するとき とします。
- 任意の に対して ならば であるとき とします。
、、 とすると 、 ならば となります。、、 とすると 、 ならば となります。
を書き換え規則、 を書き換え規則からなる集合とするとき と定義します。
に対して
とし、 と定義します。
危険対に対応する書き換え規則の集合を と定義します。危険対の集合を と定義します。
は を含まないとします。
を満たす が存在するとき を を満たす最小の自然数とします。 とおきます。
の停止性
となる書き換え規則の列 と項の列 ()が存在するとき と書くことにします。 であり、かつ となる と項 が存在しないとき と書くことにします。
を満たす無限列 と が存在するとします。すると となり、このような無限列は存在しないので矛盾となります。よって となる が存在します。
よって任意の に対して を満たす が存在します(停止性)。
の合流性
、 (、)のとき、、 を満たす 、 が存在すること(合流性)を示します。
、、 とします。 となる が存在します。よって となる が存在します。 となります。
であるから 、 である が存在して または となります。
のとき より となって が成り立ち、 のとき より となって が成り立ちます。
よって任意の に対して が存在して となります。
、 とすると
- のとき 、
- のとき 、
- のとき 、
となる が存在します。
よって合流性が成り立ちます。
の完備性
停止性と合流性を満たすとき完備と呼びます。 は完備となります。任意の に対して を満たす は一意的に決まります。 を と書きます。
、 の部分集合 を とおきます。 を を含む最小の同値関係(反射・推移・対称閉包)とし、 を と書くことにすると
が成り立ちます。