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

$\gamma$ に対応する $d \in D$ で決まる証明図の逆方向の写像を $\bar{\delta}_d : \bar{L} \to P(\bar{L})$ とします。

$\overleftarrow{\gamma} : P(\bar{L}) \to P(\bar{L})$ を $\overleftarrow{\gamma}(X) = \bigcup_{x \in X} \bar{\delta}_d(x)$ と定義します。これは証明図の逆方向の写像となります。

$\overrightarrow{\gamma} : P(\bar{L}) \to P(\bar{L})$ を $\overrightarrow{\gamma}(Y) = \{ x \in \bar{S} | \bar{\delta}_d(x) \subseteq Y \}$ と定義します。これは証明図の方向の写像となります。

$s_n \in \bar{S}$ を $1 \in \overleftarrow{\gamma}^n(\{ s_n \})$ を満たすものとします。 $m \le n$ として $s_n$ を $\overrightarrow{\gamma}^m(\{ 1 \})$ の元 $s_m$ に変換する(切り詰める)ことを考えます。 $\overrightarrow{\gamma}^m(\{ 1 \})$ の元が一つだけのときは決まりますが、複数ある場合は $s_n$ に最も近いものをとることができるのかを調べていきます。

図で書くと以下のような状況です。右方向が証明図の方向です。

$\require{AMScd} \begin{CD} P(\bar{L}) @< \overleftarrow{\gamma}^{n-m} << P(\bar{L}) @< \overleftarrow{\gamma}^{m} << P(\bar{L}) \\ @V f_n VV @V f_m VV @VV f_0 V \\ P(\bar{L}) @>> \overrightarrow{\gamma}^{n-m} > P(\bar{L}) @>> \overrightarrow{\gamma}^{m} > P(\bar{L}) \end{CD}$

$L$ は $\xi \vdash \eta$ の形のもの(シークエント)の全体で自由生成された $0$ と $1$ を含む可換半環で $1 + x = x + 1 = 1$ を満たすものでした。しかし $0$ と $1$ の扱い方をどうするかはっきり決めていませんでした。 $L$ の元の標準形をどうするか考えてみます。 $L$ の元は以下の「選言標準形」にすることができます。
$\begin{array}{cc} & x_{11} x_{12} \cdots x_{1l_1} \\ + & x_{21} x_{22} \cdots x_{2l_2} \\ + & \\ & \vdots \\ + & x_{k1} x_{k2} \cdots x_{kl_k} \end{array}$
ここでそれぞれの $x_{ij}$ はシークエントです。まず $0x = x0 = 0$ と $1x = x1 = x$ によって各行は

$0$
$1$
$0$ も $1$ も含まない式

のどれかにすることができます。この結果に対して $0+x = x+0 = x$ と $1+x = x+1 = 1$ を使うことによって

$0$
$1$
$0$ も $1$ も含まない選言標準形

のどれかにすることができます。これを $L$ の元の標準形とします。]

$x \in \bar{L}$ と $d \in \bar{D}$ に対して $\delta_d: \bar{L} \to \bar{L}$ を以下のように定義します。

$\delta_d(0) = 0$
$\delta_d(1) = 1$
$0$ でも $1$ でもない場合は標準形の各シークエント $x_{ij}$ を $\delta_d(x_{ij})$ に変換したものの標準形

$x \in \bar{L}$ と $d \in D$ に対して $\bar{\delta}_d: \bar{L} \to P(\bar{L})$ を $\bar{\delta}_d(x)$ は $d$ の変数に変数を含まない項を代入したもの全体の集合と定義します。

まず $\gamma$ がホーン節
$\begin{array}{lll} rep(0, []). \\ rep(\sigma(N), [a|L]) & \mathop{:-} & rep(N, L). \end{array}$
の和であるとき(大文字で始まるものが変数)、 $\gamma \vdash rep(n, [ \underbrace{ a, \cdots , a }_n ])$ を $s_n$ とおくと $1 \in \overleftarrow{\gamma}^n(\{ s_n \})$ が成り立つことを見ていきます。 $[ \underbrace{ a, \cdots , a }_n ]$ を $[ a ] ^n$ と書くことにします。

$\bar{\delta}_d(\gamma \vdash x)$ は
$\begin{array}{lll} & (x \equiv rep(0, [])) \\ + & (x \equiv rep(\sigma(N), [a|L])) & (\gamma \vdash rep(N, L)) \end{array}$
の変数に変数を含まない項を代入したもの全体の集合になります。ここで同じ行にある同じ名前の変数には同じ項を代入します。したがってすべての変数を変数を含まない項に変更したときにも成功となるか失敗となるかという結果には影響を与えないということが言えます。 $x \equiv y$ は $x$ と $y$ が一致するとき $0$ 、一致しないとき $1$ となります。変数を含まない $x$ と $y$ に対して $x \equiv y$ は $0$ または $1$ となります。

以下 $x \equiv y$ が $0$ となる行は省略して書くことにします。また、関係のない行の変数は変数のまま書くことにします。これは変数に変数を含まない項を代入したものすべての和を表すものとします。

$\bar{\delta}_d(\gamma \vdash rep(0, [ ] ))$ は
$\begin{array}{lll} & (rep(0, [ ] ) \equiv rep(0, [])) \\ + & (rep(0, [ ] ) \equiv rep(\sigma(N), [a|L])) & (\gamma \vdash rep(N, L)) \end{array}$
を元として持つことがわかります。1行目は $1$ となるので $1 \in \bar{\delta}_d(\gamma \vdash rep(0, [ ] ))$ となります。

$\bar{\delta}_d(\gamma \vdash rep(\sigma(0), [a] ))$ は
$\begin{array}{lll} & (rep(\sigma(0), [a] ) \equiv rep(0, [])) \\ + & (rep(\sigma(0), [a] ) \equiv rep(\sigma(0), [a])) & (\gamma \vdash rep(0, [])) \end{array}$
を元として持つことがわかります。 $1 \in \bar{\delta}_d(\gamma \vdash rep(0, [ ] ))$ であったので $1 \in \bar{\delta}_d^2(\gamma \vdash rep(\sigma(0), [a] ))$ となります。

$1 \in \bar{\delta}_d^n(\gamma \vdash rep(n, [a]^n ))$ と仮定します。

$\bar{\delta}_d(\gamma \vdash rep(\sigma(n), [a|[a]^n] ))$ は
$\begin{array}{lll} & (rep(\sigma(n), [a|[a]^n]) \equiv rep(0, [])) \\ + & (rep(\sigma(n), [a|[a]^n]) \equiv rep(\sigma(n), [a|[a]^n]) & (\gamma \vdash rep(n, [a]^n)) \end{array}$
を元として持つことがわかります。仮定より $1 \in \bar{\delta}_d^n(\gamma \vdash rep(n, [a]^n ))$ であったので $1 \in \bar{\delta}_d^{n+1}(\gamma \vdash rep(\sigma(n), [a|[a]^n] ))$ すなわち $1 \in \bar{\delta}_d^{n+1}(\gamma \vdash rep(n+1, [a]^{n+1} ))$ となります。

以上の議論から帰納法によりすべての自然数 $n$ に対して $1 \in \bar{\delta}_d^n(\gamma \vdash rep(n, [a]^n ))$ であることがわかります。

次に $\bar{\delta}_d^n(\gamma \vdash rep(n+1, [a]^{n+1} ))$ を考えます。この式の標準形は $\gamma \vdash rep(1, [a])$ というシークエントを含むので、それを $1$ に変換すると証明図を切り詰めることができます。(どうすれば良いか？)