単一化 (Unification)

単一化可能性 (unifiability)

[定義] 単一子と単一化可能 (unifier and unifiable) 代入 θ が集合 {E₁, ..., E_k} に対して E₁θ = E₂θ = ... = E_kθ のとき，θ を {E₁, ..., E_k} の単一子 (unifier)という．
集合 {E₁, ..., E_k} に対して単一子が存在するとき， {E₁, ..., E_k} を単一化可能 (unifiable) という．

(例)
集合 {P(x, f(x)), P(a, y)} は単一化可能か? 可能なら単一子を求めよ．

最汎単一子/最大単一化置換 (mgu: most general unifier)

[定義] 最汎単一子集合 {E₁, ..., E_k} の単一子 σ は，その集合の任意の単一子 θ に対して，ある代入 λ によって θ = σ○λ とできるとき，最汎単一子 (mgu: most general unifier)とよばれる．

不一致集合 (disagreement set)

[定義] 不一致集合基本論理式 E_i の集合 M = {E₁, ..., E_n} が与えられたとき，E₁, ..., E_n を構成する記号を左から順に調べていき，一致しない記号があれば，その記号からはじまる項 t_i を各 E_i から抜き出して集めた集合を不一致集合 (disagreement set) という．

(例)
A = {P(x, f(a,b), c), P(x, y, d), P(x, f(a, b), d), P(x, z, e)}の不一致集合は何か?

B = {P(x, g(f(y, z), x), y), P(x, g(a, b), b), P(x, g(g(h(x), a), y), h(x))}の不一致集合は何か?

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

{A₁, A₂, ..., A_n} を調べようとする基本論理式の集合であるとする．

[ステップ0] 空な代入θ₀ (つまり何もしない)から出発する．

[ステップi+1] ステップi(i ≧0) で得られた代入をθ_i とする．

(a) 代入を受けた集合{A₁θ_i, A₂θ _i, ..., A_nθ_i} がすべて同じになるとき，このθ_iを最汎単一子(mgu)という．この場合のA₁θ _i を因子(factor)とよぶ．そしてアルゴリズムは終了する．

(b) そうでなければ，

{A₁θ_i, A₂θ _i, ..., A_nθ_i}

の不一致集合を求めて，これを D_i とする．D_i の中に固体変項 v_i と項 t_i があり，t_i の中に v_i が現れないとすれば(この検査を「出現検査」(occur check)という)，これを t_i/v_iという代入とし，θ _i に加えて

θ_i+1 = θ_i○{t_i/v_i}

を作る．すなわち，θ_i の中に現れる全ての v_i を t_i に置き換え，t_i/v_i を加える．このような v_i，t_i が存在しなければ，これらの基本論理式の間には単一子はないとしてアルゴリズムは終了する．

(例)
W = {P(a, x, f(x)), P(y, g(y), z)} の最汎単一子を求めよ．最汎単一子が存在する場合は，因子も求めよ．

[定理] 単一化アルゴリズムの停止性単一化可能な基本論理式の有限集合 W (≠φ)が与えられたとき，上で示した単一化アルゴリズムはステップi+1(有限回)で停止し，そのとき(a)で停止すれば得られたθ_i は最汎単一子である．

...Return

講義の詳細