エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

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

一般マグマの多項式の書き換え規則の合成

環の演算」(これはスマートフォンで使えるように以前のものを少し書き直しました)での式の合成の説明をする準備ができました。これを説明する前に、まず書き換え規則の合成について考えます。

ある代数的構造を等式の集合で書いたとき、その等式「任意の  x_1, \cdots, x_n に対して  a = b 」に対して書き換え規則  (x_1, \cdots, x_n \mapsto a \to b) (x_1, \cdots, x_n \mapsto b \to a) を考えます。

このようにして代数的構造の定義を書き換え規則の集合で書くことができます。二つの書き換え規則  \rho = (x_1, \cdots, x_n \mapsto a \to b) \mu = (y_1, \cdots, y_m \mapsto c \to d) を合成することを考えます。

 M を環の演算から作られる一般マグマとします。 T = M[x_1, \cdots, x_n, y_1, \cdots, y_m] とおきます。一般マグマの多項式の最汎単一化子を得る写像 u: T \times T \to \Sigma \sqcup \{\bot\} とします。

 b(x_1, \cdots, x_n) の部分項の位置  p の部分項を  b(x_1, \cdots, x_n)_p \rho = (x_1, \cdots, x_n \mapsto a \to b) に対して  b(x_1, \cdots, x_n) の部分項の位置全体の集合を  P_\rho α の部分項の位置  p の部分項を  β で置き換えたものを  α(p←β) とします。

 \sigma = u(b(x_1, \cdots, x_n)_p, c(y_1, \cdots, y_m)) のとき  ρ \stackrel{p}{\triangleright} μ を \begin{cases}
ρ \stackrel{p}{\triangleright} μ & = & (x_1, \cdots, x_n, y_1, \cdots, y_m \mapsto \\ & & \hspace{1em} a(x_1, \cdots, x_n)[σ] \to \\
& & \hspace{2em} b(x_1, \cdots, x_n)(p←d(y_1, \cdots, y_m)[σ])) & (σ \in Σ) \\
ρ \stackrel{p}{\triangleright} μ & = & ⊥ & (σ = ⊥) \\
\end{cases} と定義します。

 1 を何も変換しない規則とし、書き換え規則の集合  R に対して \begin{cases}
R^0 & = & \{1\} \\
R^{n+1} & = & \{λ \stackrel{p}{\triangleright} ρ \mid λ \in R^n, ρ \in R, p \in P_ρ\} \setminus \{⊥\} \\
\end{cases} と定義します。

以下では、書き換え規則  (x_1, \cdots, x_n \mapsto λ \to μ) を、 λ(x'_1, \cdots, x'_n) \to μ(x'_1, \cdots, x'_n) と書きます。ここで  x'_i は、 x_i に書き換え規則の集合内の番号  r と合成の回数  t によってインデックスをつけたもの( x_i y とすると  y_{r,t})とします。 λ \stackrel{p}{\triangleright} ρ μ とするとき  λ \stackrel{\rho,p}{\Longrightarrow} μ と書きます。部分項の位置  p は、項を文字列で書いたときの左から順番につけた番号で表すとします。

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

以前考察したマグマの左単位元・右単位元について考えていきます。書き換え規則の集合は以下のようになります。\begin{cases}
\rho_{1} & = & ( & x & \mapsto & e_L x & \to & x & ) \\
\rho_{2} & = & ( & x & \mapsto & x & \to & e_L x & ) \\
\rho_{3} & = & ( & x & \mapsto & x e_R & \to & x & ) \\
\rho_{4} & = & ( & x & \mapsto & x & \to & x e_R & ) \\
\end{cases}  1 から始めた2段階の合成をすべて書くと以下のようになります。\begin{matrix}
1 & \stackrel{\rho_{1},0}{\Longrightarrow} & e_L x_{1,1} \to x_{1,1} & \stackrel{\rho_{1},0}{\Longrightarrow} & e_L ( e_L x_{1,2} ) \to x_{1,2} \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{1},0}{\Longrightarrow} & x_{1,2} \to x_{1,2} \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{1},2}{\Longrightarrow} & e_L x_{1,2} \to e_L x_{1,2} \\
1 & \stackrel{\rho_{3},0}{\Longrightarrow} & x_{3,1} e_R \to x_{3,1} & \stackrel{\rho_{1},0}{\Longrightarrow} & ( e_L x_{1,2} ) e_R \to x_{1,2} \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{1},0}{\Longrightarrow} & e_L \to e_R \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{1},1}{\Longrightarrow} & e_L x_{1,2} \to x_{1,2} e_R \\
1 & \stackrel{\rho_{1},0}{\Longrightarrow} & e_L x_{1,1} \to x_{1,1} & \stackrel{\rho_{2},0}{\Longrightarrow} & e_L x_{2,2} \to e_L x_{2,2} \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L ( e_L x_{2,1} ) \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{2},1}{\Longrightarrow} & x_{2,1} \to ( e_L e_L ) x_{2,1} \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{2},2}{\Longrightarrow} & x_{2,2} \to e_L ( e_L x_{2,2} ) \\
1 & \stackrel{\rho_{3},0}{\Longrightarrow} & x_{3,1} e_R \to x_{3,1} & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,2} e_R \to e_L x_{2,2} \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{4,1} \to e_L ( x_{4,1} e_R ) \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{2},1}{\Longrightarrow} & x_{2,2} \to ( e_L x_{2,2} ) e_R \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{2},2}{\Longrightarrow} & x_{4,1} \to x_{4,1} ( e_L e_R ) \\
1 & \stackrel{\rho_{1},0}{\Longrightarrow} & e_L x_{1,1} \to x_{1,1} & \stackrel{\rho_{3},0}{\Longrightarrow} & e_L ( x_{3,2} e_R ) \to x_{3,2} \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{3},0}{\Longrightarrow} & e_R \to e_L \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{3},2}{\Longrightarrow} & x_{3,2} e_R \to e_L x_{3,2} \\
1 & \stackrel{\rho_{3},0}{\Longrightarrow} & x_{3,1} e_R \to x_{3,1} & \stackrel{\rho_{3},0}{\Longrightarrow} & ( x_{3,2} e_R ) e_R \to x_{3,2} \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{3},0}{\Longrightarrow} & x_{3,2} \to x_{3,2} \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{3},1}{\Longrightarrow} & x_{3,2} e_R \to x_{3,2} e_R \\
1 & \stackrel{\rho_{1},0}{\Longrightarrow} & e_L x_{1,1} \to x_{1,1} & \stackrel{\rho_{4},0}{\Longrightarrow} & e_L x_{4,2} \to x_{4,2} e_R \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{2,1} \to ( e_L x_{2,1} ) e_R \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{4},1}{\Longrightarrow} & x_{2,1} \to ( e_L e_R ) x_{2,1} \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{4},2}{\Longrightarrow} & x_{4,2} \to e_L ( x_{4,2} e_R ) \\
1 & \stackrel{\rho_{3},0}{\Longrightarrow} & x_{3,1} e_R \to x_{3,1} & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,2} e_R \to x_{4,2} e_R \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to ( x_{4,1} e_R ) e_R \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{4},1}{\Longrightarrow} & x_{4,2} \to ( x_{4,2} e_R ) e_R \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{4},2}{\Longrightarrow} & x_{4,1} \to x_{4,1} ( e_R e_R ) \\
\end{matrix} これによって書き換え規則を合成した書き換え規則として \begin{matrix}
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to x_{4,1} e_R & \stackrel{\rho_{1},0}{\Longrightarrow} & e_L \to e_R \\
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,1} \to e_L x_{2,1} & \stackrel{\rho_{3},0}{\Longrightarrow} & e_R \to e_L \\
\end{matrix} が得られることがわかります。

モノイドの左逆元・右逆元

次にモノイドの左逆元・右逆元について考えていきます。書き換え規則の集合は以下のようになります。\begin{cases}
\rho_{1} & = & ( & x, y, z & \mapsto & (x y) z & \to & x (y z) & ) \\
\rho_{2} & = & ( & x, y, z & \mapsto & x (y z) & \to & (x y) z & ) \\
\rho_{3} & = & ( & x & \mapsto & e x & \to & x & ) \\
\rho_{4} & = & ( & x & \mapsto & x & \to & e x & ) \\
\rho_{5} & = & ( & x & \mapsto & x e & \to & x & ) \\
\rho_{6} & = & ( & x & \mapsto & x & \to & x e & ) \\
\rho_{7} & = & ( & & \mapsto & x_L x & \to & e & ) \\
\rho_{8} & = & ( & & \mapsto & e & \to & x_L x & ) \\
\rho_{9} & = & ( & & \mapsto & x x_R & \to & e & ) \\
\rho_{10} & = & ( & & \mapsto & e & \to & x x_R & ) \\
\end{cases} 以下の書き換え規則を得ることができます。\begin{matrix}
1 & \stackrel{\rho_{6},0}{\Longrightarrow} & x_{6,1} \to x_{6,1} e & \stackrel{\rho_{10},2}{\Longrightarrow} & x_{6,1} \to x_{6,1} ( x x_R ) \\
& \stackrel{\rho_{2},0}{\Longrightarrow} & x_{2,3} \to ( x_{2,3} x ) x_R & \stackrel{\rho_{7},1}{\Longrightarrow} & x_L \to e x_R \\
& \stackrel{\rho_{3},0}{\Longrightarrow} & x_L \to x_R \\
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x_{4,1} \to e x_{4,1} & \stackrel{\rho_{8},1}{\Longrightarrow} & x_{4,1} \to ( x_L x ) x_{4,1} \\
& \stackrel{\rho_{1},0}{\Longrightarrow} & z_{1,3} \to x_L ( x z_{1,3} ) & \stackrel{\rho_{9},2}{\Longrightarrow} & x_R \to x_L e \\
& \stackrel{\rho_{5},0}{\Longrightarrow} & x_R \to x_L \\
\end{matrix}