論理プログラミング(12) - エレファント・ビジュアライザー調査記録

PLPとPrologの違いについて説明していきます。Prologのプログラムは論理式として見ることもできるのですが、実行する順序が決まっていて、プログラムとして実行することができるようになっています。これを説明するためPrologの単一化(unification)について説明します。

PLPの代入を定義しましたが、これはPrologの代入とは違った定義になっています。そこでまずPrologにおける代入について見てみます。ここではこれを一般代入と呼ぶことにします。 $V$ を変数全体の集合、 $T$ を項全体の集合としたとき、写像 $\sigma : V \rightarrow T$ を拡張した $\sigma : T \rightarrow T$ を一般代入と呼ぶことにします。PLPの代入は変数を含まない項全体の集合を $T'$ としたとき $\sigma : V \rightarrow T'$ として定義していました。

一般代入をさらに述語式全体の集合から述語式全体の集合への写像 $\sigma : Q \rightarrow Q$ に拡張して考えます。2つの述語式 $p$ と $q$ が一致することを $equal(p, q)$ と表すことにします。

Prologの単一化とは、述語式 $p$ と $q$ に対して $equal(\sigma(p), \sigma(q))$ となる一般代入のうち、最も一般的なものを見つける手順のことを表します。最も一般的なものとは、もし $equal(\lambda(p), \lambda(q))$ となる一般代入 $\lambda$ があれば、ある一般代入 $\psi$ が存在して $\lambda = \sigma \circ \psi$ を満たすということを表します。この一般代入を単一化代入と呼びます。

単一化の手順は、まず述語式 $p$ と $q$ の項の個数が異なるときは単一化は失敗となります。項の個数が同じであるときは、項の構造に関して帰納的に実行されます。すべての項に対する単一化が成功したときは単一化は成功、失敗した項があるときは単一化は失敗となります。このときの単一化代入は各項に対する単一化代入の合成となります。述語式を単に項と考えると、述語式の単一化は以下の項の単一化と同じものになります。このように考えると $unify(p, q)$ も述語式と考えることができます。

項 $t$ と $u$ に対する単一化は、項 $t$ が変数であるときは、 $t$ を $u$ に写す写像を単一化代入として単一化は成功します。項 $tu が変数であるときは、[tex: u$ を $t$ に写す写像を単一化代入として単一化は成功します。

次に項 $t$ も $u$ も変数ではない場合を考えます。項 $t$ が定数であるときは $u$ も定数で $t=u$ のとき単一化代入は恒等写像として成功、そうではないときは失敗となります。項 $t$ が関数であるときは $u$ も関数で、両方の関数の項の個数が一致し、各項の単一化が成功したとき、単一化代入は各項の単一化代入の合成写像として成功、そうではないときは失敗となります。

これで単一化の手順は終わりで、単一化が成功したときには単一化代入 $\sigma$ を得ることができました。この単一化代入 $\sigma$ が最も一般的なものになっているというのはどういうことかということを見ていきます。もし $equal(\lambda(p), \lambda(q))$ となる一般代入 $\lambda$ があれば、それは各述語式に現れる変数のうちのいくつかをある項に写す写像となります。単一化代入は必要な最小の個数の変数を写すものであるため、 $\lambda$ は $\sigma$ とある一般代入の合成となります。ただし、変数を変数に写す場合もあり、その方向によって合成にならないとき( $\lambda$ と $\sigma$ が逆になっているとき)もありますが、方向はどちらでも同じことなのでこの場合は無視することにします。

次に PLP の代入について考えると、代入 $\lambda \in \mu(unify(p, q))$ をとると、これは変数を「変数を含まない項」に写すものなので上記の $\lambda$ と同様単一化代入との合成で表すことができます。また、単一化代入があれば、まだ代入が行われていない変数を「変数を含まない項」に写す写像と合成することによって代入 $\lambda \in \mu(unify(p, q))$ を得ることができます。

以上で PLP を無限に実行したものを数学的に定義することがだいたいできました。これを PLP+ と呼ぶことにして、この後は PLP+ について考えていきます。これを使ってサーバーで無限に実行されるプログラムと連携して動いて入出力を行うようなプログラムを考えていきます。無限に実行されているプログラムの入出力は、 $n$ の順で行うようにプログラムを書かなければなりません。関数プログラミングにおいても無限に実行されるプログラムの入出力は、ある決まった順序で書かなければなりません。これは今後考えていこうと思います。