半環上のフラクタル代数(8) - エレファント・コンピューティング調査報告

Prolog の動作を説明するため、集合 $X$ に対して $\mathcal{S}(X) = S(S(X))$ と $\mathcal{F}(X) = F(F(X))$ を考えました。 $\mathcal{S}(X)$ は Prolog のデータの「標準形」を作るためのもので、 $\mathcal{F}(X)$ は理論的な論理プログラミングのデータの「標準形」を作るためのものです。

$\mathcal{F}(X)$ は半環になっています。半環の場合は「選言標準形」に変形することができるので「標準形」を作る議論は必要ないのですが、Prolog と対応させるために定義してあります。

理論的な論理プログラミングは証明に対応しています。Prolog のデータはそれを非可換にしたものと考えられ、演算の順序が実行順序に対応しています。ここでは、理論的な論理プログラミングの実行順序を決める方法を考えるため、Prolog と関連付けて議論しています。これは Prolog と関連付ける方がわかりやすいかもしれないためですが、本来はこの議論は不要かもしれません。

論理プログラミングと証明の関係について「論理計算と随伴関手(13)」で説明していたのですが、説明が間違っていました。関数名と述語名は有限個しかないのでそれらの関係を全部付け加えればできると簡単に考えていたのですが、そんなに簡単ではないようです。今回説明をやり直します。

まず $\mathcal{F}(X)$ の「プログラム微分」と「代入」について考えます。「プログラム微分」は Prolog のプログラムの基本的な単位を1回だけ実行することに対応したものです。

論理プログラミングのプログラム微分

集合 $X$ に対して $R = \mathcal{F}(X)$ は半環(単位元を持つ自明ではない冪等可換半環)となります。

$S$ を単位元を持つ自明ではない半環とし、 $f: X \to S$ とします。 $x \in R$ は
$x = x_{11} x_{12} \cdots x_{1m_1} + x_{21} x_{22} \cdots x_{2m_2} + \cdots + x_{n1} x_{n2} \cdots x_{nm_n}$ $(x_{ij} \in X)$
と順序を除いて一意的に表すことができます。よって $f^*: R \to S$ を
$f^*(x) = f(x_{11}) f(x_{12}) \cdots f(x_{1m_1}) + f(x_{21}) f(x_{22}) \cdots f(x_{2m_2}) + \cdots + f(x_{n1}) f(x_{n2}) \cdots f(x_{nm_n})$
と定義することができます。 $f^*$ は半環の準同型となります。

集合 $X$ から集合 $Y$ への写像 $f: X \to Y$ に対して $f: X \to \mathcal{F}(X)$ と考えると半環の準同型 $f^* : \mathcal{F}(X) \to \mathcal{F}(X)$ を定義することができます。

$X$ を集合、 $R = \mathcal{F}(X)$ 、 $f: X \to R$ とします。 $Y \subseteq X$ 、 $r \in R$ に対して、 $\rho_{f,Y,r}: X \to R$ を $x \in Y$ のとき $\rho_{f,Y,r}(x) = f(x)$ 、 $x \notin Y$ のとき $\rho_{f,Y,r}(x) = r$ と定義します。

論理プログラミングのデータ

集合 $X$ と $Y$ に対して、 $X$ と $Y$ の直和を $X + Y$ 、 $X$ と $Y$ の直積を $X \times Y$ と書きます。 $X$ の $n$ 個の直積( $n$ は自然数)を $X^n$ と書きます。 $0$ 個の直積も考えます。 $X^* = X^0 + X^1 + X^2 + \cdots X^n$ と書きます。

$C$ (Prolog の定数名に対応)、 $F$ (Prolog の関数名に対応)、 $P$ (Prolog の述語名に対応)を有限集合、 $V$ (Prolog の変数名に対応)を可算集合とします。

$T = V + C + F \times T^*$ (Prolog の項に対応)、
$S = P \times T^*$ (Prolog の述語の項に対応)、
$Q = S^* \times S$ (Prolog のホーン節に対応)、
$P = Q^*$ (Prolog のプログラムに対応)、
$E = S \times S$ (Prolog の述語の項が一致することを表すものに対応)、
$U = E + S$ (Prolog の述語の項が一致することを表すもの、または述語の項に対応)

とします。これらのもののうち変数を含まないものを

$T_C = C + F \times T_C^*$ (Prolog の変数を含まない項に対応)、
$S_C = P \times T_C^*$ (Prolog の変数を含まない述語の項に対応)、
$Q _C= S_C^* \times S_C$ (Prolog の変数を含まないホーン節に対応)、
$P_C = Q_C^*$ (Prolog の変数を含まないプログラムに対応)、
$E_C = S_C \times S_C$ (Prolog の変数を含まない述語の項が一致することを表すものに対応)、
$U_C = E_C + S_C$ (Prolog の変数を含まない述語の項が一致することを表すもの、または変数を含まない述語の項に対応)

とします。

論理プログラミングの定義

$\lambda: Q \times S \to \mathcal{F}(U)$ を $( (s_1, s_2, \cdots , s_n), h) \in Q$ $(s_1, s_2, \cdots , s_n, h \in S)$ と $x \in S$ に対して $\lambda( ( (s_1, s_2, \cdots , s_n), h), x) = e(h, x) s_1, s_2, \cdots , s_n$ と定義します。 $e(h, x) \in E$ は $h$ と $x$ が一致することを表すものとします。

$\gamma: P \times S \to \mathcal{F}(U)$ を $( q_1, q_2, \cdots , q_m) \in P$ $(q_1, q_2, \cdots , q_m \in Q)$ と $x \in S$ に対して $\gamma( (q_1, q_2, \cdots , q_m), x) = \lambda(q_1, x) + \lambda(q_2, x) + \cdots + \lambda(q_m, x)$ と定義します。ただし $q_i$ と $q_j$ $(i \ne j)$ に現れる変数は重複しないものとします。 $q_i$ に現れる変数は $V_i$ に含まれるとし、 $V = V_1 + \cdots + V_m$ とします。

$p \in P$ に対して $\delta_p: U \to \mathcal{F}(U)$ を $x \in S$ のとき $\delta_p(x) = \gamma(p, x)$ 、 $x \in E$ のとき $\delta_p(x) = x$ と定義します。

$\delta_p^*: \mathcal{F}(U) \to \mathcal{F}(U)$ となります。 $\delta_p^*: \mathcal{F}(U) \to \mathcal{F}(U)$ を $n$ 回繰り返したものを $\delta_p^{*n}: \mathcal{F}(U) \to \mathcal{F}(U)$ とします。ただし $i$ 回目の $p$ ( $p_i$ とします)と $j$ 回目の $p$ ( $p_j$ とします) $(i \ne j)$ に現れる変数は重複しないものとします。 $p_i$ に現れる変数は $V_i$ に含まれるとし、 $V = V_1 + V_2 + \cdots$ とします。 $V$ は可算集合としたので可算回繰り返すことができます。変数以外は同じものとします。

論理プログラミングの代入

$\sigma: V \to T_C$ を代入と呼びます。代入全体の集合を $\Sigma$ とおきます。変数以外は保存されるものとして、 $\sigma: V \to T_C$ を $\bar{\sigma}: U \to U_C$ に拡張することができます。

$\iota: U \to U$ を恒等写像とします。

$\bar{\sigma}(\rho_{\iota,E,0}^*(\delta_p^{*n}(x))) = 1$ を満たす $\sigma \in \Sigma$ が存在するとき $(p, x)$ は $n$ 回で成功
$\bar{\sigma}(\rho_{\iota,E,1}^*(\delta_p^{*n}(x))) = 1$ を満たす $\sigma \in \Sigma$ が存在しないとき $(p, x)$ は $n$ 回で失敗

ということにします。

シークエント計算

これをシークエント計算に対応させます。シークエント計算の $n$ 回はプログラム微分の $n$ 回に対応するものとします。

$p \in P$ 、 $x \in S$ とし、 $(p, x)$ は $n$ 回で成功とします。このときシークエント計算の図を書くことができることを示します。これを $n$ 回の図ということにします。

まず $n = 1$ のときを考えます。

ホーン節に対応する論理式を考えます。

$T = V + C + F \times T^*$ (Prolog の項に対応)の元が $(f, (t_1, t_2, \cdots , t_n)) \in F \times T^n$ $(f \in F, t_1, t_2, \cdots , t_n \in T)$ のとき $n$ を関数 $f$ の引数の個数と呼び $a(f)$ と表すことにします( $n$ -ary ( $n$ 項の)を表す)。引数の個数が異なる関数は異なる関数とします(Prolog では関数名は同じものにできるが関数としては異なるものとする)。

各 $f \in F$ に対して $n = a(f)$ とするとき述語 $r_f(x_1, \cdots , x_n, y)$ を追加し、 $\forall x_1 \cdots \forall x_n \exists y \ r_f(x_1, \cdots , x_n, y)$ を証明の前提に追加します。

$q \in Q = S^* \times S$ (Prolog のホーン節に対応)、 $q = ( (s_1, s_2, \cdots , s_n), h)$ $(s_1, s_2, \cdots , s_n, h \in S)$ とします。

$q$ に関数が現れるごとにそれに対応した変数を追加します。 $q$ に関数 $f(t_1, t_2,\cdots , t_n)$ が現れたとします。その $f(t_1, t_2,\cdots , t_n)$ の出現を、この出現に対応する変数 $v_f$ で置き換えます。そして $s_1, s_2, \cdots , s_n$ の列に $r_f(t_1, t_2,\cdots , t_n, v_f)$ を追加します。この変形によって関数の出現が1つ減ります。よってこの変形を繰り返すことにより、 $q$ に関数が現れないように変形することができます。

関数が現れないように変形した $q = ( (s_1, s_2, \cdots , s_n), h)$ に対して $\forall x_1 \cdots \forall x_m (s_1 \land s_2 \land \cdots \land s_n \implies h)$ を $\bar{q}$ とおきます。ここで $x_1, \cdots , x_m$ は $q$ に現れるすべての変数とします。

$p = (q_1, \cdots , q_k) \in P$ に対して $\bar{q_1} \land \cdots \land \bar{q_k}$ を $\bar{p}$ とおきます。

同様に $u \in S$ を関数が現れないように変形します。 $\exists v_1 \cdots \exists v_c u$ を $\bar{u}$ とおきます。ここで $v_1, \cdots , v_c$ は $u$ に現れるすべての変数とします。

上で追加した $\forall x_1 \cdots \forall x_n \exists y \ r_f(x_1, \cdots , x_n, y)$ の全体を $r_1, \cdots , r_l$ とし、 $\bar{r} = r_1 \land \cdots \land r_l$ とおきます。

すると $\bar{r} \land \bar{p} \implies \bar{u}$ を証明する図を書くことができます。

LK の記法を一部使って書きます。
$\begin{eqnarray*} & \vdash & \bar{r} \land \bar{p} \implies \bar{u} \\ & \Uparrow & (右 \implies) \\ \bar{r} \land \bar{p} & \vdash & \bar{u} \\ & \Uparrow & (右 \exists の繰り返し) \\ \bar{r} \land \bar{p} & \vdash & \bar{u}' \\ & \Uparrow & (左 \forall の繰り返し) \\ \bar{r}' \land \bar{p}' & \vdash & \bar{u}' \\ \end{eqnarray*}$
ここで $\bar{r}'$ は $\bar{r}$ の先頭の $\forall$ をすべて取り除いたもの、ここで $\bar{p}'$ は $\bar{p}$ の先頭の $\forall$ をすべて取り除いたもの、ここで $\bar{u}'$ は $\bar{u}$ の先頭の $\exists$ をすべて取り除いたものとします。

簡単に書くために $\bar{r}'$ を $r$ 、 $\bar{p}'$ を $p$ 、 $\bar{u}'$ を $u$ と書きます。 $p = q_1 \land \cdots \land q_n$ のとき
$\begin{array}{c} r \land q_1 \land \cdots \land q_n \vdash u \\ \Uparrow (左 \land の繰り返し) \\ r , q_1 , \cdots , q_n \vdash u \\ \Uparrow (左増加の繰り返し) \\ ( r , q_1 \vdash u ) \sqcup \cdots \sqcup ( r , q_n \vdash u ) \\ \end{array}$
となります。ここで $q_i = s_1 \land \cdots \land s_n \implies h$ のとき
$\begin{array}{c} r , s_1 \land \cdots \land s_n \implies h \vdash u \\ \Uparrow (左 \implies) \\ (r \vdash s_1 \land \cdots \land s_n) \sqcap (r, h \vdash u) \\ \Uparrow (右 \land) \\ (r \vdash s_1) \sqcap \cdots \sqcap (r \vdash s_n) \sqcap (r, h \vdash u) \\ \end{array}$
となります。ここまでが1回目とします。 $n = 0$ のとき1回で成功とします。

2回目からは $u$ の代わりに $s_i$ として $r, p \vdash s_i$ から続けます。

$p$ を途中で増やすことはできないものとして、 $r, p, \cdots , p \vdash u$ ( $p$ の個数は $n$ 個、 $p^n$ と書きます)の図を書くことができるとき $n$ 回の図を書くことができるとします。

論理プログラミングの $\delta_p^{*n}$ に対応する「 $n$ 回までの図」を考えることができます。 $r, p^n \vdash u$ から始めて $n$ 回まで書いたものを $\Delta_{r, p,n}(u)$ とします。

$e'(x, y)$ を $x = y$ のとき $e'(x, y) = 1$ 、 $x \ne y$ のとき $e'(x, y) = 0$ とします。定数は有限個なので定義できます。

論理プログラミングの述語の項に対応するものを、シークエントでも述語の項と呼ぶことにします。述語の項 $p(x_1, \cdots , x_m)$ と $q(y_1, \cdots , y_n)$ に対して、 $p(x_1, \cdots , x_m) \equiv q(y_1, \cdots , y_n)$ を

$p = q$ のとき(このとき $m = n$ としました) $e'(x_1, y_1) \land \cdots \land e'(x_m, y_m)$ 、
$p \ne q$ のとき $0$

と定義します。

あまりうまく書けていないので、この項は後でちゃんと書き直すことにします。

シークエント計算の半環

$Z = P \times S$ (シークエントを表す)、 $E' = T \times T$ ( $e(x, y)$ を表す)とします。 $W = Z + E'$ とおいて $\mathcal{F}(W)$ (シークエントで生成される半環を表す)の計算を考えます。

$Q \times S \subseteq W$ と考えて、 $\Lambda_{r}: Q \times S \to \mathcal{F}(W)$ を $( (s_1, s_2, \cdots , s_n), h) \in Q$ $(s_1, s_2, \cdots , s_n, h \in S)$ と $x \in S$ に対して $\Lambda_{r}( ( (s_1, s_2, \cdots , s_n), h), x) = (h \equiv x) s_1, s_2, \cdots , s_n$ と定義します。

この場合も、先頭の $\forall$ と $\exists$ を取り除いたものから始めます。

$\mathcal{F}(U)$ の加法を $\lor$ 、乗法を $\land$ 、 $\mathcal{F}(W)$ の加法を $\sqcup$ 、乗法を $\sqcap$ と書くことにして、「LKの変形版」で書くと
$\begin{array}{c} r , s_1 \land \cdots \land s_n \implies h \vdash x \\ \Uparrow (左 \implies) \\ (r \vdash s_1 \land \cdots \land s_n) \sqcap (r, h \vdash x) \\ \Uparrow (右 \land) \\ (r \vdash s_1) \sqcap \cdots \sqcap (r \vdash s_n) \sqcap (r \vdash h \equiv x) \\ \end{array}$
のように書けます。ここから $r$ を取り除いて書くこととし、 $\vdash s_i$ を $s_i$ と書くと $(h \equiv x) s_1, s_2, \cdots , s_n$ となります。(さらに進めると $e(t_1, t'_1) e(t_2, t'_2) \cdots e(t_k, t'_k) s_1, s_2, \cdots , s_n$ ( $h$ と $x$ の述語名が一致するとき、各 $t_i, t'_i$ は引数の項)、または $0$ ( $h$ と $x$ の述語名が一致しないとき)となります。この説明もわかりにくいので後で考えることとします。)

$\Gamma_{r}: P \times S \to \mathcal{F}(W)$ を $( q_1, q_2, \cdots , q_m) \in P$ $(q_1, q_2, \cdots , q_m \in Q)$ と $x \in S$ に対して $\Gamma_{r}( (q_1, q_2, \cdots , q_m), x) = \Lambda_{r}(q_1, x) + \Lambda_{r}(q_2, x) + \cdots + \Lambda_{r}(q_m, x)$ と定義します。ただし $q_i$ と $q_j$ $(i \ne j)$ に現れる変数は重複しないものとします。 $q_i$ に現れる変数は $V_i$ に含まれるとし、 $V = V_1 + \cdots + V_m$ とします。

これを「LKの変形版」で書くと
$\begin{array}{c} r \land q_1 \land \cdots \land q_n \vdash x \\ \Uparrow (左 \land の繰り返し) \\ r , q_1 , \cdots , q_m \vdash x \\ \Uparrow (左増加の繰り返し) \\ ( r , q_1 \vdash x ) \sqcup \cdots \sqcup ( r , q_m \vdash x ) \\ \end{array}$
となります。

$p \in P$ に対して $\Delta_{r,p}: W \to \mathcal{F}(W)$ を $x \in S$ のとき $\Delta_{r,p}(x) = \Gamma_r(p, x)$ 、 $x \in E$ のとき $\Delta_{r,p}(x) = x$ と定義します。

$\Delta_{r,p}^*: \mathcal{F}(W) \to \mathcal{F}(W)$ となります。 $\Delta_{r,p}^*: \mathcal{F}(W) \to \mathcal{F}(W)$ を $n$ 回繰り返したものを $\Delta_{r,p}^{*n}: \mathcal{F}(W) \to \mathcal{F}(W)$ とします。ただし $i$ 回目の $p$ ( $p_i$ とします)と $j$ 回目の $p$ ( $p_j$ とします) $(i \ne j)$ に現れる変数は重複しないものとします。 $p_i$ に現れる変数は $V_i$ に含まれるとし、 $V = V_1 + V_2 + \cdots$ とします。 $V$ は可算集合としたので可算回繰り返すことができます。変数以外は同じものとします。

シークエント計算の代入

$E'$ は $e(x,y)$ 全体の集合とします。

$\bar{\sigma}(\rho_{\iota,E',0}^*(\Delta_{r,p}^{*n}(x))) = 1$ を満たす代入 $\sigma \in \Sigma$ が存在するとき $p \vdash x$ のシークエント計算は $n$ 回で成功
$\bar{\sigma}(\rho_{\iota,E',1}^*(\Delta_{r,p}^{*n}(x))) = 1$ を満たす代入 $\sigma \in \Sigma$ が存在しないとき $p \vdash x$ のシークエント計算は $n$ 回で失敗