単一化アルゴリズム(2) - エレファント・ビジュアライザー調査記録

『数理論理学: 合理的エ-ジェントへの応用に向けて』のわからないところを説明します。まずこの本の定義を引用していきます。用語と記法を一部書き直しています。

定義4.6 (単一化，単一化代入)

$2$ 以上の整数 $n$ に対し、各 $\{L_1, L_2, \cdots, L_n\}$ を項の集合とする。この集合のすべての要素に対し、 $L_1θ=L_2θ=\cdots＝L_nθ$ となるような代入 $θ$ が存在するとき、この $θ$ を集合 $\{L_1,L_2, \cdots, ，L_n\}$ の単一化代入(unifier)と呼ぶ。また、このような単一化代入 $θ$ を求め、 $L_1, L_2, \cdots, L_n$ をそれぞれ $L_1θ, L_2θ, \cdots, L_nθ$ に置き換える操作を単一化(unification)と呼ぶ。

定義 4.7 (不一致集合)

項の集合 $\{L_1, L_2, \cdots, L_n\}$ を $S$ とする。各 $L_i$ に現れる記号(定数記号、変数、関数記号)を左から順にたどり共通しない記号が見つかった場合、それぞれの記号の位置から始まる項の集合を $S$ の不一致集合(disagreement set)と呼ぶ。

定義 4.8 (代入の合成 $\circ$ )

$θ_1, θ_2, σ$ を代入とする。任意の項 $F$ に対し $(Fθ_2)σ＝Fθ_1$ となるような $θ_1$ を $θ_2$ と $σ$ の合成と呼び、合成された代入を $σ \circ θ_2$ と表記する。

定義 4.9 (単一化アルゴリズム(unification algorithm))

$S$ を $1$ 個以上の原子論理式の集合とする。また、 $k＝0,S_k=S, θ_k＝\epsilon$ とする。以下に示す手順1.2.3.を順に実行し正常終了したときに求まる代入 $θ_k$ が、 $S$ の単一化代入である。

1. $S_k$ の要素数が $1$ ならば正常終了とし、以降の操作は行わない。

2. $S_k$ の不一致集合を $D_k$ とする。 $D_k$ の要素として変数が存在し、かつその変数を含まないような項が $D_k$ の要素として存在する場合、その変数と項をそれぞれ $x_k, t_k$ とする。そうでない場合は $S$ は単一化不可能としてこの手順を終了し、以降の操作は行わない。

3. $θ_{k+1}=θ_k \circ (x_k \mapsto t_k), S_{k+1}=S_k(x_k \mapsto t_k)$ とし、 $k$ を $1$ 増やして1. に戻る。

定義 4.10 (代入間の等価性)

$θ_1,θ_2$ を代入とする。任意の項または論理式 $F$ に対し $Fθ_1 = Fθ_2$ となるとき、 $θ_1=θ_2$ とする。

定義4.11 (最汎単一化代入 mgu)

$2$ 以上の要素を持つ原子論理式の集合を $S$ とし、 $θ_1$ と $θ_2$ を $S$ の単一化代入とする。ある代入 $σ$ が存在して $θ_1=σ \circ θ_2$ となるとき、 $θ_2$ は $θ_1$ に対し、より一般的であるという。
$S$ の単一化代入 $θ_g$ が、 $S$ の任意の単一化代入 $θ$ に対し、より一般的であるとき、 $θ_g$ を $S$ の最汎単一化代入(most general unifier)またはmguと呼ぶ。

定理 4.1 (単一化定理)

$S$ を項の空でない有限集合とする。このとき $S$ が単一化可能であれば、定義 4.9 に示した操作は手順 1. で停止する。 $S_n$ で停止したとすると(変数の個数は有限なのである $n$ で停止する)、代入 $θ_n$ は $S$ の mgu である。

この定理の証明は書かれていないので、『計算論理に基づく推論ソフトウェア論』の単一化アルゴリズムの定義と証明について見ていきます。『計算論理に基づく推論ソフトウェア論』では代入は写像として扱われているようです。

アルゴリズム 3.1

入力：項の空でない集合 $S$
出力：mgu か“単一化不能”性の表示 $\bot$
方法：次の帰納的な関数を実行し、出力 $u(S)$ を得る。ただし、任意の代入 $\varphi$ に対して、 $\bot \circ \varphi ＝ \bot$ とする。

$u(S) \Leftarrow$	$\mathop{\mathbf{if}}$		$S$ が単一の項からなる
	$\mathop{\mathbf{then}}$		$\epsilon$
	$\mathop{\mathbf{else}}$	$\mathop{\mathbf{if}}$	$D(S)$ が変数 $x$ と $x$ が出現しない項 $t$ を含む
		$\mathop{\mathbf{then}}$	$u(S(x \mapsto t)) \circ (x \mapsto t)$
		$\mathop{\mathbf{else}}$	$\bot$

( $D(S)$ は不一致集合、 $x$ と $t$ は任意のものとします)

定理 3.3

項の空でない集合 $S$ が与えられたとき，アルゴリズム3.1によって、 $S$ 　が単一化可能なときは一つの mgu が得られ、 $S$ が単一化不能なときは"単一化不能”の表示を得る。

[証明] アルゴリズム 3.1 を $u: \mathfrak{F}(T) \to \Sigma \cup \{\bot\}$ とおきます。 $\mathfrak{F}(T)$ は $T$ の有限部分集合の全体、 $\Sigma$ は代入の全体、 $\bot$ は単一化不可能であることを表します。

$S$ に含まれる変数の個数は有限なので、アルゴリズム 3.1 で $u$ の中から $u$ が呼び出される回数 $n$ は有限となります。 $n$ に関する帰納法により示します。

(i) $n=0$ のとき、 $S$ が単一の要素からなるか、不一致を解消できない(“単一化不能”の表示を得る)。前者の場合、定義 4.9 により $\epsilon$ が得られる。 $S$ の任意の単一化代入 $θ$ に対して、(補題 3.3) により $θ=θ \circ \epsilon$ であるので、一つの mgu $\epsilon$ が得られている。

(ii) $n=k$ のとき定理が正しいと仮定する。 $S$ の不一致集合が変数 $x$ と $x$ が現れない頃 $t$ を含み、代入 $(x \mapsto t)$ を適用し、 $S(x \mapsto t)$ への代入適用回数が $k$ であるとする。仮定から、 $u(S(x \mapsto t))$ は一つの mgu $φ$ か“単一化不能”の表示( $\bot$ )を与える。

後者の場合、 $u(S)=\bot$ である。

前者の場合、 $S$ の任意の単一化代入 $θ$ は、 $\{x, t\}$ を単一化できるので、 $θ = θ' \circ (x \mapsto t)$ と書け、 $θ'$ は $S(x \mapsto t)$ の単一化代入である。 $φ = u(S(x \mapsto t))$ に対して、ある代入 $λ$ があって $θ' = λ \circ φ$ である。よって、 $θ = θ' \circ (x \mapsto t) = λ \circ u(S(x \mapsto t)) \circ (x \mapsto t) = λ \circ u(S)$ である。すなわち、 $u(S)$ は一つの mgu である。[証明終わり]

この証明は「 $S$ の任意の単一化代入 $θ$ は、 $\{x, t\}$ を単一化できる」こと、「 $θ = θ' \circ (x \mapsto t)$ と書ける」ことの説明が書かれていないのでわかりにくいです。代入の順序を入れ替える方法が何かあるかと思いましたがとくに何も見つかりませんでした。エレファントな群とリー代数(11) - エレファント・ビジュアライザー調査記録ではこれを書き直しています。