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

$S$ を集合(本来は「シークエント」全体の集合)、 $S$ で自由生成された代数系(本来は分配束)全体の集合を $L$ とおきます(Wikipediaによると代数的構造を持つ集合は代数系と呼びます)。 $L$ は本来は分配束なのですが、可換冪等半環、可換半環、可換環の場合も考えていきます。 $L$ の冪集合を $P(L)$ とおきます。

「シークエント」の記号で書かれた有限個のホーン節からなる集合のことを指す言葉をまだ決めていなかったのでここで決めたいと思います。これは論理プログラミングの推論規則に相当するものなので「論理プログラミング推論規則」と呼ぶことにします。「論理プログラミング推論規則」全体の集合(に相当する一般の代数系のもの)を $D$ とおきます。上記の場合と同様、これは一般の代数系の場合も含むものとします。

$d \in D$ に対応する推論規則を $\rho_d$ とおきます。 $s \in S$ に対して推論規則 $\rho_d$ によって $s$ に変換することができる $L$ の元全体の集合を $\delta_d(s)$ とおきます( $\delta_d(s)$ の元は「同型を除いて一意的」となります)。 $\delta_d: S \rightarrow P(L)$ は $\delta_d: L \rightarrow P(L)$ に拡張することができます。

$\delta_d$ の「逆」として部分写像 $L \rightarrow L$ を考えることができます。これを(推論規則と同じ記号を使って) $\rho_d$ とおきます( $\rho_d: \delta_d(L) \rightarrow L$ )。

ここでいったん $L$ は分配束で $\top$ (「真」を表す)と $\bot$ (「偽」を表す)を持つものとします。 $M \subseteq L$ に対して $M$ のすべての元を $\vee$ (「または」を表す)で結んだものを $\bigvee M$ と書くことにします。 $s \in S$ に対して論理プログラミングのプログラム $(d, s)$ は

$\bigvee \rho_d^{-n}(s) = \top$ を満たす $n \in \mathbb{N}$ が存在するとき $(d, s)$ は成功
$\bigvee \rho_d^{-n}(s) = \bot$ を満たす $n \in \mathbb{N}$ が存在するとき $(d, s)$ は失敗
成功でも失敗でもないとき $\bigcup_{n \in \mathbb{N}} \rho_d^{-n}(s)$ を $(d, s)$ の極限と呼びます。

一般の場合でも $\bigcup_{n \in \mathbb{N}} \rho_d^{-n}(s)$ を考えることはできるので、以下では一般の場合で考えていきます。

$L$ を $0$ と $1$ を持つ可換半環とします。ホーン節 $q \leftarrow p_1 \land \cdots \land p_n$ によって $s \in S$ は $(s \equiv q) p_1 \cdots p_n$ に(証明の逆の方向に)変換されるとします。 $(s \equiv q)$ は $s$ と $q$ が一致するときに $1$ 、 $s$ と $q$ が一致しないときに $0$ となるものとします。 $d \in D$ による変換 $\delta_d: S \rightarrow P(L)$ はこの和として定義します。変数の置き換え方が複数あるため変換された先のものは複数あり、変数の置き換えによる同値関係を除いて一意的となります。この、証明の逆の方向に変換されたものの全体が $\delta_d(s)$ となります。この「逆」の $\rho_d: \delta_d(L) \rightarrow L$ を定義することができます。 $\sum$ は和を表します。