論理計算と随伴関手(6) - エレファント・ビジュアライザー調査記録

論理プログラミングとシークエント計算の関係について以前書いていましたが、まとめてみます。

論理プログラミングで述語式の列(ゴール節) $p_1, p_2, \cdots , p_m$ を実行するには、 $p_1$ 、 $p_2$ 、…、 $p_m$ をすべて(Prologの場合は順に)実行することになります。これは証明図で書くと以下のようになります。

$\displaystyle \cfrac {\delta^{l-1} \vdash p_1 \ \ \ \ \cdots \ \ \ \ \delta^{l-1} \vdash p_m \ \ \ \ q \vdash r} {\delta^{l-1} \vdash p_1 \land \cdots \land p_m \ \ \ \ q \vdash r} (m -1 回の \land 右の図をまとめたもの)$

これは以下の証明図のパターンの項を論理式で置き換えたものを複数組み合わせたものをまとめたものとなります。

$\displaystyle \cfrac {\Gamma \vdash A, \Delta \ \ \ \ \Sigma \vdash B, \Pi} {\Gamma, \Sigma \vdash A \land B, \Delta, \Pi} \ \ (\land 右)$

論理プログラミングで述語式 $r$ を一つのホーン節 $p_1 \land p_2 \land \cdots \land p_m \rightarrow q$ に対して実行することは、 $q$ が $r$ が一致するかどうかを調べて、ゴール節 $p_1 \land p_2 \land \cdots \land p_m$ を実行することになります。これは証明図で書くと以下のようになります。

$\displaystyle \cfrac {\delta^{l-1} \vdash p_1 \land \cdots \land p_m \ \ \ \ q \vdash r} {\delta^{l-1}, p_1 \land \cdots \land p_m \rightarrow q \vdash r } \ \ (\rightarrow 左)$

これは以下の証明図のパターンの項を論理式で置き換えたものとなります。

$\displaystyle \cfrac {\Gamma \vdash A, \Delta \ \ \ \ \Sigma, B \vdash \Pi} {\Gamma, \Sigma, A \rightarrow B \vdash \Delta, \Pi } \ \ (\rightarrow 左)$

論理プログラミングで述語式 $r$ を実行するには、ホーン節の集合 $\delta$ の中の $q$ が $r$ と一致する一つのホーン節 $p_1 \land p_2 \land \cdots \land p_m \rightarrow q$ を選択することになります(Prologの場合はホーン節の選択を順に実行していって失敗した場合は次のホーン節をやり直すという手順になります)。
これは証明図で書くと以下のようになります。

$\displaystyle \cfrac {\delta^{l-1}, p_1 \land \cdots \land p_m \rightarrow q \vdash r } {\delta^l \vdash r} \ \ (\land 左1または \land 左2と何回かの項の交換)$

これは以下の証明図のパターンの項を論理式で置き換えたものとなります。

$\displaystyle \cfrac {\Gamma, A \vdash \Delta} {\Gamma, A \land B \vdash \Delta} \ \ (\land 左1)$

$\displaystyle \cfrac {\Gamma, B \vdash \Delta} {\Gamma, A \land B \vdash \Delta} \ \ (\land 左2)$

ここまでが1回分の証明図となります。論理プログラミングの動作としてはここまでですが、さらに証明を続けると以下のようになります。

$\displaystyle \cfrac {\delta^l \vdash r } {d \vdash r} \ \ (l - 1 回の縮約左)$

$\displaystyle \cfrac {\delta \vdash r } {\vdash \delta \rightarrow r} \ \ (\rightarrow 右)$

$\displaystyle \cfrac {\vdash \delta \rightarrow r} {\vdash \exists t_1 \cdots \exists t_k (\delta \rightarrow r)} \ \ (k 回の \exists 右)$

これは以下の証明図のパターンの項を論理式で置き換えたものとなります。

$\displaystyle \cfrac {\Gamma, A \vdash B, \Delta} {\Gamma \vdash A \rightarrow B, \Delta} \ \ (\rightarrow 右)$

$\displaystyle \cfrac {\Gamma \vdash A[t/x], \Delta} {\Gamma \vdash \exists x A, \Delta} \ \ (\exists 右)$
( $A[t/x]$ は $A$ 内の変項 $x$ の全ての自由出現を項 $t$ で置換した論理式を表します)

1回分の証明図をまとめて書くことを考えます。「 $\Gamma \vdash \Delta$ 」という形のものと論理積(ここでは $\sqcap$ と書きます)と論理和(ここでは $\sqcup$ と書きます)の組み合わせで書けるもの(自由分配束)を「シークエント式」と呼ぶことにします。「シークエント式」の全体を $Seq$ と書きます。1回分の証明図をまとめると以下のようになります。

$\cfrac {\begin{array}{ccccccc} \delta \vdash p_{11} & \sqcap & \cdots & \sqcap & \delta \vdash p_{1n_1} & \sqcap & q_1 \vdash r \\ & & & \sqcup & & & \\ & & & \vdots & & & \\ & & & \sqcup & & & \\ \delta \vdash p_{m1} & \sqcap & \cdots & \sqcap & \delta \vdash p_{mn_m} & \sqcap & q_m \vdash r \end{array}} {\begin{array}{cccccccc} \delta, & p_{11} & \land & \cdots & \land & p_{1n_1} & \rightarrow & q_1 & \\ & & & & \lor & & & & \\ & & & & \vdots & & && \\ & & & & \lor & & && \\ & p_{m1} & \land & \cdots & \land & p_{mn_m} & \rightarrow & q_m & \vdash r \end{array}} \ \ \ \ (\rho)$

この推論規則を $\rho$ とします。 $\rho$ は $Seq$ から $Seq$ への部分写像 $\rho: Seq \rightarrow Seq$ と考えることができます。
この逆写像を $\rho^{-1}$ とすると論理プログラミングのプログラム $(\delta, t)$ は $\top \in \rho^{-n}(\delta \vdash t)$ を満たす $n \in \mathbb{N}$ が存在するとき成功となります( $\top \in Seq$ は $Seq$ の中の $true$ を表すものとします)。
$\rho^{-n}(\delta \vdash t)$ の元がすべて $\bot$ となる $n \in \mathbb{N}$ が存在するとき失敗となります( $\bot \in Seq$ は $Seq$ の中の $false$ を表すものとします)。
それ以外の場合は無限の回数実行されます。