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

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

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

一般マグマの多項式の等式の合成(2)

続いて単位元をもつマグマの準同型についても見ていきます。

単位元をもつマグマの準同型(1)

第1段階

等式の集合 \begin{cases}
\mathrm{eq}_{1}: & x & \mapsto & e x & = & x \\
\mathrm{eq}_{2}: & x & \mapsto & x e' & = & x \\
\mathrm{eq}_{3}: & x, y & \mapsto & f( x y ) & = & f( x ) f( y ) \\
\mathrm{eq}_{4}: & & \mapsto & f( x ) & = & e' \\
\end{cases} から \begin{cases}
\mathrm{eq}_{1}: & x & \mapsto & e x & = & x \\
\mathrm{eq}_{3}: & x, y & \mapsto & f( x y ) & = & f( x ) f( y ) \\
\end{cases} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & x, y & \mapsto & f( e ( x y ) ) & = & f( x ) f( y ) \\
\mathrm{ceq}_{2}: & x, y & \mapsto & f( ( e x ) y ) & = & f( x ) f( y ) \\
\mathrm{ceq}_{3}: & x, y & \mapsto & f( x ( e y ) ) & = & f( x ) f( y ) \\
\mathrm{ceq}_{4}: & x, y & \mapsto & f( e x ) f( y ) & = & f( x y ) \\
\mathrm{ceq}_{5}: & x, y & \mapsto & f( x ) f( e y ) & = & f( x y ) \\
\mathrm{ceq}_{6}: & x & \mapsto & f( x ) & = & f( e ) f( x ) \\
\mathrm{ceq}_{7}: & x, y & \mapsto & f( x y ) & = & f( e x ) f( y ) \\
\mathrm{ceq}_{8}: & x, y & \mapsto & f( x y ) & = & f( x ) f( e y ) \\
\mathrm{ceq}_{9}: & x, y & \mapsto & f( x ) f( y ) & = & f( ( e x ) y ) \\
\mathrm{ceq}_{10}: & x, y & \mapsto & f( x ) f( y ) & = & f( x ( e y ) ) \\
\end{cases} が得られます。

第2段階

等式の集合に  \mathrm{ceq}_{6} を追加し \begin{cases}
\mathrm{eq}_{4}: & & \mapsto & f( x ) & = & e' \\
\mathrm{eq}_{5}: & x & \mapsto & f( x ) & = & f( e ) f( x ) \\
\end{cases} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & & \mapsto & e' & = & f( e ) f( x ) \\
\mathrm{ceq}_{2}: & & \mapsto & f( e ) e' & = & f( x ) \\
\end{cases} が得られます。

第3段階

等式の集合に  \mathrm{ceq}_{2} を追加し \begin{cases}
\mathrm{eq}_{4}: & & \mapsto & f( x ) & = & e' \\
\mathrm{eq}_{6}: & & \mapsto & f( e ) e' & = & f( x ) \\
\end{cases} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & & \mapsto & f( e ) f( x ) & = & f( x ) \\
\mathrm{ceq}_{2}: & & \mapsto & e' & = & f( e ) e' \\
\end{cases} が得られます。

第4段階

等式の集合に  \mathrm{ceq}_{2} を追加し \begin{cases}
\mathrm{eq}_{2}: & x & \mapsto & x e' & = & x \\
\mathrm{eq}_{7}: & & \mapsto & e' & = & f( e ) e' \\
\end{cases} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & & \mapsto & e' e' & = & f( e ) e' \\
\mathrm{ceq}_{2}: & & \mapsto & ( f( e ) e' ) e' & = & e' \\
\mathrm{ceq}_{3}: & & \mapsto & ( f( e ) e' ) e' & = & e' \\
\mathrm{ceq}_{4}: & & \mapsto & f( e ) ( e' e' ) & = & e' \\
\mathrm{ceq}_{5}: & & \mapsto & e' & = & ( f( e ) e' ) e' \\
\mathrm{ceq}_{6}: & x & \mapsto & x & = & x ( f( e ) e' ) \\
\mathrm{ceq}_{7}: & & \mapsto & f( e ) & = & e' \\
\mathrm{ceq}_{8}: & & \mapsto & f( e ) e' & = & e' e' \\
\end{cases} が得られます。よって \begin{matrix}
\mathrm{ceq}_{7}: & & \mapsto & f( e ) & = & e' \\
\end{matrix} が成り立ちます。

単位元をもつマグマの準同型(2)

第1段階

等式の集合 \begin{cases}
\mathrm{eq}_{1}: & & \mapsto & x^{-1} x & = & e \\
\mathrm{eq}_{2}: & x, y & \mapsto & f( x y ) & = & f( x ) f( y ) \\
\mathrm{eq}_{3}: & & \mapsto & f( e ) & = & e' \\
\end{cases} から \begin{cases}
\mathrm{eq}_{1}: & & \mapsto & x^{-1} x & = & e \\
\mathrm{eq}_{2}: & x, y & \mapsto & f( x y ) & = & f( x ) f( y ) \\
\end{cases} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & y & \mapsto & f( ( x^{-1} x ) y ) & = & f( e ) f( y ) \\
\mathrm{ceq}_{2}: & y & \mapsto & f( y ( x^{-1} x ) ) & = & f( y ) f( e ) \\
\mathrm{ceq}_{3}: & y & \mapsto & f( x^{-1} x ) f( y ) & = & f( e y ) \\
\mathrm{ceq}_{4}: & y & \mapsto & f( y ) f( x^{-1} x ) & = & f( y e ) \\
\mathrm{ceq}_{5}: & & \mapsto & f( e ) & = & f( x^{-1} ) f( x ) \\
\mathrm{ceq}_{6}: & y & \mapsto & f( e y ) & = & f( x^{-1} x ) f( y ) \\
\mathrm{ceq}_{7}: & y & \mapsto & f( y e ) & = & f( y ) f( x^{-1} x ) \\
\mathrm{ceq}_{8}: & y & \mapsto & f( e ) f( y ) & = & f( ( x^{-1} x ) y ) \\
\mathrm{ceq}_{9}: & y & \mapsto & f( y ) f( e ) & = & f( y ( x^{-1} x ) ) \\
\end{cases} が得られます。

第2段階

等式の集合に  \mathrm{ceq}_{5} を追加し \begin{cases}
\mathrm{eq}_{3}: & & \mapsto & f( e ) & = & e' \\
\mathrm{eq}_{4}: & & \mapsto & f( e ) & = & f( x^{-1} ) f( x ) \\
\end{cases} を選択して合成すると \begin{matrix}
\mathrm{ceq}_{1}: & & \mapsto & e' & = & f( x^{-1} ) f( x ) \\
\end{matrix} が得られます。

単位元をもつマグマの準同型(3)

第1段階

等式の集合 \begin{cases}
\mathrm{eq}_{1}: & & \mapsto & x^{-1} x & = & e \\
\mathrm{eq}_{2}: & x, y & \mapsto & f( x y ) & = & f( x ) f( y ) \\
\mathrm{eq}_{3}: & & \mapsto & f( x^{-1} ) f( x ) & = & e' \\
\end{cases} から \begin{cases}
\mathrm{eq}_{1}: & & \mapsto & x^{-1} x & = & e \\
\mathrm{eq}_{2}: & x, y & \mapsto & f( x y ) & = & f( x ) f( y ) \\
\end{cases} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & y & \mapsto & f( ( x^{-1} x ) y ) & = & f( e ) f( y ) \\
\mathrm{ceq}_{2}: & y & \mapsto & f( y ( x^{-1} x ) ) & = & f( y ) f( e ) \\
\mathrm{ceq}_{3}: & y & \mapsto & f( x^{-1} x ) f( y ) & = & f( e y ) \\
\mathrm{ceq}_{4}: & y & \mapsto & f( y ) f( x^{-1} x ) & = & f( y e ) \\
\mathrm{ceq}_{5}: & & \mapsto & f( e ) & = & f( x^{-1} ) f( x ) \\
\mathrm{ceq}_{6}: & y & \mapsto & f( e y ) & = & f( x^{-1} x ) f( y ) \\
\mathrm{ceq}_{7}: & y & \mapsto & f( y e ) & = & f( y ) f( x^{-1} x ) \\
\mathrm{ceq}_{8}: & y & \mapsto & f( e ) f( y ) & = & f( ( x^{-1} x ) y ) \\
\mathrm{ceq}_{9}: & y & \mapsto & f( y ) f( e ) & = & f( y ( x^{-1} x ) ) \\
\end{cases} が得られます。

第2段階

等式の集合に  \mathrm{ceq}_{5} を追加し \begin{cases}
\mathrm{eq}_{3}: & & \mapsto & f( x^{-1} ) f( x ) & = & e' \\
\mathrm{eq}_{4}: & & \mapsto & f( e ) & = & f( x^{-1} ) f( x ) \\
\end{cases} を選択して合成すると \begin{matrix}
\mathrm{ceq}_{1}: & & \mapsto & e' & = & f( e ) \\
\end{matrix} が得られます。


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

一般マグマの多項式の等式の合成(1)

書き換え規則  \rho = (x_1, \cdots, x_n \mapsto a \to b) に対して、 -\rho = (x_1, \cdots, x_n \mapsto b \to a) とします。 e_\rho = \{\rho, -\rho\} を等式と考えます。これを  x_1, \cdots, x_n \mapsto a = b と書くことにします。書き換え規則の合成を等式の合成に書き直すことができます。

書き換え規則  \rho \mu に対して書き換え規則の集合の合成  e_\rho \cdot e_\mu を考えると、 e_\rho \cdot e_\mu = e_\mu \cdot e_\rho となります。よって  e_\rho \cdot e_\mu を等式  e_\rho e_\mu の合成からなる集合と考えることができます。

等式の集合  E E' に対して  \displaystyle E \cdot E' = \bigcup \{e \cdot e' \mid e \in E, e' \in E'\} とします。等式の集合  E に対して \begin{cases}
E_1 & = & E \\
E_{n+1} & = & E_n \cup (E_n \cdot E_n) \\
\end{cases} と定義します。

環の演算の操作はこれと同様のものになっています。まず  e_1, e_2 \in E_n をユーザーが選択し、次に  e' \in e_1 \cdot e_2 をユーザーが選択して  E_{n+1} = E_n \cup \{e'\} とするようになっています。群の完備化も同様の操作になっています。

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

等式の集合 \begin{cases}
\mathrm{eq}_{1}: & x & \mapsto & e_L x & = & x \\
\mathrm{eq}_{2}: & x & \mapsto & x e_R & = & x \\
\end{cases} から  \mathrm{eq}_{1}, \mathrm{eq}_{2} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & x & \mapsto & e_L ( x e_R ) & = & x \\
\mathrm{ceq}_{2}: & x & \mapsto & ( e_L x ) e_R & = & x \\
\mathrm{ceq}_{3}: & x & \mapsto & x ( e_L e_R ) & = & x \\
\mathrm{ceq}_{4}: & x & \mapsto & e_L x & = & x e_R \\
\mathrm{ceq}_{5}: & & \mapsto & e_R & = & e_L \\
\mathrm{ceq}_{6}: & x & \mapsto & x e_R & = & e_L x \\
\mathrm{ceq}_{7}: & x & \mapsto & x e_R & = & e_L x \\
\mathrm{ceq}_{8}: & x & \mapsto & x & = & ( e_L x ) e_R \\
\mathrm{ceq}_{9}: & x & \mapsto & x & = & ( e_L e_R ) x \\
\mathrm{ceq}_{10}: & x & \mapsto & x & = & e_L ( x e_R ) \\
\end{cases} が得られます。よって \begin{matrix}
\mathrm{ceq}_{5}: & & \mapsto & e_R & = & e_L \\
\end{matrix} が成り立つことがわかります。この場合は1回で終了するので書き換え規則の合成と同じです。

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

等式の集合 \begin{cases}
\mathrm{eq}_{1}: & x, y, z & \mapsto & ( x y ) z & = & x ( y z ) \\
\mathrm{eq}_{2}: & x & \mapsto & e x & = & x \\
\mathrm{eq}_{3}: & x & \mapsto & x e & = & x \\
\mathrm{eq}_{4}: & & \mapsto & x_L x & = & e \\
\mathrm{eq}_{5}: & & \mapsto & x x_R & = & e \\
\end{cases} から \begin{cases}
\mathrm{eq}_{1}: & x, y, z & \mapsto & ( x y ) z & = & x ( y z ) \\
\mathrm{eq}_{4}: & & \mapsto & x_L x & = & e \\
\end{cases} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & y, z & \mapsto & ( ( x_L x ) y ) z & = & e ( y z ) \\
\mathrm{ceq}_{2}: & y & \mapsto & ( y x_L ) x & = & y e \\
\mathrm{ceq}_{3}: & y, z & \mapsto & ( y ( x_L x ) ) z & = & y ( e z ) \\
\mathrm{ceq}_{4}: & y, z & \mapsto & ( y z ) ( x_L x ) & = & y ( z e ) \\
\mathrm{ceq}_{5}: & y, z & \mapsto & ( e y ) z & = & ( x_L x ) ( y z ) \\
\mathrm{ceq}_{6}: & y, z & \mapsto & ( y e ) z & = & y ( ( x_L x ) z ) \\
\mathrm{ceq}_{7}: & y, z & \mapsto & ( y z ) e & = & y ( z ( x_L x ) ) \\
\mathrm{ceq}_{8}: & y & \mapsto & x_L ( x y ) & = & e y \\
\mathrm{ceq}_{9}: & y, z & \mapsto & ( x_L x ) ( y z ) & = & ( e y ) z \\
\mathrm{ceq}_{10}: & y, z & \mapsto & y ( ( x_L x ) z ) & = & ( y e ) z \\
\mathrm{ceq}_{11}: & y, z & \mapsto & y ( z ( x_L x ) ) & = & ( y z ) e \\
\mathrm{ceq}_{12}: & y, z & \mapsto & e ( y z ) & = & ( ( x_L x ) y ) z \\
\mathrm{ceq}_{13}: & y, z & \mapsto & y ( e z ) & = & ( y ( x_L x ) ) z \\
\mathrm{ceq}_{14}: & y, z & \mapsto & y ( z e ) & = & ( y z ) ( x_L x ) \\
\end{cases} が得られます。ここから \begin{matrix}
\mathrm{ceq}_{8}: & y & \mapsto & x_L ( x y ) & = & e y \\
\end{matrix} を選択して等式の集合に追加し \begin{matrix}
\mathrm{eq}_{6}: & y & \mapsto & x_L ( x y ) & = & e y \\
\end{matrix} とします。次に等式の集合から \begin{cases}
\mathrm{eq}_{5}: & & \mapsto & x x_R & = & e \\
\mathrm{eq}_{6}: & y & \mapsto & x_L ( x y ) & = & e y \\
\end{cases} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & & \mapsto & x_L ( x ( x x_R ) ) & = & e e \\
\mathrm{ceq}_{2}: & y & \mapsto & ( x x_R ) y & = & x_L ( x y ) \\
\mathrm{ceq}_{3}: & & \mapsto & e ( x x_R ) & = & x_L ( x e ) \\
\mathrm{ceq}_{4}: & & \mapsto & x_L e & = & e x_R \\
\mathrm{ceq}_{5}: & & \mapsto & x_L ( x e ) & = & e ( x x_R ) \\
\mathrm{ceq}_{6}: & & \mapsto & e e & = & x_L ( x ( x x_R ) ) \\
\end{cases} が得られるので \begin{matrix}
\mathrm{ceq}_{4}: & & \mapsto & x_L e & = & e x_R \\
\end{matrix} を等式の集合に追加し \begin{matrix}
\mathrm{eq}_{7}: & & \mapsto & x_L e & = & e x_R \\
\end{matrix} とします。次に等式の集合から \begin{cases}
\mathrm{eq}_{2}: & x & \mapsto & e x & = & x \\
\mathrm{eq}_{7}: & & \mapsto & x_L e & = & e x_R \\
\end{cases} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & & \mapsto & e ( x_L e ) & = & e x_R \\
\mathrm{ceq}_{2}: & & \mapsto & ( e x_L ) e & = & e x_R \\
\mathrm{ceq}_{3}: & & \mapsto & x_L ( e e ) & = & e x_R \\
\mathrm{ceq}_{4}: & & \mapsto & e ( e x_R ) & = & x_L e \\
\mathrm{ceq}_{5}: & & \mapsto & ( e e ) x_R & = & x_L e \\
\mathrm{ceq}_{6}: & & \mapsto & e ( e x_R ) & = & x_L e \\
\mathrm{ceq}_{7}: & & \mapsto & x_L e & = & e ( e x_R ) \\
\mathrm{ceq}_{8}: & & \mapsto & x_R & = & x_L e \\
\mathrm{ceq}_{9}: & & \mapsto & e x_R & = & e ( x_L e ) \\
\end{cases} が得られるので \begin{matrix}
\mathrm{ceq}_{8}: & & \mapsto & x_R & = & x_L e \\
\end{matrix} を等式の集合に追加し \begin{matrix}
\mathrm{eq}_{8}: & & \mapsto & x_R & = & x_L e \\
\end{matrix} とします。次に等式の集合から \begin{cases}
\mathrm{eq}_{3}: & x & \mapsto & x e & = & x \\
\mathrm{eq}_{8}: & & \mapsto & x_R & = & x_L e \\
\end{cases} を選択して合成すると \begin{cases}
\mathrm{ceq}_{1}: & & \mapsto & x_R e & = & x_L e \\
\mathrm{ceq}_{2}: & & \mapsto & ( x_L e ) e & = & x_R \\
\mathrm{ceq}_{3}: & & \mapsto & ( x_L e ) e & = & x_R \\
\mathrm{ceq}_{4}: & & \mapsto & x_L ( e e ) & = & x_R \\
\mathrm{ceq}_{5}: & & \mapsto & x_R & = & ( x_L e ) e \\
\mathrm{ceq}_{6}: & & \mapsto & x_L & = & x_R \\
\mathrm{ceq}_{7}: & & \mapsto & x_L e & = & x_R e \\
\end{cases} が得られます。よって \begin{matrix}
\mathrm{ceq}_{6}: & & \mapsto & x_L & = & x_R \\
\end{matrix} が成り立つことがわかります。

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

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

前回の説明で間違っているところがあったので訂正します。

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

二つの書き換え規則  \rho = (x_1, \cdots, x_n \mapsto a \to b) \mu = (y_1, \cdots, y_m \mapsto c \to d) を合成することを考えます。 \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} と定義します。 \sigma = u(b(x_1, \cdots, x_n), c(y_1, \cdots, y_m)_p) のとき  ρ \stackrel{p}{\triangleright} μ を \begin{cases}
ρ \stackrel{p}{\triangleright} μ & = & (x_1, \cdots, x_n, y_1, \cdots, y_m \mapsto \\ & & \hspace{1em} c(x_1, \cdots, x_n)(p←a(y_1, \cdots, y_m))[σ] \to \\
& & \hspace{2em} d(x_1, \cdots, x_n)[σ]) & (σ \in Σ) \\
ρ \stackrel{p}{\triangleright} μ & = & ⊥ & (σ = ⊥) \\
\end{cases} と定義します。

書き換え規則の集合  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 \{⊥\} と定義します。 1 を何も変換しない規則とし、書き換え規則の集合  R に対して \begin{cases}
R^0 & = & \{1\} \\
R^{n+1} & = & R^n \cdot R \\
\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})とします。 p \in P_λ のとき、 λ \stackrel{p}{\triangleright} ρ μ とするとき  λ \stackrel{\rho,p}{\Longrightarrow} μ と書きます。 p \in Q_μ のとき、 λ \stackrel{p}{\triangleright} ρ μ とするとき  λ \stackrel{\rho,\hat{p}}{\Longrightarrow} μ と書きます。部分項の位置  p は、項を文字列で書いたときの左から順番につけた番号で表すとします。

単位元をもつマグマの準同型(1)

 M単位元  e をもつマグマ、 M'単位元  e' をもつマグマ、 f: M \to M' をマグマの準同型とします。このとき  e' \in f(M) ならば  f(e) = e' が成り立つことを示します。

以下の表記では、 x のように「 '」がつかないものは  M に属するもの、 x' のように「 '」がついたものは  M' に属するものとします。

書き換え規則の集合 \begin{cases}
\rho_{1} & = & ( & x & \mapsto & e x & \to & x & ) \\
\rho_{2} & = & ( & x & \mapsto & x & \to & e x & ) \\
\rho_{3} & = & ( & x' & \mapsto & x' e' & \to & x' & ) \\
\rho_{4} & = & ( & x' & \mapsto & x' & \to & x' e' & ) \\
\rho_{5} & = & ( & x, y & \mapsto & f(x y) & \to & f(x) f(y) & ) \\
\rho_{6} & = & ( & x, y & \mapsto & f(x) f(y) & \to & f(x y) & ) \\
\rho_{7} & = & ( & & \mapsto & f(x) & \to & e' & ) \\
\rho_{8} & = & ( & & \mapsto & e' & \to & f(x) & ) \\
\end{cases} から規則の合成によって \begin{matrix}
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & x'_{4,1} \to x'_{4,1} e' & \stackrel{\rho_{8},2}{\Longrightarrow} & x'_{4,1} \to x'_{4,1} f( x ) \\
& \stackrel{\rho_{6},0}{\Longrightarrow} & f( x_{6,3} ) \to f( x_{6,3} x ) & \stackrel{\rho_{1},1}{\Longrightarrow} & f( e ) \to f( x ) \\
& \stackrel{\rho_{7},0}{\Longrightarrow} & f( e ) \to e' \\
1 & \stackrel{\rho_{8},0}{\Longrightarrow} & e' \to f( x ) & \stackrel{\rho_{2},1}{\Longrightarrow} & e' \to f( e x ) \\
& \stackrel{\rho_{5},0}{\Longrightarrow} & e' \to f( e ) f( x ) & \stackrel{\rho_{7},3}{\Longrightarrow} & e' \to f( e ) e' \\
& \stackrel{\rho_{3},0}{\Longrightarrow} & e' \to f( e ) \\
\end{matrix} を得ることができます。

単位元をもつマグマの準同型(2)

 M単位元  e をもつマグマ、 M'単位元  e' をもつマグマ、 f: M \to M' をマグマの準同型、 f(e) = e' とします。このとき  x^{-1} x の逆元ならば  f(x^{-1}) f(x) の逆元となることを示します。

書き換え規則の集合 \begin{cases}
\rho_{1} & = & ( & & \mapsto & x^{-1} x & \to & e & ) \\
\rho_{2} & = & ( & & \mapsto & e & \to & x^{-1} x & ) \\
\rho_{3} & = & ( & x, y & \mapsto & f(x y) & \to & f(x) f(y) & ) \\
\rho_{4} & = & ( & x, y & \mapsto & f(x) f(y) & \to & f(x y) & ) \\
\rho_{5} & = & ( & & \mapsto & f(e) & \to & e' & ) \\
\rho_{6} & = & ( & & \mapsto & e' & \to & f(e) & ) \\
\end{cases} から規則の合成によって \begin{matrix}
1 & \stackrel{\rho_{4},0}{\Longrightarrow} & f( x_{4,1} ) f( y_{4,1} ) \to f( x_{4,1} y_{4,1} ) & \stackrel{\rho_{1},1}{\Longrightarrow} & f( x^{-1} ) f( x ) \to f( e ) \\
& \stackrel{\rho_{5},0}{\Longrightarrow} & f( x^{-1} ) f( x ) \to e' \\
1 & \stackrel{\rho_{6},0}{\Longrightarrow} & e' \to f( e ) & \stackrel{\rho_{2},1}{\Longrightarrow} & e' \to f( x^{-1} x ) \\
& \stackrel{\rho_{3},0}{\Longrightarrow} & e' \to f( x^{-1} ) f( x ) \\
\end{matrix} を得ることができます。

単位元をもつマグマの準同型(3)

 M単位元  e をもつマグマ、 M'単位元  e' をもつマグマ、 f: M \to M' をマグマの準同型とします。このとき  x^{-1} x の逆元、 f(x^{-1}) f(x) の逆元ならば  f(e) = e' となることを示します。

書き換え規則の集合 \begin{cases}
\rho_{1} & = & ( & & \mapsto & x^{-1} x & \to & e & ) \\
\rho_{2} & = & ( & & \mapsto & e & \to & x^{-1} x & ) \\
\rho_{3} & = & ( & x, y & \mapsto & f(x y) & \to & f(x) f(y) & ) \\
\rho_{4} & = & ( & x, y & \mapsto & f(x) f(y) & \to & f(x y) & ) \\
\rho_{5} & = & ( & & \mapsto & f(x^{-1}) f(x) & \to & e' & ) \\
\rho_{6} & = & ( & & \mapsto & e' & \to & f(x^{-1}) f(x) & ) \\
\end{cases} から規則の合成によって \begin{matrix}
1 & \stackrel{\rho_{2},0}{\Longrightarrow} & e \to x^{-1} x & \stackrel{\rho_{3},\hat{1}}{\Longrightarrow} & f( e ) \to f( x^{-1} ) f( x ) & \stackrel{\rho_{5},0}{\Longrightarrow} & f( e ) \to e' \\
1 & \stackrel{\rho_{6},0}{\Longrightarrow} & e' \to f( x^{-1} ) f( x ) & \stackrel{\rho_{4},0}{\Longrightarrow} & e' \to f( x^{-1} x ) & \stackrel{\rho_{1},1}{\Longrightarrow} & e' \to f( e ) \\
\end{matrix} を得ることができます。

エレファントな群とリー代数(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}

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

一般マグマの多項式の単一化アルゴリズム(3)

前回の議論(「wikipedia:ユニフィケーション」の「一階の項」を参照)を『計算論理に基づく推論ソフトウェア論』の議論のように2段階に分けます。なお、前回の記事でも単一化アルゴリズムの中で項を変化させる場合と変化させない場合が混在していたので、この点も直します。

 X = \{x_1, x_2, \cdots, x_n\} とします。一般マグマの多項式  \varphi \in M[X] a_1, a_2, \cdots, a_n ( a_1, a_2, \cdots, a_n \in M[X])を代入したものを  \varphi(a_1, a_2, \cdots, a_n) とします。

 \sigma: X \to M[X] \langle x_1, x_2, \cdots, x_n \rangle \mapsto \langle a_1, a_2, \cdots, a_n \rangle という置換とすると  \varphi(a_1, a_2, \cdots, a_n) = \sigma^*(\varphi) となります( \sigma^* \sigma を拡張した一般マグマの準同型)。これを  \varphi[\sigma] と書くことにします。 \vec{a} = \langle a_1, a_2, \cdots, a_n \rangle としたとき  \varphi[\vec{a}] と書くことにします。

 \langle x_1, x_2, \cdots, x_n \rangle \mapsto \langle x_1, x_2, \cdots, x_n \rangle という置換を  1 とします。

 x \in X a \in M[X] に対して  [x \mapsto a] x \mapsto a y \mapsto y \ (y \in X \setminus \{x\}) という置換とします。 \sigma = [x \mapsto a] のとき  \varphi[\sigma] \varphi[x \mapsto a] と書くことにします。

置換全体の集合を  \Sigma とおきます。 \sigma, \tau \in \Sigma に対して  \tau^* \circ \sigma \sigma \succ \tau と書くことにします。 \sigma, \tau \in \Sigma に対して  \psi \circ \sigma = \tau となる一般マグマの準同型  \psi が存在するとき  \sigma \le \tau と書くことにします。 \le は前順序となります。

 \alpha, \beta \in M[X] に対して、置換  \sigma: X \to M[X] が存在して  \alpha[\sigma] = \beta[\sigma] となるとき、 \alpha \beta は単一化可能といって、 \sigma \alpha \beta の単一化子と呼びます。

  • (MGU1)  \sigma \alpha \beta の単一化子で、
  • (MGU2)  \tau \alpha \beta の単一化子ならば  \sigma \le \tau

となるとき  \sigma \alpha \beta の最汎単一化子と呼びます。

 T = M[X] とおきます。 T f_i(t_1, t_2, \cdots, t_n) という形の元の全体を  T_{f_i}、 T_{f_0} = M とします。すると、 T = X \cup T_{f_0} \cup T_{f_1} \cup T_{f_2} \cup \cdots \cup T_{f_m} となります。 T_+ = T_{f_0} \cup T_{f_1} \cup T_{f_2} \cup \cdots \cup T_{f_m} とします。

 v(\alpha) \alpha の部分項として現れる  X の元全体の集合とします。

 d(\alpha, \beta) d: T \times T \to \Sigma \sqcup \{\bot\} ( \bot は失敗を表す)を \begin{cases}
(D1) & α \in M, & β \in M, & α = β & のとき & ⊥ \\
(D2) & α \in M, & β \in M, & α \ne β & のとき & ⊥ \\
(D3) & α \in X, & β \in X, & α = β & のとき & ⊥ \\
(D4) & α \in X, & β \in X, & α \ne β & のとき & [α \mapsto β] \\
(D5) & α \in X, & β \in T_+, & α \notin v(β) & のとき & [α \mapsto β] \\
(D6) & α \in X, & β \in T_+, & α \in v(β) & のとき & ⊥ \\
(D7) & α \in T_+, & β \in X , & β \notin v(α) & のとき & [β \mapsto α] \\
(D8) & α \in T_+, & β \in X , & β \in v(α) & のとき & ⊥ \\
(D9) & α \in T_f, & β \in T_g , & f = g & のとき & 以下を参照 \\
(D10) & α \in T_f, & β \in T_g , & f \ne g & のとき & ⊥ \\
\end{cases} と定義します。(D9)は \begin{cases}
σ \in Σ & のとき & σ \triangleright d(s, t) = σ \\
⊥ & のとき & ⊥ \triangleright d(s, t) = d(s, t) \\
\end{cases} としたとき \begin{eqnarray*}
(D9) & & u(f(s_1, s_2, \cdots, s_n), f(t_1, t_2, \cdots, t_n)) \\
& = & ⊥ \triangleright d(s_1, t_1) \triangleright d(s_2, t_2) \triangleright \cdots \triangleright d(s_n, t_n) \\
\end{eqnarray*} と定義します( \triangleright は左から順に適用)。こうすると  d帰納的に定義することができます。

 u(\alpha, \beta) u: T \times T \to \Sigma \sqcup \{\bot\} ( \bot は失敗を表す)を \begin{cases}
(U 1) & σ = d(α, β) \in Σ & & のとき & σ \succ u(α[σ], β[σ]) \\
(U 2) & d(α, β) = ⊥, & α = β & のとき & 1 \\
(U 3) & d(α, β) = ⊥, & α \ne β & のとき & ⊥ \\
\end{cases} と定義します( σ \succ ⊥ = ⊥ とします)。 v(\alpha) \cup v(\beta) は有限なのでこのように帰納的に定義することができます。

このとき \begin{cases}
u(α, β) \in Σ & のとき & u(α, β) \ は \ α, β \ の最汎単一化子 \\
u(α, β) = ⊥ & のとき & α, β \ は単一化不可能 \\
\end{cases} が成り立つことを以下で示します。

(UA1)  u(α, β) \in Σ ならば  u(α, β) α β の単一化子

[証明]  σ_0 = 1 \le σ_1 \le \cdots \le σ_n という列を \begin{cases}
(U1') & θ_i = d(α[σ_i], β[σ_i]) \in Σ & のとき & σ_{i+1} = σ_i \succ θ_i \\
(U 2'), (U3') & d(α[σ_i], β[σ_i]) = ⊥ & のとき & σ_i \ で列は終了 \\
\end{cases} とおくと  v(\alpha) \cup v(\beta) の元の個数以下の  n で列は終了します。よってこの列を帰納的に定義することができます。 d(α[σ_n], β[σ_n]) = ⊥ となります。

  • (U2')  α[σ_n] = β[σ_n] のとき  u(α, β) = σ_n となります。
  • (U3')  α[σ_n] \ne β[σ_n] のとき  u(α, β) = \bot となります。

よって  σ = u(α, β) \in Σ ならば  α[σ] = β[σ] が成り立ちます。[証明終わり]

(UA2)  \alpha \ne \beta かつ  \tau \alpha \beta の単一化子ならば  d(α, β) \in Σ かつ  d(α, β) \le τ

[証明]  \alpha \ne \beta かつ  \tau \alpha \beta の単一化子ならば  d(\alpha, \beta) は \begin{cases}
(D4) & α \in X, & β \in X, & α \ne β & のとき & [α \mapsto β] \\
(D5) & α \in X, & β \in T_+, & α \notin v(β) & のとき & [α \mapsto β] \\
(D7) & α \in T_+, & β \in X , & β \notin v(α) & のとき & [β \mapsto α] \\
(D9) & α \in T_f, & β \in T_g , & f = g & のとき & 以下を参照 \\
\end{cases} のどれかとなります。ここで(D9)は、 α = f(s_1, s_2, \cdots, s_n) β = f(t_1, t_2, \cdots, t_n) とすると、 d(\alpha, \beta) d(s_i, t_i) \in \Sigma となる最初の  d(s_i, t_i) となります。

(D4)、(D5)、(D7)のとき  d(\alpha, \beta) = [x \mapsto t] とすると \begin{cases}
(d(α, β) \succ τ)(x) = τ^*(t) = τ(x) \\
(d(α, β) \succ τ)(y) = τ(y) & (y \in X \setminus {x}) \\
\end{cases} より  d(α, β) \succ τ = τ d(α, β) \leq τ となります。

(D9)のとき任意の  i に対して  \tau s_i t_i の単一化子となります。 \alpha \ne \beta よりどれかの  \langle s_i, t_i \rangle の組は  s_i \ne t_i となります。この最初の組を  \langle s_{i_0}, t_{i_0} \rangle とおきます。

すべての  i に対する  s_i t_i に対して主張が成り立っていると仮定すると、 d(\alpha, \beta) = d(s_{i_0}, t_{i_0}) となります。よって  \alpha \beta に対しても主張が成り立ちます。[証明終わり]

(UA3)  \tau \alpha \beta の単一化子ならば  u(α, β) \in Σ かつ  u(α, β) \le τ

[証明] 上で定義した  σ_0 = 1 \le σ_1 \le \cdots \le σ_n という列を使って、 σ_n \in Σ かつ  σ_n \le τ であることを帰納的に示します。

 σ_0 \in Σ かつ  σ_0 \le τ は成り立っています。

 i < n とし、 σ_i \in Σ かつ  σ_i \le τ であると仮定します。

 α[σ_i] = β[σ_i] ならば主張は成り立っています。 α[σ_i] \ne β[σ_i] とします。

 σ_i \succ τ_i = τ とすると  α[σ_i][τ_i] = α[σ_i \succ τ_i] = α[τ] = β[τ] = β[σ_i \succ τ_i] = β[σ_i][τ_i] となり、 τ_i α[σ_i] β[σ_i] の単一化子となります。

(UA2)より  θ_i = d(α[σ_i], β[σ_i]) \in Σ かつ  θ_i \le τ_i となります。 σ_{i+1} = σ_i \succ θ_i \le σ_i \succ τ_i = τ となって  i+1 のときも成り立ちます。

よって帰納法により主張が成り立ちます。[証明終わり]

(UA4)  u(α, β) \in Σ ならば  u(α, β) α β の最汎単一化子

[証明]

  • (MGU1): (UA1)より  u(α, β) \alpha \beta の単一化子となります。
  • (MGU2): (UA3)より  \tau \alpha \beta の単一化子ならば  u(α, β) \le \tau となります。

[証明終わり]

中間報告(7)

このブログは、論理プログラミングを無限に実行する場合、実行順序を指定する機能を追加することを目的としています。現在は「無限の項書き換え」のような方法で記述する方法を検討しています。

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

項書き換えと同様の方法で群やリー代数で成り立つ関係を示すということをやっています。現在はマグマとモノイドで成り立つ関係について書いています。項書き換えの標準的な記述方法は『Universal Algebra for Computer Scientists (Monographs in Theoretical Computer Science. An EATCS Series, 25)』または『計算論理に基づく推論ソフトウェア論』に書かれていると思われますが、まだ全部読んでいないのでよくわかりません。また、項書き換えを無限に繰り返したものを扱うには「多項式の代入」の記述方法の方が良いのではないかと思われるため、現在はそのような記述方法になっています。この方法が有効かどうかはまだわかりません。

現在は環で成り立つ関係を示すということをやっています。この内容は『環の演算』で書いたものです。ここでは書き換え規則を合成するということをやっています。これを説明するために、現在は単一化について説明しています。単一化については『計算論理に基づく推論ソフトウェア論』に書かれているようなのでこの本を見ています。

今後は合成を無限に繰り返したものを記述する方法について考えていきます。このような記述方法があれば、数学の理論でプログラムとして記述することができるものがあると考えられます。このような記述方法がないために記述する方法がないという誤解があるという気がするので、それを解消したいと考えています。

代数的構造による圏論

現在は『圏論の道案内 ~矢印でえがく数学の世界~ 数学への招待』という本を随伴の項目まで読んでいます。「項書き換え」のような方法で随伴を記述するということが目標ですが、現在はまだ随伴のことがよくわかっていないので本の引用だけになっています。

数学的帰納法、可換モノイド、連立一次方程式については、残念ながらこの本にはこの後とくに記述がありませんでした。

前回の中間報告以降更新していない項目

エレファントな整数論

この項目も「項書き換え」のような方法で

の記述ができないか、今後考えていきます。

エレファントな線形代数

この項目も「項書き換え」のような方法で、連立一次方程式の解法や行列のランクなどを、行列を使わずに記述できるかを今後考えていきます。

エレファントな関数論

この項目も「項書き換え」のような方法で、コーシーの積分定理の証明について記述できないか、今後考えていきます。

群論の計算

この項目も「項書き換え」のような方法で、

  • 群の簡単な計算
  • 可解群の定義
  • 対称式の基本定理
  • ガロア理論の基本定理
  • 可解群と代数方程式の代数的解法の関係

について記述できないか、今後考えていきます。

今後の予定

現在は「無限の項書き換え」のような方法で数学の問題を記述する方法を検討しています。今後は他の方法も検討していき、プログラミング言語で表すことを目標としています。

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

一般マグマの多項式の単一化アルゴリズム(2)

この項目の内容は「一階の項」の理論と内容は同じものになると思われます。書き方を変えることで極限や普遍性について考えるときに多項式の考え方が使えると思うのですが、今のところどうなるかわかりません。

前回の  u(\alpha, \beta, \sigma) の定義は、 \alpha, \beta を固定しても、変化させても定義できるのですが、両方が混じっていたので変化させるように書き直します。また、記述が複雑になってしまったので  M[X] T として書き直します。

 T f_i(t_1, t_2, \cdots, t_n) という形の元の全体を  T_{f_i}、 T_{f_0} = M とします。すると、 T = X \cup T_{f_0} \cup T_{f_1} \cup T_{f_2} \cup \cdots \cup T_{f_m} となります。 T_+ = T_{f_0} \cup T_{f_1} \cup T_{f_2} \cup \cdots \cup T_{f_m} とします。

 \Sigma を置換全体の集合とします。 v(\alpha) \alpha の部分項として現れる  X の元全体の集合とします。

 u(\alpha, \beta) u: T \times T \to \Sigma \sqcup \{F\} ( F は失敗を表す)を(場合分け(*)) \begin{cases}
(1) & α \in M, & β \in M, & α = β & のとき & σ \\
(2) & α \in M, & β \in M, & α \ne β & のとき & F \\
(3) & α \in X, & β \in X, & α = β & のとき & σ \\
(4) & α \in X, & β \in X, & α \ne β & のとき & σ \succ (α \mapsto β) \\
(5) & α \in X, & β \in T_+, & α \notin v(β) & のとき & σ \succ (α \mapsto β) \\
(6) & α \in X, & β \in T_+, & α \in v(β) & のとき & F \\
(7) & α \in T_+, & β \in X , & β \notin v(α) & のとき & σ \succ (β \mapsto α) \\
(8) & α \in T_+, & β \in X , & β \in v(α) & のとき & F \\
(9) & α \in T_f, & β \in T_g , & f = g & のとき & 以下を参照 \\
(10) & α \in T_f, & β \in T_g , & f \ne g & のとき & F \\
\end{cases} と定義します(定義できるかどうかは以下で検討)。(9)は \begin{cases}
σ \in Σ & のとき & σ \triangleright u(s, t) = u(s[σ], t[σ]) \\
F & のとき & F \triangleright u(s, t) = F \\
\end{cases} としたとき \begin{eqnarray*}
(9) & & u(f(s_1, s_2, \cdots, s_n), f(t_1, t_2, \cdots, t_n)) \\
& = & 1 \triangleright u(s_1, t_1) \triangleright u(s_2, t_2) \triangleright \cdots \triangleright u(s_n, t_n) \\
\end{eqnarray*} と定義します( \triangleright は左から順に適用)。このとき \begin{cases}
u(α, β) = σ \in Σ & のとき & σ \ は \ α, β \ の最汎単一化子 \\
u(α, β) = F & のとき & α, β \ は単一化不可能 \\
\end{cases} が成り立ちます。

単一化アルゴリズムの定義

 u(\alpha, \beta) \alpha, \beta を変化させても定義できるならば、 u写像として定義できます。場合分け(*)の(1)から(10)の場合分けを1段階として、上位の部分項から順に実行することはアルゴリズムということができます。(9)の項は左から順に実行するとします。

 \alpha の部分項  f_i(t_1, t_2, \cdots, t_n) があるとき  f_i(t_1, t_2, \cdots, t_n) > t_j とします。 r+1 個の部分項が  t_0 > t_1 > \cdots > t_r という関係のとき  t_0 >^r t_r とします。 \alpha の部分項で  t >^r t' となる最大の  r r(\alpha) r(\alpha, \beta) = \max(r(\alpha), r(\beta)) とします。

 k(\alpha, \beta) v(\alpha) \cup v(\beta) の元の個数とします。

 k(\alpha, \beta) = 0 のとき、 u(\alpha, \beta) r(\alpha, \beta) 段階実行すると、ある  \sigma \in \Sigma または  F の結果を得ることができます。

 k= k(\alpha, \beta) とし、 u(\alpha, \beta) を段階的に実行して結果が得られるとき、その段階数を  s(\alpha, \beta) とします。結果が得られないとき、 s(\alpha, \beta) = \infty とします。

 r= r(\alpha, \beta) k= k(\alpha, \beta) のとき、 s(\alpha, \beta) の最大値があれば  t(r, k) とします。最大値がなければ  t(r, k) = \infty とします。

 k = 0 のとき  r = s(\alpha, \beta) = t(r, 0) となります。

 t(r, k) \le (2^{k+1}-1)r と仮定します。

 u(\alpha, \beta) r(\alpha, \beta) 段階実行すると、 \alpha または  \beta の部分項に  X の元が出現します。最初に現れた  X の元に対応する項を代入したものを  \alpha', \beta' とします。すると  r(\alpha', \beta') \le 2r(\alpha, \beta) k(\alpha', \beta') = k-1 となります。

帰納法の仮定より \begin{eqnarray*}
& & t(r(α', β'), k(α', β')) \\
& \le & r + (2^{k(α', β')+1}-1)r(α', β') \\
& \le & r + (2^{ (k - 1 ) + 1 }- 1) \cdot 2r \\
& = & (2^{k+1}-1)r
\end{eqnarray*} となって、任意の  \alpha, \beta に対して  t(r(\alpha, \beta), k(\alpha, \beta)) \le (2^{k(\alpha, \beta)+1}-1)r(\alpha, \beta) が成り立ちます。

よって  s(\alpha, \beta) \le t(r, k) \le (2^{k+1}-1)r となります。 u(\alpha, \beta) \alpha, \beta を変化させても定義できるので写像となり、上位の部分項から順に実行する手順はアルゴリズムということができます。