unificationを書いてみる(1)
表現を書く
unificationを書きたいのだけど、unificationという理解だと、どうしても手続きになってしまう。
最初は仕方がないと思う。
いろいろやってみたけど、なんか間違っているような気もする・・・
一番簡単な項として、定数aを考えてみる。
項がaだけのclauseの集合Σがあったとする。このときのDの定義はどうなるだろうか。
まず、項というより、表現(Expr)を定義してみる。
Σ0 : (clauseの集合0)
+Expr(a)
定数はaしかないので、aに関する定義を書いていく。
ここで、aが定数であることを書きたければ
+Const(a)
と書く。これはΣの構文的な特徴から(つまりaしかないから)生成される定義。
表現(ここでは項しかないけれど)を表すExprの定義として、Constとの関係を書くと
∀w +Expr(w)∨ -Const(w)
というようなclauseが必要になるだろう。こちらは変数を使っているのでΣ0とは独立に書ける。
Σ_1:
+Const(a)
∀w +Expr(w)∨ -Const(w)
というような具合。
このaという定数は、対象世界の定数であると同時に、記述世界の定数でもある。
Constは何を宣言しているのだろうか?? でも、証明論の話で、項の定義が定数から始まるのだから上のように書きたくなる。
* ちなみに、考えているとき心の中では「対象世界」を「あちら」、「記述世界」を「こちら」と言っているので、ここでもそう書くことにしたい。
さて、unificationを考えるには変数も必要なので、変数を含む式をこう書きたい
+Var(x)
∀w +Expr(w)∨-Var(w)
こう書いておくと、定数も変数も式であるということになる。
Exprを定義しているのが、必要なのかどうかはまだわからない。
これで定義の集合はこうなる。
ちなみに、あちらの変数はこちらの定数になっている。
Σ_2:
+Const(a)
∀w +Expr(w)∨ -Const(w)
+Var(x)
∀w +Expr(w)∨-Var(w)
定数や変数を増やしたければ
+Const(b)
とか
+Var(y)
とかを追加すればよい。
∀wのwはこちらの世界の変数であり、+Var(x)のxはあちらの世界の定数であって、あちらの世界では変数になっている。
ここで、w, a, yに同じ記号を使わないことは大切だ。変数だからといってあちらのxとこちらのxを同じ記号xで書くとおかしなことになる。
また、+Var(x)があるので、∀wを使わずに
+Expr(x)
だけを書くこともできる。このように∀wを使うか、使わずに変数の数だけ定義を書くと言う選択肢はある。もとのclauseの集合に出現する記号は有限個なので、どちらでもかまわないと思うが、書く手間を考えると∀wを使った書き方をしたくなる。
Unifyを書く
表現e1とe2をunifyするということを書く。
unifyするというのは、disagreeな部分を同じとみなす/同じにする操作をすることだと考えられる。
それで述語Dを使い
+D(e1, e2, σ)
で
e1*σ ≡ e2*σ
と考えてみる。
この考え方は今のところ怪しいと思うのだけど、Unificationという手続が頭にあるのでどうしても入出力関係で書こうとしてしまう。
いずれ他の方法も考えたい。
そういえば、Herbrandは、Unificationを推論規則で書いたという噂を読んだことがあるのだけど、いったいどうやって、と思う。
σはe1とe2の不一致部分を表すと考えてもよい。
Dの定義はこうなるだろう。まず・・・
∀e +D(e, e, ∅)
同じ表現eは、相違がないので∅となる。
ここで、+D(e,e,∅) -Expr(e)と書くこともできる。
それは、変数に表現以外の例えば代入にあたる∅のような記号が書かれた場合どうなるのか?
-Expr(∅)
を書くのか? など
この∅はこちらの定数であるが、あちらでも代入を表したいはずなので、あちらの定数にもならなくてはならない。
だんだんややこしくなってくる。
次に、変数xとaの違いを考える。つまり
+D(a,x, (x,a))
とでも書くようなことになる。(x,a)はx=aを意味しているし、x←aという代入を意味するかもしれない。
ここでは(x,a)はタプルであり、一階述語論理の表現ではないので、たとえば関数sを使ってs(x,a)と書くことにする。
最終的にこちらの世界の証明で、関数の合成の形で得られたものを代入とみなせばよい。
+D(a,x, s(x,a))
なにを言っているかというと、こういう定義Σについて、conjectureの否定としてたとえば
∀u -D(x, a, u)
を追加して、反証し、uに代入される式をxとaのmguだと確認する「テスト」みたいなことが考えられる。
そのときのmguは計算されない、式つまり関数合成の形として得られるので、上のs(x,a)のsが関数だといってもtupleを表す記法と考えてよいという意味。
xの1️位置によって+Dの定義はふたつあって
+D(a,x, s(x,a))
+D(x,a, s(x,a))
となる。
もしも定数がa,b,c, 変数がx,y,zなどと増えてきたら、いちいちこの書き方をするのは冗長なので
∀e,w +D(e, w, s(w, e)) -Expr(e) -Var(w)
と書きたいわけだけど、うまくいくだろうか。
ちなみに、このDの定義では、Unifierになるかどうかはわからない。もちろんmguの定義はさらに遠い。
あと、いろいろ思うこと。
★同じと違うの違い
∀e +D(e, e, ∅)
は変数を使ってかけたのに、a,xの場合の定義は変数でなくあちらの定数で書いている。
つまり、同じであることは変数を使って書けるのに、違うことは変数では書けていない。
x ≠ y
を書いてもよいのなら、書けるが、等号は一階述語に含まれないので回避している。
★unifyに失敗するとき
定数aとbのunifyはどう書くのか。
unifyできないのだから-Dとすればよいのだろうか。
∀w -D(a,b,w)
Dがunifier wを定義するとして、unifyできないとき-D(e1,e2,?)となるとするのは見当違いな気がする。
1) unifierを使う何かを書いたとする。それをclause集合 Σ'だとすると、Σ'の中でunifierはDを使って書くことになるだろう。
それは
+X(..,x) -D(...,w) … (x)
のような形になり、+Dが証明できたら、wが定義されその値をXで参照する。
しかし、unifyに失敗したことが-Dになるとしたら、この上の式は+Dがないので、放置される。つまり、(x)からの証明が先に進まないので、この+Dの証明ができないという形でunifyの失敗が捉えられる。
これをよしとすることもできるだろう。証明が存在しないということを失敗したのと同値に考えればよいわけだ。
一方、unifiyに失敗したときにResolutionを実行することを考えると、これはうまく書けない。
今の場合、unifyに失敗したらresolventができず、その世界が存在しないというだけなので、良いように思う。
もしも+Dの場合と-Dの場合で違うふるまいをさせたい場合どうすればいいのか?
長くなったのでこのへんで