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

一般マグマの多項式の単一化

環(および自然数の演算)(日本語が正しく表示されない可能性がありますがいつか書き直します)の使い方を説明すると書きましたが、ここで行っている「規則の合成」を説明するには単一化(ユニフィケーション)について説明する必要があるのでまずそこから説明します。

「wikipedia:ユニフィケーション」(Wikipedia)の項目に書かれている内容と同じなのですが、Wikipediaの用語はわかりにくいので、「最汎単一化子 (most general unifier, MGU)」(これは一般的な用語です。Wikipediaでは最大汎用単一子)という用語を使って説明します。また、「多項式の代入」を使って説明したほうが今後の説明がわかりやすくなると思われるため、その方針で説明します。

を一般マグマの多項式(Wikipediaでは「一階の項」と呼ばれているものに相当します)とします。 から への写像を置換(これはWikipediaでも使われていますが一般的な用語のようです)と呼びます。「多項式」 に置換 を「代入」したものを とします( は を拡張したただ一つの一般マグマの準同型)。

に対して、置換 が存在して となるとき、 と は単一化可能といって、 を単一化子と呼びます。

置換 に対して、 を満たす一般マグマの準同型 が存在するとき と書くことにします。

と が単一化可能であるとき、 が と の単一化子ならば となる単一化子 が存在します。 を最汎単一化子と呼びます。

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

の演算を とします。演算の結果を のように写像の形で書くことにします。 の という形の元の全体を とすると、 となります。、 とします。

を置換全体の集合とします。、 に対して、置換 を \begin{cases}
x \mapsto \alpha \\
y \mapsto \alpha & (y \ne x) \\
\end{cases} という写像とし、 を拡張したただ一つの一般マグマの準同型を 、 置換 に対して を と書くことにします。

を の部分項として現れる の元全体の集合とします。 ( は失敗を表す)、 を \begin{cases}
α[σ] \in M, & β[σ] \in M, & α[σ] = β[σ] & のとき & σ \\
α[σ] \in M, & β[σ] \in M, & α[σ] \ne β[σ] & のとき & F \\
α[σ] \in X, & β[σ] \in X, & α[σ] = β[σ] & のとき & σ \\
α[σ] \in X, & β[σ] \in M[X]_+, & α[σ] \notin v(β[σ]) & のとき & σ \succ (α[σ] \mapsto β[σ]) \\
α[σ] \in X, & β[σ] \in M[X]_+, & α[σ] \in v(β[σ]) & のとき & F \\
α[σ] \in M[X]_+, & β[σ] \in X , & β[σ] \notin v(α[σ]) & のとき & σ \succ (β[σ] \mapsto α[σ]) \\
α[σ] \in M[X]_+, & β[σ] \in X , & β[σ] \in v(α[σ]) & のとき & F \\
α[σ] \in M[X]_f, & β[σ] \in M[X]_g , & f = g & のとき & 以下の(*)を参照 \\
α[σ] \in M[X]_f, & β[σ] \in M[X]_g , & f \ne g & のとき & F \\
\end{cases} と(演算の回数に関して)帰納的に定義することができます。(*)は \begin{cases}
σ \in Σ & のとき & σ \triangleright u(s, t) = u(s[σ], t[σ], σ) \\
F & のとき & F \triangleright u(s, t) = F \\
\end{cases} としたとき \begin{eqnarray*}
(*) & & u(f(s_1, s_2, \cdots, s_n), f(t_1, t_2, \cdots, t_n), σ) \\
& = & σ \triangleright u(s_1, t_1) \triangleright u(s_2, t_2) \triangleright \cdots \triangleright u(s_n, t_n) \\
\end{eqnarray*} と定義します。

を の恒等写像を から への写像とみなした置換とします。\begin{cases}
u(α, β, 1) = σ \in Σ & のとき & σ \ は \ α, β \ の最汎単一化子 \\
u(α, β, 1) = F & のとき & α, β \ は単一化不可能 \\
\end{cases} が成り立ちます。この結果は項の順序に依存しません。

Universal Algebra for Computer Scientists (Monographs in Theoretical Computer Science. An EATCS Series, 25)

新しいプログラミング・パラダイム

岩波講座 ソフトウェア科学〈〔理論〕12〉計算モデルの基礎理論

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

環の性質(2)

任意の 項演算を任意の個数もつ代数的構造に対しても「±マグマ」と同様の議論が成り立ちます。これを「一般マグマ」と呼ぶことにします。「一般マグマ」によって環の性質を証明することができます。

前回の続きを書いていきます。\begin{cases}
\rho_{1} & = & ( & x & \mapsto & 0 + x & \to & x & ) \\
\rho_{2} & = & ( & x & \mapsto & x & \to & 0 + x & ) \\
\rho_{3} & = & ( & x & \mapsto & x + 0 & \to & x & ) \\
\rho_{4} & = & ( & x & \mapsto & x & \to & x + 0 & ) \\
\rho_{5} & = & ( & x & \mapsto & (-x) + x & \to & 0 & ) \\
\rho_{6} & = & ( & x & \mapsto & 0 & \to & (-x) + x & ) \\
\rho_{7} & = & ( & x & \mapsto & x + (-x) & \to & 0 & ) \\
\rho_{8} & = & ( & x & \mapsto & 0 & \to & x + (-x) & ) \\
\rho_{9} & = & ( & x, y, z & \mapsto & (x + y) + z & \to & x + (y + z) & ) \\
\rho_{10} & = & ( & x, y, z & \mapsto & x + (y + z) & \to & (x + y) + z & ) \\
\rho_{11} & = & ( & x, y, z & \mapsto & (x y) z & \to & x (y z) & ) \\
\rho_{12} & = & ( & x, y, z & \mapsto & x (y z) & \to & (x y) z & ) \\
\rho_{13} & = & ( & y, x, z & \mapsto & x (y + z) & \to & x y + x z & ) \\
\rho_{14} & = & ( & x, y, z & \mapsto & x y + x z & \to & x (y + z) & ) \\
\rho_{15} & = & ( & x, y, z & \mapsto & (x + y) z & \to & x z + y z & ) \\
\rho_{16} & = & ( & x, y, z & \mapsto & x z + y z & \to & (x + y) z & ) \\
\rho_{17} & = & ( & x & \mapsto & x 0 & \to & 0 & ) \\
\rho_{18} & = & ( & x & \mapsto & 0 & \to & x 0 & ) \\
\rho_{19} & = & ( & x & \mapsto & 0 x & \to & 0 & ) \\
\rho_{20} & = & ( & x & \mapsto & 0 & \to & 0 x & ) \\
\end{cases} から \begin{matrix}
x ( -y ) & \xrightarrow{\rho_{4}} & x ( -y ) + 0 \\
& \xrightarrow{\rho_{8}} & x ( -y ) + ( x_{8,2} + ( -x_{8,2} ) ) \\
& \xrightarrow{\rho_{10}} & ( x ( -y ) + y_{10,3} ) + ( -y_{10,3} ) \\
& \xrightarrow{\rho_{14}} & x ( ( -y ) + z_{14,4} ) + ( -x z_{14,4} ) \\
& \xrightarrow{\rho_{5}} & x 0 + ( -x y ) \\
& \xrightarrow{\rho_{17}} & 0 + ( -x y ) \\
& \xrightarrow{\rho_{1}} & -x y \\
( -x ) y & \xrightarrow{\rho_{4}} & ( -x ) y + 0 \\
& \xrightarrow{\rho_{8}} & ( -x ) y + ( x_{8,2} + ( -x_{8,2} ) ) \\
& \xrightarrow{\rho_{10}} & ( ( -x ) y + y_{10,3} ) + ( -y_{10,3} ) \\
& \xrightarrow{\rho_{16}} & ( ( -x ) + y_{16,4} ) y + ( -y_{16,4} y ) \\
& \xrightarrow{\rho_{5}} & 0 y + ( -x y ) \\
& \xrightarrow{\rho_{19}} & 0 + ( -x y ) \\
& \xrightarrow{\rho_{1}} & -x y \\
\end{matrix} が成り立ちます。

\begin{cases}
\rho_{21} & = & ( & x, y & \mapsto & x (-y) & \to & -x y & ) \\
\rho_{22} & = & ( & x, y & \mapsto & -x y & \to & x (-y) & ) \\
\rho_{23} & = & ( & x, y & \mapsto & (-x) y & \to & -x y & ) \\
\rho_{24} & = & ( & x, y & \mapsto & -x y & \to & (-x) y & ) \\
\end{cases} を追加すると \begin{matrix}
( -x ) ( -y ) & \xrightarrow{\rho_{21}} & -( -x ) y \\
& \xrightarrow{\rho_{23}} & -( -x y ) \\
& \xrightarrow{\rho_{4}} & ( -( -x y ) ) + 0 \\
& \xrightarrow{\rho_{6}} & ( -( -x y ) ) + ( ( -x_{6,4} ) + x_{6,4} ) \\
& \xrightarrow{\rho_{10}} & ( ( -( -x y ) ) + ( -z_{10,5} ) ) + z_{10,5} \\
& \xrightarrow{\rho_{5}} & 0 + x y \\
& \xrightarrow{\rho_{1}} & x y \\
\end{matrix} が成り立ちます。

から に \begin{cases}
\rho_{21} & = & ( & x & \mapsto & 1 x & \to & x & ) \\
\rho_{22} & = & ( & x & \mapsto & x & \to & 1 x & ) \\
\rho_{23} & = & ( & x & \mapsto & x 1 & \to & x & ) \\
\rho_{24} & = & ( & x & \mapsto & x & \to & x 1 & ) \\
\end{cases} を追加すると \begin{matrix}
x + y & \xrightarrow{\rho_{4}} & ( x + y ) + 0 \\
& \xrightarrow{\rho_{8}} & ( x + y ) + ( x_{8,2} + ( -x_{8,2} ) ) \\
& \xrightarrow{\rho_{10}} & ( ( x + y ) + y_{10,3} ) + ( -y_{10,3} ) \\
& \xrightarrow{\rho_{9}} & ( x + ( y + z_{9,4} ) ) + ( -z_{9,4} ) \\
& \xrightarrow{\rho_{2}} & ( 0 + ( x + ( y + z_{9,4} ) ) ) + ( -z_{9,4} ) \\
& \xrightarrow{\rho_{6}} & ( ( ( -x_{6,6} ) + x_{6,6} ) + ( x + ( y + z_{9,4} ) ) ) + ( -z_{9,4} ) \\
& \xrightarrow{\rho_{9}} & ( ( -y_{9,7} ) + ( y_{9,7} + ( x + ( y + z_{9,4} ) ) ) ) + ( -z_{9,4} ) \\
& \xrightarrow{\rho_{10}} & ( ( -x_{10,8} ) + ( ( x_{10,8} + x ) + ( y + z_{9,4} ) ) ) + ( -z_{9,4} ) \\
& \xrightarrow{\rho_{22}} & ( ( -x_{10,8} ) + ( ( x_{10,8} + x ) + ( y + 1 x_{22,9} ) ) ) + ( -x_{22,9} ) \\
& \xrightarrow{\rho_{22}} & ( ( -x_{10,8} ) + ( ( x_{10,8} + x ) + ( 1 y + 1 x_{22,9} ) ) ) + ( -x_{22,9} ) \\
& \xrightarrow{\rho_{24}} & ( ( -x_{10,8} ) + ( ( x_{10,8} + x 1 ) + ( 1 y + 1 x_{22,9} ) ) ) + ( -x_{22,9} ) \\
& \xrightarrow{\rho_{14}} & ( ( -x_{10,8} ) + ( ( x_{10,8} + x 1 ) + 1 ( y + z_{14,12} ) ) ) + ( -z_{14,12} ) \\
& \xrightarrow{\rho_{14}} & ( ( -x y_{14,13} ) + ( x ( y_{14,13} + 1 ) + 1 ( y + z_{14,12} ) ) ) + ( -z_{14,12} ) \\
& \xrightarrow{\rho_{16}} & ( ( -x y ) + ( x + 1 ) ( y + 1 ) ) + ( -1 ) \\
& \xrightarrow{\rho_{13}} & ( ( -x y ) + ( ( x + 1 ) y + ( x + 1 ) 1 ) ) + ( -1 ) \\
& \xrightarrow{\rho_{15}} & ( ( -x y ) + ( ( x y + 1 y ) + ( x + 1 ) 1 ) ) + ( -1 ) \\
& \xrightarrow{\rho_{15}} & ( ( -x y ) + ( ( x y + 1 y ) + ( x 1 + 1 \cdot 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{21}} & ( ( -x y ) + ( ( x y + y ) + ( x 1 + 1 \cdot 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{23}} & ( ( -x y ) + ( ( x y + y ) + ( x + 1 \cdot 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{21}} & ( ( -x y ) + ( ( x y + y ) + ( x + 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{9}} & ( ( -x y ) + ( x y + ( y + ( x + 1 ) ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{10}} & ( ( ( -x y ) + x y ) + ( y + ( x + 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{5}} & ( 0 + ( y + ( x + 1 ) ) ) + ( -1 ) \\
& \xrightarrow{\rho_{1}} & ( y + ( x + 1 ) ) + ( -1 ) \\
& \xrightarrow{\rho_{10}} & ( ( y + x ) + 1 ) + ( -1 ) \\
& \xrightarrow{\rho_{9}} & ( y + x ) + ( 1 + ( -1 ) ) \\
& \xrightarrow{\rho_{7}} & ( y + x ) + 0 \\
& \xrightarrow{\rho_{3}} & y + x \\
\end{matrix} が成り立ちます。

さらに \begin{cases}
\rho_{25} & = & ( & & \mapsto & 1 & \to & 0 & ) \\
\rho_{26} & = & ( & & \mapsto & 0 & \to & 1 & ) \\
\end{cases} を追加すると \begin{matrix}
x & \xrightarrow{\rho_{22}} & 1 x & \xrightarrow{\rho_{25}} & 0 x & \xrightarrow{\rho_{19}} & 0 \\
\end{matrix} が成り立ちます。

Universal Algebra for Computer Scientists (Monographs in Theoretical Computer Science. An EATCS Series, 25)

新しいプログラミング・パラダイム

岩波講座 ソフトウェア科学〈〔理論〕12〉計算モデルの基礎理論

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

±マグマ

集合 が二項演算 と単項演算 を持つとき を±マグマと呼ぶことにします。「単項・二項マグマ」と呼んでいましたが長いのでこう呼ぶことにします。ここでは、マグマに関する議論に演算を付け加えたものをまとめて説明していきます。

この議論に関する一般論があると思うのですが、ウェブで検索しても見つかりませんでした。「Universal Algebra for Computer Scientists」という本に少し書かれているようです。この本を持っているので今後読んでみたいと思います。「完備化」についてはWikipediaに「クヌース・ベンディックス完備化アルゴリズム」という記事があります。「完備化」についても今後調査したいと思います。

部分±マグマ

を±マグマとします。 に対して 、 と書くことにします。 が 、 を満たすとき は 、 の への制限に関して±マグマとなります。このような を の部分±マグマと呼ぶことにします。

±マグマの準同型

±マグマ から±マグマ への写像 が演算を保存するとき、すなわち

• 
• 

を満たすとき、 を±マグマ から±マグマ への±マグマの準同型と呼びます。

部分集合で生成された部分±マグマ

を±マグマ の部分集合とします。 に対して、 が を含む の部分マグマであり、 を含む の部分±マグマの最小のものであるとき、 を で生成された の部分±マグマと呼ぶことにします。±マグマ が で生成された の部分±マグマであるとき を で生成された±マグマと呼ぶことにします。

は で生成された の部分±マグマとなります。

±マグマの「多項式」

±マグマと と集合 の元に、「 」、「」、「」、「」をを付け加えたものからなる、有限個の列全体の集合を とします。

だけの長さ の列を とし、 とします。同様に だけの長さ の列を とし、 とします。 に対して となる を とします。

に二項演算 を \begin{cases}
α \boxplus β = [\grave{α} + \grave{β}] & (α, β \in M' \ のとき) \\
α \boxplus β = (\!\!(α \oplus β)\!\!) & (それ以外のとき) \\
\end{cases}、単項演算 を \begin{cases}
\boxminus α = [- \grave{α}] & (α \in M' \ のとき) \\
\boxminus α = (\!\!(\ominus α)\!\!) & (それ以外のとき) \\
\end{cases} と定義すると は±マグマとなります。

で生成された の部分±マグマを と書くことにします。 の演算を 、 と書くことにします。以下では を 、 を と書きます。

「多項式」からの写像の準同型への拡張

の台集合 の部分集合 に対して \begin{cases}
B^{\pm(1)} = B \\
B^{\pm(n+1)} = (B^{\pm(n)} + B^{\pm(n)}) \cup (- B^{\pm(n)}) \\
\end{cases} と帰納的に を定義します。 となります。

を±マグマ、 を単射( は集合の直和)、 の への制限が±マグマの準同型であるとします。

に対して が存在します。 または となる が存在する( とします)か、または となる が存在します( とします)。\begin{cases}
g^*(\alpha) = g(\alpha) & (\alpha \in M \cup X \ のとき) \\
g^*(\alpha) = g^*(\beta) + g^*(\gamma) & (\alpha \in M[X]^+, \alpha = \beta + \gamma \ のとき) \\
g^*(\alpha) = - g^*(\beta) & (\alpha \in M[X]^-, \alpha = - \beta \ のとき) \\
\end{cases} と帰納的に定義することにより、±マグマの準同型 を定義することができます。

「多項式」への「代入」

とすると、上の議論により、 を拡張した を保存する±マグマの準同型 が一意的に存在します。

に対して と定義します。 のとき を と書くことにします。これを の に を代入する、または に を代入するということにします。 を代入写像と呼ぶことにします。

を を に写す写像とします。 のとき を を に写す写像とします。これは を に写す写像となります。これらを の「ラムダ式化」と呼ぶことにします。

部分項の位置

に対して、 となる が一意的に存在します。 を に写す写像を 、 を に写す写像を と定義することができます。 のときは に含まれない元 (失敗を表す)を追加した を考え、 と定義することによってこれらを拡張して、 とします。さらに と定義することによって拡張して、 とします。

同様に、 に対して、 となる が一意的に存在します。 を に写す写像を と定義することができます。 のときは と定義することによって拡張して、 とします。さらに と定義することによって拡張して、 とします。

を 、 を 、 を と書くことにすると \begin{cases}
α L = α_L & (α \in M[X]^+) \\
α L = ⊥ & (α \in M[X] \setminus M[X]^+) \\
⊥ L = ⊥
\end{cases} \begin{cases}
α R = α_L & (α \in M[X]^+) \\
α R = ⊥ & (α \in M[X] \setminus M[X]^+) \\
⊥ R = ⊥
\end{cases} \begin{cases}
α B = α_B & (α \in M[X]^-) \\
α B = ⊥ & (α \in M[X] \setminus M[X]^-) \\
⊥ B = ⊥
\end{cases} となります。

各 を 、 または としたとき、すべての自然数 に対する 全体の集合 を考えます。

であることから が存在するので、すべての に対する 全体の集合を とすると となります。

の元を の部分項と呼ぶことにします。 の部分項を と表したときの最も小さい に対応する 全体の集合を とします。 を の部分項 の位置と呼ぶことにします。

の位置 を で置き換えた を \begin{cases}
β & (n = 0) \\
L(α)(δ_2 \cdots δ_n \gets β) + R(α) & (n>0, δ_1 = L) \\
L(α) + R(α)(δ_2 \cdots δ_n \gets β) & (n>0, δ_1 = R) \\
- B(α)(δ_2 \cdots δ_n \gets β) & (n>0, δ_1 = B) \\
\end{cases} と帰納的に定義します。 のときの位置を と書くことにします。

書き換え規則

とします。 の順序のついた組 の「ラムダ式化」 を上の議論と同様に考えることができます。これを書き換え規則と呼び、 と書くことにします。

に対して、代入写像 が存在して、ある の部分項の位置 に対して となるとき、 は書き換え規則 によって書き換え可能ということにします。 の部分項の位置 を で置き換えた を書き換え後の項と呼ぶことにします。これを \begin{eqnarray*}
α & \xrightarrow{ρ, σ, p} & α(p \gets γ[σ])
\end{eqnarray*} または \begin{eqnarray*}
α & \xrightarrow{ρ} & α(p \gets γ[σ])
\end{eqnarray*} と書くことにします。

Universal Algebra for Computer Scientists (Monographs in Theoretical Computer Science. An EATCS Series, 25)

新しいプログラミング・パラダイム

岩波講座 ソフトウェア科学〈〔理論〕12〉計算モデルの基礎理論

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

環の性質

「群の性質」で考えた「単項・二項マグマ」に二項演算を付け加えたものを考えます。これをここでは「単項・二項・二項マグマ」と呼ぶことにします。「単項・二項・二項マグマ」について「代入」を考えることで「群の性質」と同様に環で成り立つ関係を求めることができます。

Ring でこの式の変形ができるようになっているのですが、群の場合と違って半自動的にできるようになっていないので、式の変形のやり方がわかっていないとできません。以下で説明します。

環の定義から得られる関係

集合 に二つの二項演算 (加法)、 (乗法)が定義されていて、 次の条件が成り立っているとき、 は環であるといいます。

1. 加法に関して可換群である。 すなわち
   1. (結合法則)(associative law) が成り立つ。
   2. (交換法則)(commutative law) が成り立つ。
   3. ある の元 が存在して、すべての の元 に対し が成り立つ。 を の零元(zero element)という。
   4. すべての の元 に対して、 の元 が存在して が成り立つ。 を と書く。
2. 乗法に関して結合法則が成り立つ。すなわち が成り立つ。
3. 分配法則(distributive law)が成り立つ。すなわち
   1. 、
   2. 

の乗法に関する単位元を単に単位元と呼びます。単位元を と書きます。以下の関係が成り立ちます。

• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 

これは長くてわかりにくいので、加法の結合法則 が成り立つことを考慮して を と書くことにして書き直すと

• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 
• 

となります。よって

• 環の定義(加法の交換法則を除く)から、、、 が成り立ちます。
• 環の定義(加法の交換法則を除く)と単位元の存在から、 が成り立ちます。
• 環の定義(加法の交換法則を除く)と単位元の存在から、 ならば任意の に対して が成り立ちます。

「単項・二項・二項マグマ」の「代入」による方法

「単項・二項・二項マグマ」の「代入」による式の変形によってこの関係を求めることができます。\begin{cases}
\rho_{1} & = & ( & x & \mapsto & 0 + x & \to & x & ) \\
\rho_{2} & = & ( & x & \mapsto & x & \to & 0 + x & ) \\
\rho_{3} & = & ( & x & \mapsto & x + 0 & \to & x & ) \\
\rho_{4} & = & ( & x & \mapsto & x & \to & x + 0 & ) \\
\rho_{5} & = & ( & x & \mapsto & (-x) + x & \to & 0 & ) \\
\rho_{6} & = & ( & x & \mapsto & 0 & \to & (-x) + x & ) \\
\rho_{7} & = & ( & x & \mapsto & x + (-x) & \to & 0 & ) \\
\rho_{8} & = & ( & x & \mapsto & 0 & \to & x + (-x) & ) \\
\rho_{9} & = & ( & x, y, z & \mapsto & (x + y) + z & \to & x + (y + z) & ) \\
\rho_{10} & = & ( & x, y, z & \mapsto & x + (y + z) & \to & (x + y) + z & ) \\
\rho_{11} & = & ( & x, y, z & \mapsto & (x y) z & \to & x (y z) & ) \\
\rho_{12} & = & ( & x, y, z & \mapsto & x (y z) & \to & (x y) z & ) \\
\rho_{13} & = & ( & y, x, z & \mapsto & x (y + z) & \to & x y + x z & ) \\
\rho_{14} & = & ( & x, y, z & \mapsto & x y + x z & \to & x (y + z) & ) \\
\rho_{15} & = & ( & x, y, z & \mapsto & (x + y) z & \to & x z + y z & ) \\
\rho_{16} & = & ( & x, y, z & \mapsto & x z + y z & \to & (x + y) z & ) \\
\end{cases} から \begin{matrix}
x 0 & \xrightarrow{\rho_{4}} & x 0 + 0 & \xrightarrow{\rho_{8}} & x 0 + ( x_{8,2} + ( -x_{8,2} ) ) \\ & \xrightarrow{\rho_{10}} & ( x 0 + y_{10,3} ) + ( -y_{10,3} ) & \xrightarrow{\rho_{14}} & x ( 0 + z_{14,4} ) + ( -x z_{14,4} ) \\ & \xrightarrow{\rho_{1}} & x x_{1,5} + ( -x x_{1,5} ) & \xrightarrow{\rho_{7}} & 0 \\
0 x & \xrightarrow{\rho_{4}} & 0 x + 0 & \xrightarrow{\rho_{8}} & 0 x + ( x_{8,2} + ( -x_{8,2} ) ) \\ & \xrightarrow{\rho_{10}} & ( 0 x + y_{10,3} ) + ( -y_{10,3} ) & \xrightarrow{\rho_{16}} & ( 0 + y_{16,4} ) x + ( -y_{16,4} x ) \\ & \xrightarrow{\rho_{1}} & x_{1,5} x + ( -x_{1,5} x ) & \xrightarrow{\rho_{7}} & 0 \\
\end{matrix} が得られます。この続きは次回以降で説明したいと思います。

新しいプログラミング・パラダイム

岩波講座 ソフトウェア科学〈〔理論〕12〉計算モデルの基礎理論

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

群の性質(2)

今回は群の性質の続きを調べていきます。

前回の結果

「エレファントな群とリー代数(3)」では書き換え規則の集合 \begin{cases}
\rho_{1} & = & ( & x & \mapsto & e x & \to & x & ) \\
\rho_{2} & = & ( & x & \mapsto & x & \to & e x & ) \\
\rho_{3} & = & ( & x & \mapsto & x^{-1} x & \to & e & ) \\
\rho_{4} & = & ( & x & \mapsto & e & \to & x^{-1} x & ) \\
\rho_{5} & = & ( & x, y, z & \mapsto & (x y) z & \to & x (y z) & ) \\
\rho_{6} & = & ( & x, y, z & \mapsto & x (y z) & \to & (x y) z & ) \\
\rho_{7} & = & ( & x & \mapsto & e^{-1} x & \to & x & ) \\
\rho_{8} & = & ( & x & \mapsto & x & \to & e^{-1} x & ) \\
\rho_{9} & = & ( & x & \mapsto & (e^{-1})^{-1} x & \to & x & ) \\
\rho_{10} & = & ( & x & \mapsto & x & \to & (e^{-1})^{-1} x & ) \\
\end{cases} により から \begin{matrix}
e^{-1} x & \xrightarrow{\rho_{2}} & e^{-1} (e x) & \xrightarrow{\rho_{6}} & (e^{-1} e) x & \xrightarrow{\rho_{3}} & e x & \xrightarrow{\rho_{1}} & x \\
\end{matrix} から \begin{matrix}
(e^{-1})^{-1} x & \xrightarrow{\rho_{8}} & (e^{-1})^{-1} (e^{-1} x) & \xrightarrow{\rho_{6}} & ((e^{-1})^{-1} e^{-1}) x & \xrightarrow{\rho_{3}} & e x & \xrightarrow{\rho_{1}} & x \\
\end{matrix} から \begin{matrix}
e^{-1} & \xrightarrow{\rho_{10}} & (e^{-1})^{-1} e^{-1} & \xrightarrow{\rho_{3}} & e \\
\end{matrix} が得られました。

前回の続き

以下の規則を付け加えます。\begin{cases}
\rho_{11} & = & ( & & \mapsto & e^{-1} & \to & e & ) \\
\rho_{12} & = & ( & & \mapsto & e & \to & e^{-1} & ) \\
\rho_{13} & = & ( & x & \mapsto & (x^{-1})^{-1} e & \to & x & ) \\
\rho_{14} & = & ( & x & \mapsto & x & \to & (x^{-1})^{-1} e & ) \\
\rho_{15} & = & ( & x & \mapsto & (x^{-1})^{-1} & \to & x & ) \\
\rho_{16} & = & ( & x & \mapsto & x & \to & (x^{-1})^{-1} & ) \\
\rho_{17} & = & ( & x & \mapsto & x x^{-1} & \to & e & ) \\
\rho_{18} & = & ( & x & \mapsto & e & \to & x x^{-1} & ) \\
\rho_{19} & = & ( & x & \mapsto & x e & \to & x & ) \\
\rho_{20} & = & ( & x & \mapsto & x & \to & x e & ) \\
\rho_{21} & = & ( & x, y & \mapsto & (x y)^{-1} x & \to & y^{-1} & ) \\
\rho_{22} & = & ( & y, x & \mapsto & y^{-1} & \to & (x y)^{-1} x & ) \\
\end{cases} から \begin{matrix}
( x^{-1} )^{-1} e & \xrightarrow{\rho_{4}} & ( x^{-1} )^{-1} ( x_{4,0}^{-1} x_{4,0} ) & \xrightarrow{\rho_{6}} & ( ( x^{-1} )^{-1} z_{6,1}^{-1} ) z_{6,1} & \xrightarrow{\rho_{3}} & e x & \xrightarrow{\rho_{1}} & x \\
\end{matrix} から \begin{matrix}
( x^{-1} )^{-1} & \xrightarrow{\rho_{14}} & ( ( ( x^{-1} )^{-1} )^{-1} )^{-1} e & \xrightarrow{\rho_{2}} & ( ( ( x^{-1} )^{-1} )^{-1} )^{-1} ( e e ) \\ & \xrightarrow{\rho_{6}} & ( ( ( ( x^{-1} )^{-1} )^{-1} )^{-1} e ) e & \xrightarrow{\rho_{13}} & ( x^{-1} )^{-1} e & \xrightarrow{\rho_{13}} & x \\
\end{matrix} から \begin{matrix}
x x^{-1} & \xrightarrow{\rho_{16}} & ( x^{-1} )^{-1} x^{-1} & \xrightarrow{\rho_{3}} & e \\
x e & \xrightarrow{\rho_{16}} & ( x^{-1} )^{-1} e & \xrightarrow{\rho_{13}} & x \\
\end{matrix} から \begin{matrix}
( x y )^{-1} x & \xrightarrow{\rho_{20}} & ( x y )^{-1} ( x e ) & \xrightarrow{\rho_{18}} & ( x y )^{-1} ( x ( x_{18,1} x_{18,1}^{-1} ) ) \\ & \xrightarrow{\rho_{6}} & ( x y )^{-1} ( ( x y_{6,2} ) y_{6,2}^{-1} ) & \xrightarrow{\rho_{6}} & ( ( x y )^{-1} ( x y_{6,2} ) ) y_{6,2}^{-1} \\ & \xrightarrow{\rho_{3}} & e y^{-1} & \xrightarrow{\rho_{1}} & y^{-1} \\
\end{matrix} から \begin{matrix}
( x y )^{-1} & \xrightarrow{\rho_{20}} & ( x y )^{-1} e & \xrightarrow{\rho_{18}} & ( x y )^{-1} ( x_{18,1} x_{18,1}^{-1} ) \\ & \xrightarrow{\rho_{6}} & ( ( x y )^{-1} y_{6,2} ) y_{6,2}^{-1} & \xrightarrow{\rho_{21}} & y^{-1} x^{-1} \\
\end{matrix} が得られます。これで群の完備化で書いた関係が得られました。

文献(本)

新しいプログラミング・パラダイム

岩波講座 ソフトウェア科学〈〔理論〕12〉計算モデルの基礎理論

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

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

を単位元 をもつマグマ、 を単位元 をもつマグマ、 をマグマの準同型とします。このとき ならば が成り立ちます。

これを「マグマの左単位元・右単位元」と同様の方法で証明することができます。項を に属する項と に属する項に分けて、 に属する変数には に属する項を代入可能、 に属する変数には に属する項を代入可能とします。 を単項演算と同様ですが であるものとします。

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

[証明] 書き換え規則を \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}
f(e) & \xrightarrow{\rho_{4}} & f(e) e' & \xrightarrow{\rho_{8}} & f(e) f(x) & \xrightarrow{\rho_{6}} & f(e x) & \xrightarrow{\rho_{1}} & f(x) & \xrightarrow{\rho_{7}} & e' \\
\end{matrix} と変形することができて が成り立つことがわかります。[証明終わり]

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

を単位元 をもつマグマ、 を単位元 をもつマグマ、 をマグマの準同型、 とします。このとき が の逆元ならば は の逆元となります。

[証明] 書き換え規則を \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}
f(x^{-1}) f(x) & \xrightarrow{\rho_{4}} & f(x^{-1} x) & \xrightarrow{\rho_{1}} & f(e) & \xrightarrow{\rho_{5}} & e' \\
\end{matrix} が得られます。[証明終わり]

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

を単位元 をもつマグマ、 を単位元 をもつマグマ、 をマグマの準同型とします。このとき が の逆元、 が の逆元ならば となります。

[証明] 書き換え規則を \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}
f(e) & \xrightarrow{\rho_{2}} & f(x^{-1} x) & \xrightarrow{\rho_{3}} & f(x^{-1}) f(x) & \xrightarrow{\rho_{5}} & e' \\
\end{matrix} が得られます。[証明終わり]

新しいプログラミング・パラダイム

岩波講座 ソフトウェア科学〈〔理論〕12〉計算モデルの基礎理論

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

群の性質

本[1][2]の中で「群の完備化」として、群の定義の一部から出発して完備な書き換え規則を得る手順が書かれています。こちらの私のサイト http://www2.biglobe.ne.jp/~optimist/algebra/word_2.html でもやっているのですが、本では有限回で終了して完備な書き換え規則が自動的に得られるようにできると書かれていますが具体的な方法がわからないので、私のサイトでは自動的にはできません。「群の完備化」については「クヌース・ベンディックス完備化アルゴリズム」でできるということで、これについてはまた後で調査したいと思います。

ここでは「マグマの左単位元・右単位元」と同様の方法で群で成立する関係を求めるということをやります。

集合 に演算 が定義されていて(この演算子は省略して書きます)、 次の3条件が成り立っているとき、 は群であるといいます。

1. (結合法則)
2. ある の元 が存在して、すべての の元 に対し が成り立つ。 を の単位元という。
3. すべての の元 に対して、 の元 が存在して が成り立つ。 を の逆元といい、 と書く。

これは、次の条件と同値となります。

1. 
2. ある の元 が存在して、すべての の元 に対し が成り立つ。
3. すべての の元 に対して、 の元 が存在して が成り立つ。

単項・二項マグマ

単項演算 、二項演算 を持つ代数的構造をここでは「単項・二項マグマ」と呼ぶことにします(一般的な名前は不明です)。自由「単項・二項マグマ」について、自由マグマと同様の議論ができます。

次の3個の書き換え規則 \begin{eqnarray*}
e x & \to & x \\
x^{-1} x & \to & e \\
(x y) z & \to & x (y z) \\
\end{eqnarray*} の集合から出発して、以下の書き換え規則の集合を得る方法が本には書かれています。 \begin{eqnarray*}
e x & \to & x \\
x^{-1} x & \to & e \\
(x y) z & \to & x (y z) \\
x^{-1} (x y) & \to & y \\
x e & \to & x \\
(x^{-1})^{-1} & \to & x \\
x x^{-1} & \to & e \\
e^{-1} & \to & e \\
x (x^{-1} y) & \to & y \\
(x y)^{-1} & \to & y^{-1} x^{-1} \\
\end{eqnarray*} この書き換え規則の集合によって任意の式を標準形に変形することができます。

ここでは「マグマの左単位元・右単位元」と同様の方法で自由「単項・二項マグマ」によって関係式を求めていきます。

書き換え規則 \begin{cases}
\rho_{1} & = & ( & x & \mapsto & e x & \to & x & ) \\
\rho_{2} & = & ( & x & \mapsto & x & \to & e x & ) \\
\rho_{3} & = & ( & x & \mapsto & x^{-1} x & \to & e & ) \\
\rho_{4} & = & ( & x & \mapsto & e & \to & x^{-1} x & ) \\
\rho_{5} & = & ( & x, y, z & \mapsto & (x y) z & \to & x (y z) & ) \\
\rho_{6} & = & ( & x, y, z & \mapsto & x (y z) & \to & (x y) z & ) \\
\end{cases} から \begin{matrix}
e^{-1} x & \xrightarrow{\rho_{2}} & e^{-1} (e x) & \xrightarrow{\rho_{6}} & (e^{-1} e) x & \xrightarrow{\rho_{3}} & e x & \xrightarrow{\rho_{1}} & x \\
\end{matrix} を得ることができます。

\begin{cases}
\rho_{7} & = & ( & x & \mapsto & e^{-1} x & \to & x & ) \\
\rho_{8} & = & ( & x & \mapsto & x & \to & e^{-1} x & ) \\
\end{cases} を付け加えると \begin{matrix}
(e^{-1})^{-1} x & \xrightarrow{\rho_{8}} & (e^{-1})^{-1} (e^{-1} x) & \xrightarrow{\rho_{6}} & ((e^{-1})^{-1} e^{-1}) x & \xrightarrow{\rho_{3}} & e x & \xrightarrow{\rho_{1}} & x \\
\end{matrix} が得られます。

\begin{cases}
\rho_{9} & = & ( & x & \mapsto & (e^{-1})^{-1} x & \to & x & ) \\
\rho_{10} & = & ( & x & \mapsto & x & \to & (e^{-1})^{-1} x & ) \\
\end{cases} を付け加えると \begin{matrix}
e^{-1} & \xrightarrow{\rho_{10}} & (e^{-1})^{-1} e^{-1} & \xrightarrow{\rho_{3}} & e \\
\end{matrix} が得られます。

ここではこれでやめますが、これを続けていくと、上記の書き換え規則の集合が得られます。

文献(本)

[1] 井田哲雄編, 新しいプログラミング・パラダイム, 共立出版, 1989.

新しいプログラミング・パラダイム

[2] 井田哲雄著, 計算モデルの基礎理論, 岩波書店, 1991.

岩波講座 ソフトウェア科学〈〔理論〕12〉計算モデルの基礎理論