エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

半環上のフラクタル代数(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
となるので

  • 論理プログラミングが  n 回で成功  \iff シークエント計算は  n 回で成功
  • 論理プログラミングが  n 回で失敗  \iff シークエント計算は  n 回で失敗

が成り立ちます。シークエント計算が  n 回で失敗のとき、否定を表す図を書くことができます。

この項は以前書いたものを修正したものです。定数に必要なものをすべて付け加えれば良いと書いていたのに付け加えていなかった点を修正しました。ただしすべて付け加えると無限になってしまって、何も条件のない論理式として書くことができないので、個々の場合に分けて有限個で書くようにしています。

他にも間違っているところがあるかもしれないので、後で検討します。

その前に、この議論は書き方が複雑すぎるので、式を簡単に書くためにPrologのような書き方で書く方法について検討します。