論理計算と随伴関手(14) - エレファント・コンピューティング調査報告

証明図の逆方向の極限

シークエント計算 LK の $\forall 左$ と $\exists 右$ の証明図のパターンを下から上にたどると、変数のところは推論が成立するような項で置き換えられれば良いということがわかります。すべての項について調べれば良いのですが証明図には一つの項しか書けないので、そこより下の図ではこの項を書くようにすれば $\forall 左$ と $\exists 右$ は必要ないということになります。 $\forall 右$ と $\exists 左$ については下の変数に依存した項が上に現れるのですが PLP では「関数」の形で表されているので $\forall 右$ と $\exists 左$ は必要ないということになります。したがって変数を含まない証明図を書くことができたことになります。

なかなかうまく説明できないのですが、証明図はもともと一つの項のことしか書くことができないためうまく説明することは難しいと思われます。

以上は証明図が書ける場合、すなわち証明が成功した場合ですが、証明図を逆にたどることで極限を考えるということがここの目的です。最初から逆方向の写像を考えた方がうまくいきそうなので、その方向で考えていくことにします。当初は証明図の方向の写像をまず考えて、その逆写像を考えた方が極限がうまく定義できると思ったのですが、うまくいかないのでいったんやめます。

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

$L$ を $S$ で自由生成された $1$ と $0$ を持つ可換半環で、任意の $x \in L$ に対して $1 + x = 1$ を満たすものとします。 $\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$ とおきます。 $\bar{H}$ を $H$ の元で変数を含まないもの全体の集合とします。

$H$ で自由生成された可換モノイドを $D$ とおきます。 $D$ の元で変数を含まないもの全体の集合を $\bar{D}$ とおき、 $d \in D$ に対して $d$ に含まれるすべての変数を変数を含まない項で置き換えたもの全体の集合を $\bar{D}(d)$ とおきます。

まず $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 \bar{S}$ と $d \in D$ をとります。 $\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}$ の冪集合を表します。

$s \in S$ と $d \in D$ に対して $\bar{\bar{\delta}}_{d}^n : S \rightarrow P(\bar{L})$ を $\bar{\bar{\delta}}_{d}^n (s) = \bigcup_{s' \in \bar{S}(s)} \bar{\delta}_{d}^n (s')$ と定義します。

$L$ の冪集合 $P(L)$ の元 $U$ に対して $\sum U$ を以下のように定義します。

$U$ が有限のとき $\sum U$ は $U$ のすべての元の和
$U' = \{ x \in U | x \ne 0 \}$ が有限のとき $\sum U = \sum U'$ (空集合のときは $0$ )
$1 \in U$ のとき $\sum U = 1$
それ以外のとき $\sum U = \bot$ (未定義)

$L$ の元からなる可算個の列 $a_1, a_2, a_3, \cdots$ に対して $a_1, a_1+a_2, a_1+a_2+a_3, \cdots$ という列を $\sum_{n \in \mathbb{N}}a_n$ と書くことにします。

$\sum_{n \in \mathbb{N}}a_n = (a_1, a_1+a_2, a_1+a_2+a_3, \cdots)$

これは $L$ の元の $i$ 個の列全体の集合 $L_i$ と列を $j$ 個に切り詰める写像 $f_{ij}: L_i \rightarrow L_j \ \ (i \ge j)$ からなる射影系の射影的極限 $\varprojlim L_i$ の元となります。

PLP のプログラム $(d, s)$ は

$\sum \bar{\bar{\delta}}_d^{n}(s) = 1$ を満たす $n \in \mathbb{N}$ が存在するとき $(d, s)$ は成功
$\sum \bar{\bar{\delta}}_d^{n}(s) = 0$ を満たす $n \in \mathbb{N}$ が存在するとき $(d, s)$ は失敗
$\sum_{n \in \mathbb{N}} \sum \bar{\bar{\delta}}_d^{n}(s)$ を $(d, s)$ の極限と呼ぶことにします。

$X(d, s, n) = \{ s' \in \bar{S}(s) | \sum \bar{\delta}_{d}^n(s') \ne 0 \}$ とおきます。
$X(d, s, 1), X(d, s, 2), X(d, s, 3), \cdots$
という可算個の列を極限の「解」と考えることができます(極限との関係は今後考えていきます)。