論理プログラミング(9) - エレファント・コンピューティング調査報告

PLP のプログラムが成功するとき、論理式として見ると証明図を書くことができることを帰納法で証明していきます。

$\displaystyle \mu(d^n(r) \downarrow) \ne \phi$

となる $n$ に関する帰納法で証明します。 $n=1$ から始めます。PLP のプログラムは1個の述語式から始めると定義したので、 $n=0$ のときは書くことができません。もし書けるとしても何も書かないことになります。 $n=0$ のときの証明図は何も書いていないことになるので何も書かないという証明図が書けたということになりわかりにくいです。すなわち本当は $n=0$ のときにも成り立つのですが、書くのが難しいので省略することにします。

$n=1$ のときは

$\displaystyle \mu(d(r) \downarrow) \ne \phi$

となります。代入 $\sigma \in \mu(d(r) \downarrow)$ をとると $\sigma(d(r))$ は正規化された論理式なので $\sigma(d(r))$ の中にある連言節 $u_1 \land u_2 \land \cdots \land u_m$ が存在して、すべての $u_i$ が $unify(x, y)$ の形の式(これをunify式と呼ぶことにします)となります(unify式は今のところ述語式ではありませんがここの議論ではunify式のまま残しておくとします)。 $n$ が $1$ 増えるごとにunify式は1個追加されるので $n=1$ だからunify式は1個(すなわち $m=1$ )となります。

PLP のプログラムを

$\displaystyle \exists t_1 \exists t_2 \cdots \exists t_\nu (a_1 \land a_2, \land \cdots \land a_k \rightarrow r)$

という論理式(各 $a_i$ は

$\displaystyle \forall v_{i1} \forall v_{i2} \cdots \forall v_{ih_i} \exists c_{i1} \exists c_{i2} \cdots \exists c_{ig_i} (p_{i1} \land p_{i2} \land \cdots \land p_{il_i} \rightarrow q_i)$

という形の論理式)と考えます。

まず上記の

$\displaystyle \vdash \exists t_1 \exists t_2 \cdots \exists t_\nu (a_1 \land a_2, \land \cdots \land a_k \rightarrow r)$

を証明するには、

$\displaystyle \vdash (a'_1 \land a'_2, \land \cdots \land a'_k \rightarrow r')$

を証明する証明図を書くことができればよいということがわかります(「シークエント計算」の「 $\exists$ 右」)。ここで $a'_1 \land a'_2, \land \cdots \land a'_k \rightarrow r'$ は、新しい項 $t'_1, t'_2, \cdots t'_\nu$ を追加して $a_1 \land a_2, \land \cdots \land a_k \rightarrow r$ に現れる $t_1, t_2, \cdots t_\nu$ を $t'_1, t'_2, \cdots t'_\nu$ にそれぞれ置き換えたものとなります。

次に $\vdash a'_1 \land a'_2, \land \cdots \land a'_k \rightarrow r'$ を証明するには、 $a'_1 \land a'_2, \land \cdots \land a'_k \vdash r'$ を証明すればよいということになります(「 $\rightarrow$ 右」)。

$a'_1 \land a'_2, \land \cdots \land a'_k \vdash r'$ を証明するには $a'_i \vdash r'$ をどれかの $i$ に対して証明すればよいということになります(「 $\land$ 左」の繰り返し)。

$\displaystyle \forall v_{i1} \forall v_{i2} \cdots \forall v_{ih_i} \exists c_{i1} \exists c_{i2} \cdots \exists c_{ig_i} (p'_{i1} \land p'_{i2} \land \cdots \land p'_{il_i} \rightarrow q'_i) \vdash r'$

を証明するには、新しい変数 $v'_{i1} , v'_{i2}, \cdots , v'_{ih_i}$ を追加して $v_{i1} , v_{i2}, \cdots , v_{ih_i}$ を $v'_{i1} , v'_{i2}, \cdots , v'_{ih_i}$ でそれぞれ置き換えた

$\displaystyle \exists c_{i1} \exists c_{i2} \cdots \exists c_{ig_i} (p''_{i1} \land p''_{i2} \land \cdots \land p''_{il_i} \rightarrow q''_i) \vdash r''$

を証明すればよいということになります(「 $\forall$ 左」)。

これを証明するには変数に依存した新しい定数 $c'_{i1} , c'_{i2}, \cdots , c'_{ig_i}$ を追加して(PLP では関数で表します) $c_{i1} , c_{i2}, \cdots , c_{ig_i}$ を $c'_{i1} , c'_{i2}, \cdots , c'_{ig_i}$ でそれぞれ置き換えた

$\displaystyle p'''_{i1} \land p'''_{i2} \land \cdots \land p'''_{il_i} \rightarrow q'''_i \vdash r''$

を証明すればよいということになります(「 $\exists$ 左」)。

これを証明するには

$\displaystyle \vdash p'''_{i1} \land p'''_{i2} \land \cdots \land p'''_{il_i}$

と

$\displaystyle q'''_i \vdash r''$

を証明すればよいということになります(「 $\rightarrow$ 左」)。

これを証明するには

$\vdash p'''_{i1}$ 、 $\vdash p'''_{i2}$ 、… 、 $\vdash p'''_{il_i}$

と

$\displaystyle q'''_i \vdash r''$

を証明すればよいということになります(「 $\land$ 右」)。

これを PLP の正規化された論理式の記法で書くと

$\displaystyle unify(q'''_i , r'') \land p'''_{i1} \land p'''_{i2} \land \cdots \land p'''_{il_i}$

という連言節となります。証明図に使う論理記号と PLP の正規化された論理式に使う論理記号が同じなのでわかりにくいですが、別の記号を使っても煩雑になるので同じ記号を使っていきます。

unify式だけからなる連言節が存在するので、そのインデックスを $i$ とすると、 $l_i = 0$ となりその連言節は $unify(q'''_i , r'')$ となって $q'''_i$ と $r''$ は一致します。これは証明図の公理となるので、ここから始めることで証明図を書くことができます。