エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を表すことを考えていくブロクです。

エレファントな群とリー代数(16)

一般マグマの多項式の完備化

環の演算では書き換え規則の合成を行っているので、今までの議論で説明できるのですが、その説明では長くなるのでいったん
群の完備化の説明をしたいと思います。

群の完備化ではクヌース・ベンディックス完備化アルゴリズム - Wikipediaと同様のことをやろうとしているのですが、自動的にできるようになっているわけではないので環の演算とほぼ同様のやり方になっています。

クヌース・ベンディックス完備化アルゴリズム - Wikipediaでは等式の有限集合  E から完備な書き換え規則の有限集合  R を作る半アルゴリズムについて書かれています。しかし詳細は書かれていないようなので少し付け加えて説明を書いてみたいと思います。

書き換え規則の合成の記法

以前の記事で使った書き換え規則の合成の記法をここでも使います(少しわかりにくい気がしますが変更するとややこしくなるのでこのまま使うことにします)。

書き換え規則  \rho = (x_1, \cdots, x_n \mapsto a \to b) に対して、 a(x_1, \cdots, x_n) の部分項の位置全体の集合を  Q_\rho b(x_1, \cdots, x_n) の部分項の位置全体の集合を  P_\rho とします。

書き換え規則の集合  R S に対して  R \cdot S = \{λ \stackrel{p}{\triangleright} μ, λ \stackrel{\hat{p}}{\triangleright} μ \mid λ \in R, μ \in S, p \in P_λ, \hat{p} \in Q_μ\} \setminus \{⊥\} と定義します。 R = \{r\} のとき  r \cdot S S = \{s\} のとき  R \cdot s R = \{r\} S = \{s\} のとき  r \cdot s のように書きます。任意の項  t t に写す「恒等」書き換え規則を  1 とし(後で  0 と書くこともあります)、書き換え規則の集合  R に対して \begin{cases}
R^0 & = & \{1\} \\
R^{n+1} & = & R^n \cdot R \\
\end{cases} と定義します。 \displaystyle R^* = \bigcup_{n \in \mathbb{N}} R^n と定義します。

書き換え規則  \rho = (x_1, \cdots, x_n \mapsto a \to b) に対して、 -\rho = (x_1, \cdots, x_n \mapsto b \to a) とします。書き換え規則の集合  R に対して  -R = \{ -\rho \mid \rho \in R \} とします。 1 \in (-\rho) \cdot \rho が成り立ちます。 \lambda = \rho_1 \cdot \rho_2 \cdot \cdots \cdot \rho_n に対して  -\lambda = (-\rho_n) \cdot (-\rho_{n-1}) \cdot \cdots \cdot (-\rho_1) とします。

完備化アルゴリズム

ここから「恒等」書き換え規則を  0 と書きます。書き換え規則を等式と考えることができます。書き換え規則  r を等式として見たものを  eq(r) とします。

 E_0 = E \ne \varnothing R_0 = \varnothing とし、等式の有限集合の列  E_0, E_1, E_2, \cdots、書き換え規則の有限集合の列  R_0, R_1, R_2, \cdots、等式の列  e_0, e_1, e_2, \cdots ( e_i \in E_i \cup \{\bot\}) を以下のように帰納的に作ります( e_i は任意の元で良い)。\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}  E_n = \varnothing のときは  e_n = \bot とします。

項全体の集合  T は整列集合(任意の空ではない部分集合が最小元をもつ全順序集合)であるとします( \le,\ge, =, <, > という記号はこの順序を表すものとして使います)。 \varphi: T \to T を一般マグマの準同型、 s, t \in T s \le t ならば  \varphi(s) \le \varphi(t) が成り立つとします。

上の定義で使った記法  \downarrow_R rr cp について以下で説明します。

 r を書き換え規則とします。

  •  s \xrightarrow{r} t s \le t を満たす  s, t \in T が存在するとき  r \le 0 とします。
  •  s \xrightarrow{r} t s \ge t を満たす  s, t \in T が存在するとき  r \ge 0 とします。
  • 任意の  s, t \in T に対して  s \xrightarrow{r} t ならば  s = t であるとき  r = 0 とします。

 s, t \in T s \xrightarrow{r} t s \le t とすると  s', t' \in T s' \xrightarrow{r} t' ならば  s' \le t' となります。 s, t \in T s \xrightarrow{r} t s \ge t とすると  s', t' \in T s' \xrightarrow{r} t' ならば  s' \ge t' となります。

 r を書き換え規則、 R を書き換え規則からなる集合とするとき  r \downarrow_R = \{r' \in (-R)^* \cdot r \cdot R^* \mid r' \cdot R = (-R) \cdot r' = \varnothing\} と定義します。

 r \in R に対して
 rr(eq(r)) = 
\begin{cases}
 r & (r > 0) \\
 -r & (r < 0) \\
 ⊥ & (r = 0) \\
\end{cases}
とし、 rr(eq(R)) = \{rr(eq(r)) \mid r \in R\} と定義します。

危険対に対応する書き換え規則の集合を  cr(R) = \bigcup \{ (-r) \cdot s \mid r, s \in R \} \setminus \{0\} と定義します。危険対の集合を  cp(R) = eq(cr(R)) と定義します。

 E eq(0) を含まないとします。

 R_{n+1} = \bot を満たす  n が存在するとき  n R_{n+1} = \bot を満たす最小の自然数とします。 R = R_n とおきます。

 R の停止性

 t_1 \xrightarrow{r_1} t_2 \xrightarrow{r_2} t_3 \xrightarrow{r_3} \cdots \xrightarrow{r_n} t_{n+1} となる書き換え規則の列  r_1, r_2, \cdots, r_n \in R と項の列  t_1, t_2, \cdots, t_{n+1} \in T ( n \ge 0)が存在するとき  t \xrightarrow{R*} t_{n+1} と書くことにします。 t \xrightarrow{R*} t' であり、かつ  t' \xrightarrow{r} t'' となる  r \in R と項  t'' が存在しないとき  t \xrightarrow{R*>} t' と書くことにします。

 t_1 \xrightarrow{r_1} t_2 \xrightarrow{r_2} t_3 \xrightarrow{r_3} \cdots を満たす無限列  r_1, r_2, \cdots \in R t_1, t_2, \cdots \in T が存在するとします。すると  t_1 > t_2 > t_3 > \cdots となり、このような無限列は存在しないので矛盾となります。よって  t_1 \xrightarrow{R*>} t_{n+1} となる  n \ge 0 が存在します。

よって任意の  t \in T に対して  t \xrightarrow{R*>} t' を満たす  t' \in T が存在します(停止性)。

 R の合流性

 t \xrightarrow{p} u t \xrightarrow{q} v ( t, u, v \in T p, q \in R)のとき、 t \xrightarrow{p} u \xrightarrow{\lambda} t' t \xrightarrow{q} v \xrightarrow{\mu} t' を満たす  t' \in T \lambda, \mu \in R^* が存在すること(合流性)を示します。

 p, q \in R = R_n r \in (-p) \cdot q r \ne 0 とします。 eq(r) \in E_{j} となる  j が存在します。よって  eq(r) = e_{k} となる  k が存在します。 rr(e_k \downarrow_{R_k}) \subseteq R_{k+1} \subseteq R となります。

 rr(e_k \downarrow_{R_k})  = \{r' \in (-R_k)^* \cdot \{r, -r\} \cdot R_k^* \mid r' \cdot R_k = (-R_k) \cdot r' = \varnothing, r' > 0\} であるから  \lambda, \mu \in R^* r' > 0 である  r' \in rr(e_k \downarrow_{R_k}) \subseteq R が存在して  r' \in (-\lambda) \cdot r \cdot \mu または  r' \in (-\lambda) \cdot (-r) \cdot \mu となります。

 r' \in (-\lambda) \cdot r \cdot \mu のとき  (-\lambda) \cdot (-p) \cdot q \cdot \mu = (-\lambda) \cdot r \cdot \mu \ne \varnothing より  q \cdot \mu \ne \varnothing となって  p \cdot \lambda \cdot ( (-\lambda) \cdot r \cdot \mu) \supseteq p \cdot r \cdot \mu \supseteq p \cdot (-p) \cdot q \cdot r \cdot \mu \supseteq q \cdot \mu \ne \varnothing が成り立ち、 r' \in (-\lambda) \cdot (-r) \cdot \mu のとき  (-\lambda) \cdot (-q) \cdot p \cdot \mu = (-\lambda) \cdot (-r) \cdot \mu \ne \varnothing より  p \cdot \mu \ne \varnothing となって  q \cdot \lambda \cdot ( (-\lambda) \cdot (-r) \cdot \mu) \supseteq q \cdot (-r) \cdot \mu \supseteq q \cdot (-q) \cdot p \cdot (-r) \cdot \mu \supseteq p \cdot \mu \ne \varnothing が成り立ちます。

よって任意の  p, q \in R に対して  \lambda, \mu \in R^* が存在して  (p \cdot \lambda) \cap (q \cdot \mu) \ne \varnothing となります。

 t \xrightarrow{p} u t \xrightarrow{q} v とすると

  •  u = v のとき  t \xrightarrow{p} u \xrightarrow{1} v t \xrightarrow{q} v \xrightarrow{1} v
  •  u > v のとき  t \xrightarrow{p} u \xrightarrow{r} v t \xrightarrow{q} v \xrightarrow{1} v
  •  u < v のとき  t \xrightarrow{p} u \xrightarrow{1} u t \xrightarrow{q} v \xrightarrow{-r} u

となる  r \in (-p) \cdot q が存在します。

よって合流性が成り立ちます。

 R の完備性

停止性と合流性を満たすとき完備と呼びます。 R は完備となります。任意の  t \in T に対して  t \xrightarrow{R*>} t' を満たす  t' \in T は一意的に決まります。 t' t \downarrow_R と書きます。

 R = R_n T \times T の部分集合  R_E R_E = \{ \langle s, t \rangle \in T \times T \mid s \xrightarrow{r} t \ となる \ eq(r) \in E \ が存在する \} とおきます。 \widetilde{E} R_E を含む最小の同値関係(反射・推移・対称閉包)とし、 \langle s, t \rangle \in \widetilde{E} s \sim t と書くことにすると
 s \sim t \iff s \downarrow_R = t \downarrow_R
が成り立ちます。

マグマの左単位元・右単位元

 M e_L e_R で生成された自由マグマ、 X を全順序集合、 T = M[X] とします。 T の演算を  \cdot と書きます。 T の元は  e_L e_R X の元、 \cdot、括弧を使って書くことができます。 T の元  s, t に対して  s の演算の個数が  t の演算の個数より大きいとき  s > t とします。また、 e_L > e_R とします。後は適当に定義して全順序とすることができます。

  •  E = \{ e_L \cdot x \sim x, x \cdot e_R \sim x \}
  •  R_1 = \{ e_L \cdot x \to x \}
  •  E_1 = \{ x \cdot e_R \sim x \}
  •  R_2 = \{ e_L \cdot x \to x, x \cdot e_R \to x \}
  •  E_2 = \{ e_L \sim e_R \}
  •  R_3 = \{ e_L \cdot x \to x, x \cdot e_R \to x, e_L \to e_R \}
  •  E_3 = \varnothing

となります。