代入に迷う

Resolutionでは、Unificationによってmguという代入を作るが、Resolutionで用いる代入はすべてこのmguである。2つのclausesが共通の変数を持たないように、変数名を付け替える操作で代入を使う場合は、別の方法で作ることになるが、以下の話ではそれは気にしなくていい。

まず、表現(式)に代入を適用する操作を次のように定義しておく。

代入表現
代入は、siが記号(定数や変数)で、eiは表現(式)であるとして、
　　{s1←e1, s2←e2, …}のように(ここだけの記法)書く。

というところで、Eを表現としてそれに代入σを適用する代入操作(E・σと書く)をこう定義する。

　1) {s←e}のように1つしか要素がない場合は、Eの記号をすべてたどり、sと同じ記号があったらそれをeで置き換える。

　2) {s1←e1, s2←e2, sm←em}のように複数の要素がある場合、これを{ς1, ς2, …, ςm}と書いた時、
　　E・σ = (…((E・ς1)・ς2)・…・ςm) と定義する

これは、各ςiについて、Eの記号を順番に調べていくので性能の点ではあやしいが、これが最も素朴なE・σの定義になるだろう。

代入の性質
Unificationで作られる代入がもつ性質には、次の二つがあるが、このような制限のない代入というものも考えられる。

　Unification生成代入の性質
　代入mguをμとすると
　(1)  μの要素の左はすべて異なる。
　　次の(a)(b)(c)はすべてNG

　　{x←a, x←b}  … (a)
　　{x←f(y), x←f(a)}  … (b)
　　{x←f(y), x←f(a), y←a}  … ©

　これは、左端のxへの代入だけが効果を持つので、もしも代入に同値関係があるならば
　　σ = {x←a, x←b} = {x←a} であり
　　σ = {x←f(y), x←f(a)} = {x←f(x)}である。
　これは
　　{x←f(a)}に等しくなってほしいような気もするが、代入操作の定義からはこうなるしかないだろう。

　(2) 左が右に含まれない。
　　次の(d)(e)はすべてNG
　　{x←f(x,a)}  … (d)
　　{x←x}   … (e)

 E=k(x)に対して(d)を適用することを考えるとこうなるだろう。
　E・(d) ≡ f(x,a)
　E・(d)・(d) = f(f(x,a),a)
　...

 この代入は記号操作として何も矛盾していないので、一般的に代入操作としては妥当であるが(*1)、Unificationアルゴリズムではこのような代入は作らない。
(*1) 代入がどうなっていなくてはならないのかが明確ではないので、この判断基準の根拠は、余計な条件を排除するとしたらこうかなという程度の意味。

(e)の{x←x}は、どのような表現も変化させないので、空代入 {}と同値である。変数としてyやzをとれば、{y←y}や{z←z}とも同値になる。
そこで、代入が機能的に同値なら表現も唯一にしたい人には、このような代入は許しがたいかもしれず、(e)を除外するようにしたいだろう。

　(2') 左が右の表現のどれかに含まれない。
　次の(f)はNG
　{x←f(y,z), y←g(x), z←a}  … (g)

　これは、(2)を一般的にしたものになっている。unificationのアルゴリズムによっては、(2)は起きても(2')は起きないという可能性はある。

以上に加えて、Unificationとは関係なく、代入を集合の{}記法で書くのであれば成り立っていてほしい性質がある。

　(3) 代入の要素の書かれる順番に関係なく同じ代入を表す。
　集合は要素の順番を無視するということなので、こうなっているべきだと思われる。

　　たとえば、(f)(g)が次のような代入である場合
　　σ1 = {x←a, y←f(x)}  … (f)
　　σ2 = {y←f(x), x←a}  … (g)

(f)と(g)は要素の順番が逆である。
そこで、式E=k(x, y)に対してそれぞれを適用すると

　　E・σ1 ≡ k(a, f(x)}
　　E・σ2 ≡ k(a, f(a)}

となる。
これは、代入を適用するアルゴリズムの定義が適切ではないのだという立場もあるかもしれないし、代入表現としては{x←a, y←f(a)}でなくてはならないとする立場もあるだろう。つまり、(2)の条件に帰着する。この例のように(2)の性質を満たさないときにだけ、この問題がおきるならば、これは(2)を許すかどうかに帰着される。

代入の同値

あと気になるのは、2つの代入が等しいとはどういう定義になるだろうか。

漠然と考えると・・・

定義1

　σ = σ' ⇔  ∀E(E・σ ≡ E・σ')

のように定義できそうだが、なんともよくわからない。

unificationが特定の表現について同一化するという目的を持っているので、ここまで強い制約は必要ないのかもしれない。代入の同値関係を何に使いたいかによって話が変わってくるのだろう。