Unificationアルゴリズムにも迷う

Unificationは2つの式(論理式や項)から、代入mguを計算するアルゴリズムである。

以下に示す例では、x, y, zは変数、a, b, cは定数、f, g, kは関数記号とする。

2つの式とmguの例)
t1,t2 を式として、<t1:t2>でunificationした結果のmguを表す。

　(1) <a : b> : unifyできない
　(2) <f(a) : g(b,c)> : unifyできない
　(3) <x:b> = {x←b}
　(4) <f(x, b) : f(a, y)> = {x←a, y←b}
　(5) <f(a, x) : f(y, g(y))> = {y←a, x←g(a)}
　(6) <f(x, x) : f(y, g(y))> : unifyできない

[An unificationアルゴリズムの概要]

準備
Unificationアルゴリズムのひとつを示す。

式Eのこの木表現をΞ(E)と書く。
式E1とE2が与えられたとき、Unificationアルゴリズムは、Ξ(E1)とΞ(E2)を並べ、左端からひとつずつ式を比較し、木をたどる。そして、異なる式t1, t2をみつけたとき、その場所を相違点Δと呼ぶことにする。
木をたどって同じだった部分と、相違のある箇所を次のような絵で書いてみる。

　　　　　　　Δ
　　|---  同一 →↓
E1  —----------→t1 …
E2  —----------→t2 …

t1,t2は式なので、次の3つの場合がある。ただし、記号が変数か定数かはなんらかの方法で決定されているとする。

相違点Δから代入の素を作るのだが、作られた代入はδで表すことにする。
また、ΔはE1とE2を区別する必要がないので、左が変数になるように順番を入れ替える。

　(1) 変数 : 定数 ⇒  {変数←定数}
　(2) 変数 : 変数 ⇒  {変数←変数}
　(3) 変数 : 式     ⇒  {変数←式}
　(4) 式:式 または 定数:定数 ⇒ Unificationは失敗する

(1)や(3)の場合は、その変数への定数の代入をδとする。
(2)の場合、どちらの変数を左にしてもかまわない。E1側を左にするなど適当に決める。
(4)で、定数:定数の場合は、異なる定数であり、これはunifyできないのでUnificationに失敗する。式:式の場合は f(...):g(...)でありunificationは失敗する。両方の関数記号が同じ f ならば、この相違点は存在せず、その引数部分で相違点を探すことになるので、(1)から(3)に帰着する。

Unificationアルゴリズムの概要

　1. 式E1とE2が与えられる。mgu μの初期値として∅を設定する。
　2. Ξ(E1)とΞ(E2)の 相違点Δを求める。相違点が1つもなければ、E1≡E2ということなので、この時点のμがmguである。
　3. Δの左の変数が右の式に出現するならば、unificationは失敗とする。(*1)
　4. μにΔを追加する(*2)。
　5. E1をE1・μ、E2をE2・μとし2に戻る。
　
(*1) この条件がないと、Unificationアルゴリズムは停止せず、μが確定しない。また、右と左が同じ変数の場合は相違点にならないので、{x←x}のような代入は作られない。

(*2) 「代入μにΔを追加する」は、次のように行う。
　(a) 状況: μの左の変数はすべてE1とE2に代入され、E1からもE2からも消えている。だから、相違点Δの左(変数)はμのどの左(変数)とも異なる変数である。このことから、最終的なμの左はすべて異なることが言える。

　(b) 操作: μ={v1←t1, v2←t2, …, vm←tm}としたとき、μを次のμ'で置き換える。
　　 μ' = {v1←t1・Δ, v2←t2・Δ, …, vm←tm・Δ} ∪  Δ
　　つまり、代入μの右式のすべてにΔを適用し、集合としてΔを追加する。
　　この操作は「μにΔをかける」と表現することにする。

アルゴリズムおわり
　
この(*1)と(*2)から、「代入に迷う」に書いたmguの次の性質が成り立つ。
　(「代入に迷う」の(*1)などを(代入*1)のように書く)

　(代入*1)  μの要素の左はすべて異なる。(*2)より。
　(代入*2) 左は右に含まれない。(*1)より。

このように、unificationアルゴリズムで作成したmgu μは、左の変数がどの右の式にも含まれないので、

　(代入*3) 代入の要素の書かれる順番に関係なく同じ代入を表す。

が成り立つ。

　(*2)の(b)のように代入μに代入Δを適用することによって、代入の条件(2')も排除している。
　　(代入2')  左が右の表現のどれかに含まれない。

unificationの計算例)
最初にあげた例をアルゴリズムを使ってmguを計算する過程を示す。
　(1) <a : b> : unifyできない
        E1: a
　　 E2: b
      Δ = (a,b)なので定数:定数だからunificationできない。

　(2) <f(a) : g(b,c)> : unifyできない
　　　E1: f(a)
　　　E2: g(b,c)
　　Δ=(f(a), g(b,c))なので式:式だから、unificationできない。

　(3) <x:b> = {x←b}
　　　E1: x
　　　E2: b
　　xは変数で、Δ=(x,b)なので、δ={x←b}が得られ、これがμ、mguとなる。

　(4) <f(x, b) : f(a, y)> = {x←a, y←b}
　　　E1: f(x, b)
　　　E2: f(a, y)
　　x,yは変数で、第一の相違点Δは(x, a)である。これからδ={x←a}を作り、
　　μ={x←a}となって、E1, E2をμで更新し、2に進む。
　　　E!: f(a, b)
　　　E2: f(a, y)
　　第二の相違点Δは(y,b)である。これからδ={y←b)を作り、μの右にかける。
　　μ={x←a, y←b}
　　となり、これをE1,E2に適用すると、同一の式になるので
　　μ={x←a, y←b}がmguとなる。

　(5) <f(a, x) : f(y, g(y))> = {y←a, x←g(a)}
　　　E!: f(a, x)
　　　E2: f(y, g(y))
　　第一の相違点Δは(y, a)である。これからδ={y←a}を作り、
　　μ={y←a}となってE1とE2を更新する。
　　　E1: f(a, x)
　　　E2: f(a, g(a))
　　このようにg(x)がg(a)に変わる。
　　第二の相違点Δは(x, g(a))である。これからδ={x←g(a)}を作り、μの右にかけて
　　μ={y←a, x←g(a)}となる。これをE1,E2に適用すると、同一の式になるので
　　このμがmguである。

　(6) <f(x, x) : f(y, g(y))> : unifyできない
　　　E1: f(x, x)
　　　E2: f(y, g(y))
　　第一の相違点Δは(x,y)である。ここではδ={y←x}としよう。
　　これからμ={y←x}となり、E1,E2にかける。
　　　E1: f(x, x)
　　　E2: f(x, g(x))
　　第二の相違点Δは(x, g(x))となる。このΔは左のxが右のg(x)に出現しているのでunificationに失敗する。

代入*2'が起きない例
　このunificationアルゴリズムでは{y←a, x←f(y)}のような形のmguは作られない。その例として適切かどうかあやしいが、こういうものを考えてみた。

　 <k(x, g(x)):k(a, y)> = {x←a, y←g(a)}=σ1

である。これは、xにaを代入した後の相違点を求めているのでΔが(y, g(a))となる。
しかし、その引数の順序を逆にした次の例では、y←g(x)が先に求められているので、第二の相違点Δから{x←a}を作っても、μの右にこれを適用しなければ、{y←g(x), x←a}になってしまう。このunificationアルゴリズムでは、μの右に{x←a}を適用するので

　<k(g(x), x):k(y, a)> = {y←g(a), x←a} = σ2

　と、σ1と同じ代入になる。

* 他のUnificationアルゴリズム
E1とE2が与えられたとき、一度にすべての相違点を求めることもできる。
つまり、Δ(E!, E2) = {Δ1, Δ2, …, Δm}というように相違点の集合を求めることもできる。Unificationアルゴリズム中に、これらの相違点のインスタンスが出現するが、これら以外の相違点は出現しない。

たとえば、上の例(4)では、Δ(f(x, b) : f(a, y)) ={(x,a), (y, b)}のようになる。このΔ集合の要素を代入に変換し代入の合成ができればうまくいくかもしれない。

　　{x←a}*{y←b} = {x←a, y←b}

のようにできる場合もある。しかし、これまでの例にもあるように、
　Δ(f(y, a), f(g(x), x))を考えると、{(y, g(x)), (x, a)}となり、単純に合成することはできなさそうだ。つまり、xが(y, g(x))の右に含まれているので、順番によっては残ってしまう。
　アルゴリズムとして、各ΔiについてΔi左がΔj右に含まれている関係に着目し、その連鎖が輪になったらuificationできないと判定し、輪がなくツリーを作れたら、リーフから順番に右に適用していくとか、あるいはすべてのδiを別のΔjの右に適用するとか、そのような方法で解決できるかもしれない。しかし、かなり手間のかかる処理であり、ここで紹介したアルゴリズムのほうが効率はよさそうだ。

　このUnificationアルゴリズムは説明用のものなので、改良の余地はたくさんある。
たとえば、すでに同一になった左側について、毎回比較することは無駄なのでやらなくてもよい。

[mostについて]
　さて、most general unifierがなぜmostなのかという説明を前にしたような気がする。
つまり、E1とE2の任意のunifier σについて、μ = <E1:E2>のとき、代入τが存在して
   　E1・σ ≡(E1・μ)・τ
とできるからμはmostだという説明だが、これはこのアルゴリズムについて本当に成り立つのだろうか。
アルゴリズムを解析して、これが言えた時はじめて、このアルゴリズムがmguを作るUnificationアルゴリズムだと言えると思うけどわからない。
まだまだ謎=迷いは続く。

メモ
ある本にUnificationはRobinsonが作ったと書かれていた。またどこかで、Herbrandが考えたのだという話もよんだように思う。こちらでは、HerbrandはUnificationをGentzen流の推論規則で書いていて、それは彼の学位論文にあるというのだ。彼の学位論文はフランス語で書かれているので私には解読できないが、英訳が収められている本もある。英語も苦手なのでながめるだけなのだが、そんなものが書かれている気配を感じない。
どうなっているのだろうか。