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

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

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

[証明終わり]