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

証明図を遡る説明のとき、成功の場合を含めるのか含めないのか明言していませんでしたが、実質は証明が成功でも失敗でもないときの極限となっていました。証明図の極限を考えることが目的だったのですが、証明図が書けないときの極限になっているというのではここに書いてきた一連のことは意味がわからなくなってしまうという問題があります。有限の文字列を切り詰める写像による射影的極限によって無限の文字列を考えることができるのと同様、証明図を証明図に切り詰めることができれば上記の問題は解決できると考えられます。以下ではこの方向で考えていきます。

PLP のプログラムが成功して結果として有限のリストが得られる場合を考えます。このプログラムに対応する変数を含まない証明図を考えると、結論となるシークエント式には有限のリストが現れるものとなります。このリストが $n$ 項のリストである場合、 $m$ 項( $n \ge m$ )のリストが現れる証明図との関係はどうなるのか考えていきます。

以下のホーン節の和を $\gamma$ とおきます。
$rep(0, X, []).$
$rep(\sigma(n), X, [X|L]) \mathop{:-} rep(n, X, L).$
$rep_a(n, L) \mathop{:-} rep(n, a, L).$
このようにおくと $rep_a$ は $rep_a(n, [ \underbrace{ a, \cdots , a }_n ])$ が成り立つような述語となります。 $n$ は自然数で PLP では自然数は $\sigma(\sigma(\cdots(0)\cdots))$ のように $0$ と $n$ 個の $\sigma$ で表されているとします。

$\gamma$ に対応する証明図の逆方向の写像を $\bar{\delta}_d$ とします。 $\gamma \vdash rep_a(n, [ \underbrace{ a, \cdots , a }_n ])$ を $s_n$ とおくと $\sum \bar{\delta}_d^n(s_n) = 1$ が成り立ちます。 $n \ge m$ として $\gamma \vdash rep_a(m, [ \underbrace{ a, \cdots , a }_m ])$ を $s_m$ とおくと $\sum \bar{\delta}_d^m(s_m) = 1$ が成り立ちます。証明図を切り詰める写像を考えるために、まずは $f_{nm}(s_n) = s_m$ となる写像 $f_{nm}: \bar{S} \to \bar{S}$ を考えていきます。