半環上のフラクタル代数(9) - エレファント・ビジュアライザー調査記録

論理プログラミングとシークエント計算

集合の記法

集合 $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 の変数名に対応)を可算集合とします。

$f \in F$ に対して $f$ のアリティという自然数 $n = a_F(f)$ が決まっているとします。 $f$ のアリティは $f$ の引数の個数を表します。アリティの異なる元は異なる元とします。 $F_n = \{ f \in F \mid a_F(f) = n \}$ とおくと $F = F_0 + F_1 + \cdots$ となります。 $F_0$ はなくても良いのですが含めることにします。

$p \in P$ に対して $p$ のアリティという自然数 $n = a_P(p)$ が決まっているとします。 $p$ のアリティは $p$ の引数の個数を表します。アリティの異なる元は異なる元とします。 $P_n = \{ p \in P \mid a_P(p) = n \}$ とおくと $P = P_0 + P_1 + \cdots$ となります。 $P_0$ はなくても良いのですが含めることにします。

$T = V + C + F_0 +F_1 \times T + F_2 \times T^2 + \cdots$ (Prolog の項に対応)、
$S = P_0 + P_1 \times T + P_2 \times T^2 + \cdots$ (Prolog の述語の項に対応)、
$Q = S^* \times S$ (Prolog のホーン節に対応)、
$D = Q^*$ (Prolog のプログラムに対応)、
$E = S \times S$ (Prolog の述語の項が一致することを表すものに対応)、
$U = E + S$ (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: D \times S \to \mathcal{F}(U)$ を $( q_1, q_2, \cdots , q_m) \in D$ $(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^+_0 = V_1 + \cdots + V_m \subseteq V$ とします。

$p \in D$ に対して $\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)$ に現れる変数は重複しないものとします。 $V^+_i$ は $V^+_0$ と元の個数が同じ集合とします。 $p$ に現れる変数をそれに対応する $V^+_i$ の元で置き換えたものを $p_i$ とおきます。 $V$ は可算集合としたので $V = V^+_1 + V^+_2 + \cdots$ とすることができます。

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

論理プログラミングの変数を含まないデータを定義します。

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

とします。

$\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$ 回で失敗

ということにします。

シークエント計算

これをシークエント計算に対応させます。

シークエント計算のデータ

論理プログラミングのデータからシークエント計算のデータを作ります。

各 $f \in F$ に対して $n = a_F(f)$ とするとき述語 $r_f(x_1, \cdots , x_n, y)$ を $P$ に追加します。すべての $r_f$ を $P$ に追加したものを $P'$ とおきます。

$C'_0 = C$ 、 $C'_{k+1} = C'_k + \{ f(c_1, \cdots , c_n) \mid f \in F_n; \ c_1, \cdots , c_n \in C'_k \}$ $(k = 0, 1, 2, \cdots)$ 、 $C' = C'_0 + C'_1 + C'_2 +\cdots$ とおきます。

$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$ に関数が現れないように変形することができます。すべての $v_f$ を $V$ に追加したものを $V'$ とおきます。

関数が現れないように変形した $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 D$ に対して $\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$ に現れるすべての変数とします。

すべての $c_1, \cdots , c_n \in C_k$ の組み合わせに対する $r_f(c_1, \cdots , c_n, f(c_1, \cdots , c_n))$ の全体を $r_1, \cdots , r_l$ とし、 $\bar{r}_k = r_1 \land \cdots \land r_l$ とおきます。

論理プログラミングが $n$ 回で成功するとするとき、適当な $C_\nu$ をとり $C_\nu = \{ c_1, c_2, \cdots , c_k \}$ とすると $\exists c_1 \exists c_2 \cdots \exists c_k ( \bar{r}_\nu \land \bar{p} \implies \bar{u} )$ を証明する図を書くことができます。

LK の記法を一部使って書きます。簡単に書くために $\bar{r}_\nu$ を $r$ と書きます。
$\hspace{4em} \begin{eqnarray*} & \vdash & \exists c_1 \exists c_2 \cdots \exists c_k ( r \land \bar{p} \implies \bar{u} ) \\ & \Uparrow & (右 \exists の繰り返し) \\ & \vdash & r \land \bar{p} \implies \bar{u} \\ & \Uparrow & (右 \implies) \\ r \land \bar{p} & \vdash & \bar{u} \\ & \Uparrow & (右 \exists の繰り返し) \\ r \land \bar{p} & \vdash & \bar{u}' \\ & \Uparrow & (左 \forall の繰り返し) \\ r \land \bar{p}' & \vdash & \bar{u}' \\ & \Uparrow & (左減少) \\ r \land \bar{p}' , r \land \bar{p}' & \vdash & \bar{u}' \\ & \Uparrow & (左 \land の繰り返し) \\ r , \bar{p}' & \vdash & \bar{u}' \\ \end{eqnarray*}$
ここで $\bar{p}'$ は $\bar{p}$ の先頭の $\forall$ をすべて取り除いたもの、 $\bar{u}'$ は $\bar{u}$ の先頭の $\exists$ をすべて取り除いたものとします。

簡単に書くために $\bar{p}'$ を $p$ 、 $\bar{u}'$ を $u$ と書きます。 $p = q_1 \land \cdots \land q_n$ のとき
$\hspace{4em} \begin{array}{c} r , q_1 \land \cdots \land q_n \vdash u \\ \Uparrow (左 \land の繰り返し) \\ ( 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$ のとき
$\hspace{4em} \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$ 回分となります(記法の説明は後述)。

$T' = V' + C'_\nu + F_0 +F_1 \times T' + F_2 \times {T'}^2 + \cdots$ (Prolog の項に対応)、
$S' = P'_0 + P'_1 \times T' + P'_2 \times {T'}^2 + \cdots$ (Prolog の述語の項に対応、 $P'_n$ は $P'$ の元のうちアリティが $n$ であるもの全体)、
$Q' = {S'}^* \times S$ (Prolog のホーン節に対応)、
$D' = {Q'}^*$ (Prolog のプログラムに対応)、
$Z = {S'}^* \times S$ ( $r \vdash u$ の形のシークエントを表す)、
$E' = S' \times S'$ ( $h \vdash u$ の形のシークエントを表す)、
$W = E' + S'$ ( $r \vdash u$ または $h \vdash u$ の形のシークエントを表す)

とします。

シークエント計算の推論ブロック

論理プログラミングの $1$ 回分に相当するシークエント計算の推論を推論ブロックと呼ぶことにします。

$\mathcal{F}(W)$ (シークエントで生成される半環を表す)の計算を考えます。

$\mathcal{F}(U)$ の加法を $\lor$ 、乗法を $\land$ 、 $\mathcal{F}(W)$ の加法を $\sqcup$ 、乗法を $\sqcap$ と書くことにします(上記の説明でこの記法を使っています)。

$\Gamma_{r}: D' \times S' \to \mathcal{F}(W)$ を以下の変換とします。
$\hspace{4em} \begin{array}{c} r , q_1 \land \cdots \land q_n \vdash u \\ \Uparrow (左 \land の繰り返し) \\ ( r , q_1 \vdash u ) \sqcup \cdots \sqcup ( r , q_n \vdash u ) \\ \end{array}$

$p \in D'$ に対して $\Delta_{r,p}: W \to \mathcal{F}(W)$ を以下の変換とします。
$\hspace{4em} \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}$

$p \in D'$ に対して $\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$ とします(論理プログラミングの場合と同様)。

シークエント計算の代入

$\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$ 回で失敗

ということにします。

論理プログラミングの $(p, x) \in D \times S$ に上記の変換をしたシークエント計算の $(p', x') \in D' \times S'$ を対応させることによって
$\bar{\sigma}(\rho_{\iota,E,0}^*(\delta_p^{*n}(x))) = 1 \iff \bar{\sigma}(\rho_{\iota,E',0}^*(\Delta_{r,p}^{*n}(x))) = 1$
となるので