単一化(unification)

単一化の定義

項

1. x∈V ⇒ x∈T(F, V)
2. f∈F, t₁, ..., t_n∈T(F, V) ⇒ f(t₁, ..., t_n)∈T(F, V)

代入

代入の拡張

1. x∈V のとき、xσ~≡xσ
2. x≡f(x₁, ..., x_n) のとき、 f(x₁, ..., x_n)σ~ ≡ f(x₁σ~, ..., x_nσ~)

単一化代入

最も一般的な単一化代入

単一化アルゴリズム

UNIFY(s, t) = 
    begin
        θ := {}
        if s∈V ∨ t∈V then
            begin [変数をx, 他の項をuとする]
                if x≡u then unifiable := True
                else if occur(x, u) then unifiable := False
                else <unifiable, θ> := <True, {u/x}>
            end
        else if s∈K ∨ t∈K then
            begin
                if s≡t then unifiable := True
                else unifiable := False
            end
        else
            begin [t≡f(t1, ..., tnn), s≡g(s11,...,sm)とする]
                if ¬f≡g ∨ m≠n then unifiable := False
                else
                    begin
                        unifiable := True
                        for k = 1,...,n while unifiable
                            begin
                                <unifiable, σ> := UNIFY(tkθ, skθ)
                                if unifiable then θ := θσ
                            end
                    end
            end
        return <unifiable, θ>
    end

• アルゴリズム UNIFY はいかなる項 s, t の入力に対しても停止します。
• 項 s, t が単一化可能であるとき、アルゴリズム UNIFY の結果は True となります。
• アルゴリズム UNIFY の結果が True のとき、得られる代入は mgu となります。

単一化アルゴリズム

項の構成に関する帰納法

1. p(x) (x∈V のとき)
2. p(x₁), …, p(x_n) ⇒ p(f(x₁, …, x_n)) (x∈I, x≡f(x₁, …, x_n) のとき)

不一致集合

1. x∈V, y∈V, x=y のとき、x≡y
2. x₁≡y₁, …, x_n≡y_n のとき、 f(x₁, …, x_n) ≡ f(y₁, …, y_n)

1. x≡f(x₁, …, x_n), y≡f(y₁, …, y_n) のとき、x_i≡y_i ではない i をとって x_i, y_i の不一致集合を x, y の不一致集合とする。
2. それ以外のとき、{x, y} を x, y の不一致集合とする。

Mguの性質

1. x∈V, y∈V, x=y のとき θ=1 は x, y の mgu となります。
   証明: θ は単一化代入になっています。 μ が単一化代入のとき、θμ = μ となります。
2. x∈V, y∈V, x≠y のとき θ={y/x}, θ={x/y} は x, y の mgu となります。
   証明: θ={y/x} のとき: θ は単一化代入になっています。 μ が単一化代入のとき、 x{y/x}μ ≡ yμ ≡ xμ、 v∈D(μ)-{x} のとき v{y/x}μ ≡ vμ となります。 したがって任意の v∈D(μ)∪{x} に対して vθ≡v{y/x}μ≡vμ となるので θμ = μ となります。 θ={x/y} のときも同様です。
3. x∈V, y∈I, {x}∩V(y)=φ のとき θ={y/x} は x, y の mgu となります。
   証明は 2 と同様です。
4. x∈I, y∈I, x=y のとき θ=1 は x, y の mgu となります。
   証明は 1 と同様です。
5. σ₁ が x₁, y₁ の mgu、 σ₂ が x₂σ₁, y₂σ₁ の mgu のとき θ=σ₁σ₂ は <x₁, x₂>, <y₁, y₂> の mgu となります。
   証明: x₁θ≡y₁θ, x₂θ≡y₂θ となります。 代入 μ が x₁μ≡y₁μ, x₂μ≡y₂μ をみたすとき、 μ=σ₁λ₁ をみたす代入 λ₁ が存在します。 x₂σ₁λ₁≡y₂σ₁λ₁ となるので、 λ₁=σ₂λ₂ をみたす代入 λ₂ が存在します。 μ=θλ₂ となります。
6. x∈I, y∈I, x=f(x₁, …, x_n), y=f(y₁, …, y_n), 代入 σ₁=1, …, σ_n+1 が存在して 任意の i = 1, …, n に対して σ_i+1 が x_iσ₁…σ_i, y_iσ₁…σ_i の mgu となるとき、θ=σ_i+1 は x, y の mgu となります。
   証明は 4, 5 からわかります。

1. x∈V, y∈I, x∈V(y) のとき x, y は単一化可能ではありません。
   証明: θ を代入とします。 y≡f(…x…) とすると、yθ≡f(…xθ…) となるので、xθ≡yθ となる代入 θ は存在しません。
2. x∈I, y∈I, x≡f(…), y≡g(…), f≠g のとき x, y は単一化可能ではありません。
   証明: θ を代入とします。 xθ≡f(…), yθ≡g(…) となるので、このような代入 θ は存在しません。

単一化アルゴリズム(1)

1. xθ_n≡yθ_n のときは成功。
2. xθ_n≡yθ_n ではなく xθ_n, yθ_n の不一致集合 {u, v} が v∈V, u∈V のとき θ_n+1=θ_n{u/v} とする。
3. xθ_n≡yθ_n ではなく xθ_n, yθ_n の不一致集合 {u, v} が v∈V, u∈I で v が V(u) に含まれないとき θ_n+1=θ_n{u/v} とする。
4. それ以外のときは失敗。

単一化アルゴリズム(2)

1. x∈V, y∈V, x=y のとき成功。(θ=1)
2. x∈V, y∈V, x≠y のとき成功。(θ={y/x} または θ={x/y})
3. x∈V, y∈I, {x}∩V(y)=φ のとき成功。(θ={y/x})
4. x∈I, y∈V, {y}∩V(x)=φ のとき成功。(θ={x/y})
5. x∈I, y∈I, x=f(x₁, …, x_n), y=f(y₁, …, y_n) のとき σ₁=1 として i = 1, …, n に対して unify2(x_iσ₁…σ_i, y_iσ₁…σ_i, σ_i+1) を実行してすべて成功のとき成功。(θ=σ_n+1)
6. それ以外のときは失敗。

単一化アルゴリズム(1), (2)の関係

単一化アルゴリズムの記述

1. nil∈L
2. cons: E×L→L
3. =: E×E→boolean

1. equal(nil, nil)
2. equal(x, y) ⇒ equal(cons(z, x), cons(z, y))
3. それ以外は equal(x, y) にはならない。

1. P ∧ Q となっているものは、P を実行した結果が true であれば Q を実行してその結果を P ∧ Q の結果とする。 P を実行した結果が false であれば結果は false とする。
2. P ∨ Q となっているものは、P を実行した結果が false であれば Q を実行してその結果を P ∧ Q の結果とする。 P を実行した結果が true であれば結果は true とする。

これと同じように、単一化アルゴリズムを記述してみます。 S は記号の集合、 T は項の集合、 L は項のリストの集合、 Σ は代入の集合という意味です。 各集合を構成する写像と、集合 S の中の関係 = を以下のように定義します。

1. var: S→T
2. func: S×L→T
3. nil∈L
4. cons: T×L→L
5. id∈Σ
6. map: S×T→Σ
7. comp: Σ×Σ→Σ
8. =: S×S→boolean

1. subst: S×Σ×T→boolean
2. op: T×Σ×T→boolean
3. notoccur: S×T→boolean
4. s_unify: T×T×Σ→boolean
5. unify3: T×T×Σ→boolean
6. =: Σ×Σ→boolean (この定義は省略)

1. x=var(s) ∧ y=var(s) ∧ θ=id ⇒ unify3(x, y, θ)
2. x=var(u) ∧ y=var(v) ∧ (θ=map(u, y) ∨ θ=map(v, x)) ⇒ unify3(x, y, θ)
3. x=var(u) ∧ y=func(v, yl) ∧ notoccur(u, y) ∧ θ=map(u, y) ⇒ unify3(x, y, θ)
4. x=func(u, xl) ∧ y=var(v) ∧ notoccur(v, x) ∧ θ=map(v, x) ⇒ unify3(x, y, θ)
5. x=nil ∧ y=nil ∧ θ=id ⇒ unify3(x, y, θ)
6. x=cons(x1, x2) ∧ y=cons(y1, y2) ∧ unify3(x1, y1, λ) ∧ op(x2, λ, xs) ∧ op(y2, λ, ys) ∧ unify3(xs, ys, μ) ∧ θ=comp(λ, μ) ⇒ unify3(x, y, θ)
7. それ以外は unify3(x, y, θ) にはならない。

参考文献

1. 井田哲雄: 計算モデルの基礎理論, 岩波書店, 1991.
2. 小野寛晰: 情報科学における論理, 日本評論社, 1994.
3. 萩谷昌己: ソフトウェア科学のための論理学, 岩波書店, 1994.
4. 森下真一: 知識と推論, 共立出版, 1994.