エレファントな群とリー代数(9) - エレファント・ビジュアライザー調査記録

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

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

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

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

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

置換 $\sigma, \tau: X \to M[X]$ に対して、 $\varphi \circ \sigma = \tau$ を満たす一般マグマの準同型 $\varphi: M[X] \to M[X]$ が存在するとき $\sigma \le \tau$ と書くことにします。

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

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

$M$ の演算を $f_1, f_2, \cdots, f_m$ とします。演算の結果を $f_i(t_1, t_2, \cdots, t_n)$ のように写像の形で書くことにします。 $M[X]$ の $f_i(t_1, t_2, \cdots, t_n)$ という形の元の全体を $M[X]_{f_i}$ とすると、 $M[X] = M \cup X \cup M[X]_{f_1} \cup M[X]_{f_2} \cup \cdots \cup M[X]_{f_m}$ となります。 $M[X]_{f_0} = M$ 、 $M[X]_+ = M[X]_{f_0} \cup M[X]_{f_1} \cup M[X]_{f_2} \cup \cdots \cup M[X]_{f_m}$ とします。

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

$v(\alpha)$ を $\alpha$ の部分項として現れる $X$ の元全体の集合とします。 $u: M[X] \times M[X] \times \Sigma \to \Sigma \sqcup \{F\}$ ( $F$ は失敗を表す)、 $u(\alpha, \beta, \sigma)$ を \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*} と定義します。

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