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

以前説明したものの繰り返しになるのですが、もう少し詳しく説明したいと思います。その前に以前シークエント計算の説明をしたときに変数の説明が抜けていたようなので、これも以前の繰り返しになりますが説明したいと思います。

論理プログラミング

まず論理プログラミング(ここでは PLP と呼ぶことにします)のプログラムについて説明していきます。PLP のデータとなるものを項と呼ぶことにします。記号の有限集合 $C$ があってその元を定数と呼びます。定数は項となります。記号の可算集合 $V$ があってその元を変数と呼びます。変数は項となります。記号の有限集合 $F$ があってその元を関数と呼びます。関数 $f$ に対して $f(t_1, t_2, \cdots , t_n)$ という形の記号の列は項となります( $t_1, t_2, \cdots , t_n$ は項)。以上で定義された最小のものが項となります。項全体の集合を $T$ とおきます。関数は変数に依存した項を表すためのものとなっています。

記号の有限集合 $P$ があってその元を述語と呼びます。述語 $p$ に対して $p(t_1, t_2, \cdots , t_n)$ という形の記号の列はを述語式と呼ぶことにします。ここで $t_1, t_2, \cdots , t_n$ は項です。述語式全体の集合を $Q$ とおきます。
$\displaystyle q \mathop{:-} p_1, p_2, \cdots , p_n .$
の形の列をホーン節と呼びます。ここで $q, p_1, p_2, \cdots , p_n$ は述語式です。これは
$\displaystyle p_1 \land p_2 \land \cdots \land p_n \rightarrow q$
という論理式を表しています。以下では論理式の意味で使うこともあります。 $n=0$ の場合もあり、これは
$\displaystyle q .$
と書きます。ホーン節の $q$ がない場合は $q$ の部分が「偽」の場合を表し
$\displaystyle \lnot ( p_1 \land p_2 \land \cdots \land p_n )$
という論理式を表します。これをゴール節と呼び Prolog では
$\displaystyle \mathop{?-} p_1, p_2, \cdots , p_n .$
と書きます。これは(Prologでは含めるようですがここでは)ホーン節には含めないことにします。

PLP のプログラムは有限個のホーン節と1個のゴール節からなります。ゴール節は1個の述語式からなるものを考えます。複数の場合
$\displaystyle r \mathop{:-} p_1, p_2, \cdots , p_n .$
をゴール節に追加してゴール節は $r$ だけにすることができます。

PLP のプログラムは
$\begin{array}{llllll} q_1 & \mathop{:-} & p_{11}, & p_{12}, & \cdots , & p_{1n_1} . \\ q_2 & \mathop{:-} & p_{21}, & p_{22}, & \cdots , & p_{2n_2} . \\ & & & \vdots & & \\ q_m & \mathop{:-} & p_{m1}, & p_{m2}, & \cdots , & p_{mn_m} . \\ & \mathop{?-} & r . \end{array}$
という形のものでこれは以下の論理式を表しています。
$\displaystyle \exists t_1 \cdots \exists t_k (\delta \rightarrow r)$
ここで $t_1, \cdots , t_k$ は $r$ に現れるすべての変数を表します。 $\delta$ は以下の論理式を表します。
$\begin{array}{c} \forall v_{11} \forall v_{12} \cdots \forall v_{1\nu_1} \exists u_{11} \exists u_{12} \cdots \exists u_{1\mu_1} (p_{11} \land p_{12} \land \cdots \land p_{1n_1} \rightarrow q_1) \\ \land \\ \forall v_{12} \forall v_{22} \cdots \forall v_{2\nu_2} \exists u_{21} \exists u_{22} \cdots \exists u_{2\mu_2} (p_{21} \land p_{22} \land \cdots \land p_{2n_2} \rightarrow q_2) \\ \land \\ \vdots \\ \land \\ \forall v_{m1} \forall v_{m2} \cdots \forall v_{m\nu_m} \exists u_{m1} \exists u_{m2} \cdots \exists u_{m\mu_m} (p_{m1} \land p_{m2} \land \cdots \land p_{mn_m} \rightarrow q_m) \end{array}$

ここで $v_{i1}, v_{i2}, \cdots , v_{i\nu_i}$ は $p_{i1} \land p_{i2} \land \cdots \land p_{in_i} \rightarrow q_i$ に現れるすべての変数を表します。 $u_{i1}, u_{i2}, \cdots , u_{i\mu_i}$ は変数 $v_{i1}, v_{i2}, \cdots , v_{i\nu_i}$ とこれより下の証明図に現れる変数に依存した項を表しますが、PLP では変数に依存した項は「関数」として表されて、証明図としては同じものになります。

シークエント計算(変数あり)

PLP で述語式の列(ゴール節) $p_1, p_2, \cdots , p_m$ を実行するには、 $p_1$ 、 $p_2$ 、…、 $p_m$ をすべて(Prologの場合は順に)実行することになります。これは証明図で書くと以下のようになります。
$\displaystyle \cfrac {\delta \vdash p_1 \ \ \ \ \cdots \ \ \ \ \delta \vdash p_m \ \ \ \ q \vdash r} {\delta \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 右)$
PLP で述語式 $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 \vdash p_1 \land \cdots \land p_m \ \ \ \ q \vdash r} {\delta, 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 左)$
PLP で述語式 $r$ を実行するには、ホーン節の集合 $\delta$ の中の $q$ が $r$ と一致する一つのホーン節 $p_1 \land p_2 \land \cdots \land p_m \rightarrow q$ を選択することになります(Prologの場合はホーン節の選択を順に実行していって失敗した場合は次のホーン節をやり直すという手順になります)。このとき変数は $q$ が $r$ と一致するような項で置き換えることになります。これは証明図で書くと以下のようになります。
$\displaystyle \cfrac {\delta, p_1 \land \cdots \land p_m \rightarrow q \vdash r } {\delta, \exists u_1 \exists u_2 \cdots \exists u_\mu (p_1 \land \cdots \land p_m \rightarrow q) \vdash r} \ \ (\mu 回の \exists 左)$
$\displaystyle \cfrac {\delta, p_1 \land \cdots \land p_m \rightarrow q \vdash r } {\delta, \forall v_1 \forall v_2 \cdots \forall v_\nu \exists u_1 \exists u_2 \cdots \exists u_\mu (p_1 \land \cdots \land p_m \rightarrow q) \vdash r} \ \ (\nu 回の \forall 左)$
$\displaystyle \cfrac {\delta, \forall v_1 \forall v_2 \cdots \forall v_\nu \exists u_1 \exists u_2 \cdots \exists u_\mu (p_1 \land \cdots \land p_m \rightarrow q) \vdash r } {\delta , \delta \vdash r} \ \ (\land 左1または \land 左2と何回かの項の交換)$
$\displaystyle \cfrac {\delta, \delta \vdash r } {\delta \vdash r} \ \ (縮約左)$
これは以下の証明図のパターンの項を論理式で置き換えたものとなります。
$\displaystyle \cfrac {\Gamma, A[y/x] \vdash \Delta} {\Gamma, \exists x A \vdash \Delta} \ \ (\exists 左)$
$\displaystyle \cfrac {\Gamma, A[t/x] \vdash \Delta} {\Gamma, \forall x A \vdash \Delta} \ \ (\forall 左)$
$\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)$
$A[t/x]$ は $A$ 内の変項 $x$ の全ての自由出現を項 $t$ で置換した論理式を表します。PLP では「関数」の形で変数に依存する項を書くことになっているので $\exists 左$ は必要ないということになります。

ここまでが1回分の証明図となります。PLP の動作としてはここまでですが、さらに証明を続けると以下のようになります。
$\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$ と書きます)の組み合わせで書けるもの(自由分配束)を「シークエント式」と呼ぶことにします。「シークエント式」を使って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}{cccccccccc} \delta, & \forall v_{11} \cdots \forall v_{1\nu_1} \exists u_{11} \cdots \exists u_{1\mu_1} ( & p_{11} & \land & \cdots & \land & p_{1n_1} & \rightarrow & q_1 & ) & \\ & & \lor & & & & & & & \\ & & \vdots & & & & & & & \\ & & \lor & & & & & & & \\ & \forall v_{m1} \cdots \forall v_{m\nu_m} \exists u_{m1} \cdots \exists u_{m\mu_m} ( & p_{m1} & \land & \cdots & \land & p_{mn_m} & \rightarrow & q_m & ) & \vdash r \end{array}}$
図の上の $p_{ij}$ と $q_i$ は変数を適当な項で置き換えたものとなります。

シークエント計算(変数なし)

変数ありの証明図を見てみると、 $r$ の変数については、変数であっても変数を項で置き換えたものであっても、そこまでの証明図は同じものになることがわかります。また $\forall 左$ についても証明図に書けるのは一つの項だけなので、最初からその項を書けば証明図としては同じものになるということがわかります。したがって $\forall 左$ と $\exists 右$ はあってもなくても証明図としては同じものになるということがわかります。それらを省略して変数を含まない形で書いてみます。

PLP で述語式の列(ゴール節) $p_1, p_2, \cdots , p_m$ を実行するには、 $p_1$ 、 $p_2$ 、…、 $p_m$ をすべて実行することになります。これは証明図で書くと以下のようになります。
$\displaystyle \cfrac {\delta \vdash p_1 \ \ \ \ \cdots \ \ \ \ \delta \vdash p_m \ \ \ \ q \vdash r} {\delta \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 右)$
PLP で述語式 $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 \vdash p_1 \land \cdots \land p_m \ \ \ \ q \vdash r} {\delta, 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 左)$
PLP で述語式 $r$ を実行するには、ホーン節の集合 $\delta$ の中の $q$ が $r$ と一致する一つのホーン節 $p_1 \land p_2 \land \cdots \land p_m \rightarrow q$ を選択することになります。これは証明図で書くと以下のようになります。
$\displaystyle \cfrac {\delta, p_1 \land \cdots \land p_m \rightarrow q \vdash r } {\delta , \delta \vdash r} \ \ (\land 左1または \land 左2と何回かの項の交換)$
$\displaystyle \cfrac {\delta, \delta \vdash r } {\delta \vdash r} \ \ (縮約左)$
これは以下の証明図のパターンの項を論理式で置き換えたものとなります。
$\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回分の証明図となります。PLP の動作としてはここまでですが、さらに証明を続けると以下のようになります。
$\displaystyle \cfrac {\delta \vdash r } {\vdash \delta \rightarrow r} \ \ (\rightarrow 右)$
これは以下の証明図のパターンの項を論理式で置き換えたものとなります。
$\displaystyle \cfrac {\Gamma, A \vdash B, \Delta} {\Gamma \vdash A \rightarrow B, \Delta} \ \ (\rightarrow 右)$

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}}$