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

PLP のプログラムは形としてはPrologのプログラムで、実行順序のないものとします(以下で少しずつどういうことか説明していきます)。PLPのプログラムは論理的には

$\displaystyle \exists t_1 \exists t_2 \cdots \exists t_n d \rightarrow r$

という論理式と考えることができます。ここで $r$ は

$\displaystyle p(u_1, u_2, \cdots , u_m)$

という形の式とします。 $p$ は述語、各 $u_i$ は項または変数です。この形の論理式を述語式と呼ぶことにします。 $d$ は

$\displaystyle a_1 \land a_2, \land \cdots \land a_k$

という形の論理式で、各 $a_i$ は

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

という形の論理式で、各 $p_{ij}$ と各 $q_i$ は述語式です。

PLP のプログラムを論理式と考えて、それを証明することを考えます。証明は「シークエント計算」に基づいて行っていきますが、正確な説明にはなりませんが「シークエント計算」の全体を説明すると長くなるので必要な部分だけを書いていくことにします。

まず上記の

$\displaystyle \vdash \exists t_1 \exists t_2 \cdots \exists t_n d \rightarrow r$

を証明するには、新しい項 $t'_1, t'_2, \cdots t'_n$ を追加して $d \rightarrow r$ に現れる $t_1, t_2, \cdots t_n$ を $t'_1, t'_2, \cdots t'_n$ にそれぞれ置き換えたものを $d' \rightarrow r'$ と書くとすると、

$\displaystyle \vdash d' \rightarrow r'$

を証明すれば十分となります(「シークエント計算」の「 $\exists$ 右」)。 $d$ が $d(t_1, t_2, \cdots t_n)$ という述語、 $r$ が $r(t_1, t_2, \cdots t_n)$ という述語とすると、 $d' \rightarrow r'$ は $d(t'_1, t'_2, \cdots t'_n) \rightarrow r(t'_1, t'_2, \cdots t'_n)$ となります。

次に $\vdash d' \rightarrow r'$ を証明するには、 $d' \vdash r'$ を証明すれば十分となります(「 $\rightarrow$ 右」)。

$d' \vdash r'$ を証明するには $d', d' \vdash r'$ を証明すれば十分となります(「簡約左」)。

$d', d' \vdash r'$ を証明するには $d', a'_i \vdash r'$ をどれかの $i$ に対して証明すれば十分となります(「 $\land$ 左」の繰り返し)。ここで $a'_i$ は $a_i$ に同様の変換を行ったものとします。Prolog ではこの $i$ についての実行順序は固定となりますが、PLP ではプログラムは並行に実行されるとしてすべての $i$ に対して実行されるものとします。

各 $a'_i$ を

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

とおくと、

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