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

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

中間報告(8)

このブログでは、「無限の項を持つ多項式のようなもの」(「無限論理多項式」と呼ぶことにします)を使って、サーバーで無限に実行されるプログラムとブラウザーで実行されるプログラムの組み合わせを表そうとしています。この「無限論理多項式」の定義についてはまだできていませんが、これを論理プログラミングの考え方で(たとえば無限個のPrologプログラムによって構成されるものとして)定義することを目標としています。

「エレファントな群とリー代数」の記事では、項書き換えのようなシステムと「無限論理多項式」の関連について調べています。

絶対数学原論』で扱われている絶対代数は、可換モノイドを多項式のように扱うもののようです。これと「無限論理多項式」の関連についても調べてみたいと思います。

関数プログラミングの機能によって無限に動作するプログラムを表したものと「無限論理多項式」の関連についても調べてみたいと思います。

その他の記事で、可換モノイドや数学的帰納法の記述方法について調べているものがありますが、これによって「無限論理多項式」を記述することができるのではないかと考えています。

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

となります。

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

[証明終わり]