エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

論理プログラミング(4)

PLP の述語

集合 $T$ (述語の項を表す)とブール代数 $R$ (PLPの結果の成功または失敗を表す)に対して

$\displaystyle p: T^n \rightarrow R$

を( $n$ 項の)述語と呼びます。

これを拡張して可算集合 $V$ (変数を表す)に対して

$\displaystyle p: (T+V)^n \rightarrow R$

としたものも述語と呼びます。

有限個の述語の集合を $P$ とおきます。 $P$ の各元 $p$ に対して

$p(x_1, x_2, \cdots x_n)$

という形のものの全体(各 $x_i$ は $T+V$ の元)を $Q$ とおきます。

PLP の論理式

PLP の論理式全体の集合 $L$ を定義していきます。

$Q$ の元は $L$ の元となります。

$x$ と $y$ が $L$ の元ならば

$\displaystyle x \land y$ 、

$\displaystyle x \lor y$ 、

$\displaystyle x \rightarrow y$

は $L$ の元となります。

$x$ が $L$ の元で $v$ が $x$ に現れる自由変数ならば

$\displaystyle \forall v (x)$ 、

$\displaystyle \exists v (x)$

は $L$ の元となります。

以上を満たす最小のものを $L$ と定義します。

「 $x$ に現れる自由変数」をまだ定義していないので「 $x$ に現れる自由変数全体の集合 $V(x)$ 」を以下のように定義します。

$\displaystyle V(p(x_1, x_2, \cdots x_n)) = \{x_1, x_2, \cdots x_n\} \cap V$ 、

$\displaystyle V(x \land y) = V(x) \cup V(y)$ 、

$\displaystyle V(x \lor y) = V(x) \cup V(y)$ 、

$\displaystyle V(x \rightarrow y) = V(x) \cup V(y)$ 、

$\displaystyle V(\forall v (x)) = V(x) \setminus \{v\}$ 、

$\displaystyle V(\exists v (x)) = V(x) \setminus \{v\}$ 。

$V(x)$ が空集合のとき $x$ を閉論理式と呼びます。

次に PLP の動作を証明と考えるために必要な証明の理論について考えていきます。