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

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

エレファントな群とリー代数(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} が成り立ちます。この結果は項の順序に依存しません。