論理計算と随伴関手(10) - 非専門的シンギュラリティー研究所

論理プログラミングのプログラムが成功したとき、変数は変数を含まない項に置き換えられるのが普通です。したがって成功したときの場合を考えると、変数の代わりにすべての変数を含まない項について調べれば良いということになります。

$S$ を「シークエント」全体の集合とします。 $\bar{S}$ を $S$ の部分集合で変数を含まないもの全体とします。 $s \in S$ に対して $s$ に含まれるすべての変数を変数を含まない項で置き換えたもの全体の集合を $\bar{S}(s)$ とおきます。

$L$ を $S$ で自由生成された $1$ と $0$ を持つ可換半環とします。 $\bar{L}$ を $L$ の部分集合で変数を含まないもの全体とします。 $x \in L$ に対して $x$ に含まれるすべての変数を変数を含まない項で置き換えたもの全体の集合を $\bar{L}(x)$ とおきます。

$s \in S$ と $s_1, \cdots , s_n \in S$ に対して $s \leftarrow s_1 \cdots s_n$ という形のものをホーン節と呼ぶことにします。ホーン節全体の集合 $H$ で自由生成された可換モノイドを $D$ とおきます。 $D$ の部分集合で変数を含まないもの全体を $\bar{D}$ とおき、 $d \in D$ に対して $d$ に含まれるすべての変数を変数を含まない項で置き換えたもの全体の集合を $\bar{D}(d)$ とおきます。

$\bar{H}$ を $H$ の部分集合で変数を含まないもの全体とします。

まず $s \in \bar{S}$ と $h \in \bar{H}$ に対して $\delta_h(s) \in \bar{L}$ を考えます。 $h$ を $q \leftarrow p_1 \cdots p_n$ という形のホーン節とします。 $\delta_h(s) = (s \equiv q) p_1 \cdots p_n$ と定義します。ここで $s \equiv q$ は $s$ と $q$ が一致するとき $1$ 、 $s$ と $q$ が一致しないとき $0$ となるものとします。

$d \in \bar{D}$ をとると $d$ は有限個の変数を含まないホーン節の和なので $h_1, \cdots , h_m \in \bar{H}$ が存在して $d = h_1 + \cdots + h_m$ と書くことができます。 $\delta_d(s) = \delta_{h_1}(s) + \cdots + \delta_{h_m}(s)$ と定義します。 $\delta_d : \bar{S} \rightarrow \bar{L}$ となります。これを拡張して $\delta_d : \bar{L} \rightarrow \bar{L}$ とすることができます。

次に $s \in S$ と $d \in D$ をとります。 $s' \in \bar{S}(s)$ に対して $\bar{\delta}_{d}(s') = \{ \delta_{d'}(s') | d' \in \bar{D}(d) \}$ と定義します。 $\bar{\delta}_{d}$ を $n$ 回適用した $\bar{\delta}_{d}(\bar{\delta}_{d}(\cdots \bar{\delta}_{d}(s')\cdots))$ を $\bar{\delta}_{d}^n(s')$ と書きます。これによって $\bar{\delta}_{d}^n : \bar{S} \rightarrow P(\bar{L})$ が定義できます。ここで $P(\bar{L})$ は $\bar{L}$ の冪集合を表します。 $\bar{\delta}_{d}^n : S \rightarrow P(\bar{L})$ を $\bar{\delta}_{d}^n (s) = \bigcup_{s' \in \bar{S}(s)} \bar{\delta}_{d}^n (s')$ と定義します。

$L$ が分配束のときは $\sum \bar{\delta}_d^{n}(s) = 1$ を満たす $n \in \mathbb{N}$ が存在するとき論理プログラミングのプログラム $(d, s)$ は成功
$\sum \bar{\delta}_d^{n}(s) = 0$ を満たす $n \in \mathbb{N}$ が存在するとき $(d, s)$ は失敗
$\sum_{n \in \mathbb{N}} \sum \bar{\delta}_d^{n}(s)$ を $(d, s)$ の極限と呼びます。