一般マグマの多項式の単一化アルゴリズム(3)
前回の議論(「wikipedia:ユニフィケーション」の「一階の項」を参照)を『計算論理に基づく推論ソフトウェア論』の議論のように2段階に分けます。なお、前回の記事でも単一化アルゴリズムの中で項を変化させる場合と変化させない場合が混在していたので、この点も直します。
とします。一般マグマの多項式
に
(
を代入したものを
とします。
を
という置換とすると
となります(
は
を拡張した一般マグマの準同型)。これを
と書くことにします。
としたとき
と書くことにします。
という置換を
とします。
、
に対して
を
、
という置換とします。
のとき
を
と書くことにします。
置換全体の集合を とおきます。
に対して
を
と書くことにします。
に対して
となる一般マグマの準同型
が存在するとき
と書くことにします。
は前順序となります。
に対して、置換
が存在して
となるとき、
と
は単一化可能といって、
を
と
の単一化子と呼びます。
- (MGU1)
が
と
の単一化子で、
- (MGU2)
が
と
の単一化子ならば
となるとき を
と
の最汎単一化子と呼びます。
とおきます。
の
という形の元の全体を
とします。すると、
となります。
とします。
を
の部分項として現れる
の元全体の集合とします。
、
(
は失敗を表す)を \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*} と定義します( は左から順に適用)。こうすると
は帰納的に定義することができます。
、
(
は失敗を表す)を \begin{cases}
(U 1) & σ = d(α, β) \in Σ & & のとき & σ \succ u(α[σ], β[σ]) \\
(U 2) & d(α, β) = ⊥, & α = β & のとき & 1 \\
(U 3) & d(α, β) = ⊥, & α \ne β & のとき & ⊥ \\
\end{cases} と定義します( とします)。
は有限なのでこのように帰納的に定義することができます。
このとき \begin{cases}
u(α, β) \in Σ & のとき & u(α, β) \ は \ α, β \ の最汎単一化子 \\
u(α, β) = ⊥ & のとき & α, β \ は単一化不可能 \\
\end{cases} が成り立つことを以下で示します。
(UA1)
ならば
は
と
の単一化子
[証明] という列を \begin{cases}
(U1') & θ_i = d(α[σ_i], β[σ_i]) \in Σ & のとき & σ_{i+1} = σ_i \succ θ_i \\
(U 2'), (U3') & d(α[σ_i], β[σ_i]) = ⊥ & のとき & σ_i \ で列は終了 \\
\end{cases} とおくと の元の個数以下の
で列は終了します。よってこの列を帰納的に定義することができます。
となります。
- (U2')
のとき
となります。
- (U3')
のとき
となります。
よって ならば
が成り立ちます。[証明終わり]
(UA2)
かつ
が
と
の単一化子ならば
かつ 
[証明] かつ
が
と
の単一化子ならば
は \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)は、、
とすると、
は
となる最初の
となります。
(D4)、(D5)、(D7)のとき とすると \begin{cases}
(d(α, β) \succ τ)(x) = τ^*(t) = τ(x) \\
(d(α, β) \succ τ)(y) = τ(y) & (y \in X \setminus {x}) \\
\end{cases} より 、
となります。
(D9)のとき任意の に対して
は
と
の単一化子となります。
よりどれかの
の組は
となります。この最初の組を
とおきます。
すべての に対する
と
に対して主張が成り立っていると仮定すると、
となります。よって
と
に対しても主張が成り立ちます。[証明終わり]
(UA3)
が
と
の単一化子ならば
かつ 
[証明] 上で定義した という列を使って、
かつ
であることを帰納的に示します。
かつ
は成り立っています。
とし、
かつ
であると仮定します。
ならば主張は成り立っています。
とします。
とすると
となり、
は
と
の単一化子となります。
(UA2)より かつ
となります。
となって
のときも成り立ちます。
よって帰納法により主張が成り立ちます。[証明終わり]
(UA4)
ならば
は
と
の最汎単一化子
[証明]
- (MGU1): (UA1)より
は
と
の単一化子となります。
- (MGU2): (UA3)より
が
と
の単一化子ならば
となります。
[証明終わり]