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