Gödel 符号化と有限列 | 数理論理

1 Cantor の対関数

定義 1.1 (Cantor の対関数). $a,b\in\mathbb N$ に対して

\operatorname{pair}(a,b) =\frac{(a+b)(a+b+1)}2+b

と定める。この関数を Cantor の対関数 (Cantor pairing function) という。 $\operatorname{left}(z)$ と $\operatorname{right}(z)$ は

\operatorname{pair}(\operatorname{left}(z),\operatorname{right}(z))=z

を満たす二つの成分とする。

補題 1.2. $\operatorname{pair}\colon\mathbb N^2\to\mathbb N$ は全単射である。 $\operatorname{pair}$ 、 $\operatorname{left}$ 、 $\operatorname{right}$ は正のアリティをもつ原始再帰全関数であり、

\operatorname{left}(\operatorname{pair}(a,b))=a, \qquad \operatorname{right}(\operatorname{pair}(a,b))=b

が成り立つ。

証明. $w=a+b$ とおき、三角数 $T_w=w(w+1)/2$ と書けば $\operatorname{pair}(a,b)=T_w+b$ である。 $0\le b\le w$ なので、和が $w$ である対は

T_w,T_w+1,\ldots,T_w+w=T_{w+1}-1

へ、 $b$ の順に重複なく写る。これらの区間は $w=0,1,\ldots$ の順に隣接し、 $\mathbb N$ を尽くす。したがって各 $z$ はただ一つの $w$ と $b\le w$ をもち、 $z=T_w+b$ と書くことができる。 $a=w-b$ とすれば全単射性を得る。

加法、乗法、固定数 $2$ による商は原始再帰的なので $\operatorname{pair}$ は原始再帰的である。 $\operatorname{pair}(a,b)=z$ なら $a,b\le z$ である。したがって $0\le a,b\le z$ の範囲で等式を満たす唯一の対を有界探索すればよい。有界探索と有限の場合分けは原始再帰的なので、二成分を返す $\operatorname{left}$ と $\operatorname{right}$ も原始再帰全関数である。▨

2 すべての自然数を有限列として読む

定義 2.1 (Cons による有限列符号).

\begin{aligned} \operatorname{Empty}&=0,\\ \operatorname{Cons}(a,t)&=1+\operatorname{pair}(a,t),\\ \operatorname{SeqCode}(a_0,\ldots,a_{n-1}) &=\operatorname{Cons}(a_0, \operatorname{Cons}(a_1,\ldots, \operatorname{Cons}(a_{n-1},0)\ldots)). \end{aligned}

この符号化を Cons 有限列符号 (Cons finite-sequence coding) という。

$s>0$ では

\operatorname{Head}(s)=\operatorname{left}(s-1), \qquad \operatorname{Tail}(s)=\operatorname{right}(s-1)

とし、 $\operatorname{Head}(0)=\operatorname{Tail}(0)=0$ とする。

前者関数 $s\mathbin{\dot-}1$ と零判定による場合分けを用いれば、 $\operatorname{Head}$ と $\operatorname{Tail}$ は全域原始再帰関数である。

命題 2.2. $s>0$ なら $\operatorname{Tail}(s)<s$ である。したがって、任意の自然数 $s$ から $\operatorname{Tail}$ を反復すると有限回で $0$ に到達し、 $s$ はただ一つの有限列へ復号される。ゆえに符号述語 $\operatorname{Seq}(s)$ は常に真である一変数原始再帰関係とすることができ、bad code は存在しない。

証明. $s>0$ とし、 $a=\operatorname{Head}(s)$ 、 $t=\operatorname{Tail}(s)$ とおく。対関数の逆の定義により $s=1+\operatorname{pair}(a,t)$ である。 $\operatorname{pair}(a,t)=T_{a+t}+t\ge t$ なので $t<s$ である。

$s$ から始めて $s,\operatorname{Tail}(s),\operatorname{Tail}^2(s),\ldots$ と進むと、正である間は自然数が真に減少する。自然数の真の降下列は有限なので、 $\operatorname{Tail}^n(s)=0$ を満たす非負整数 $n$ が存在する。各正の符号に対する Head と Tail は対関数の全単射性から一意であるため、復号列も一意である。恒真関係の特性関数は単項定数関数 $C_1(s)=1$ であり、初期関数から合成で構成することができる。零項関係を追加する必要はない。▨

3 コース再帰を通常の原始再帰へ還元する

値 $F(s)$ を、それより小さい引数での値から定める再帰をコース再帰という。ここでは必要な過去の値を右入れ子の履歴へ保存し、通常の原始再帰だけで実行する。

補題 3.1. $D(\vec x,s)<s$ が $s>0$ で成り立つ原始再帰関数 $D$ と、原始再帰関数 $B(\vec x)$ 、 $G(\vec x,s,u)$ を考える。

F(\vec x,0)=B(\vec x), \qquad F(\vec x,s)=G(\vec x,s,F(\vec x,D(\vec x,s)))\quad(s>0)

で定まる $F$ は原始再帰全関数である。パラメータ列 $\vec x$ は空でもよい。空の場合にも $F$ は再帰引数 $s$ を残す一変数関数であり、零項関数にはならない。

証明. 最初に履歴から第 $j$ 成分を取る補助関数を作る。

\begin{aligned} I(t,0)&=t,\\ I(t,j+1)&=\operatorname{Tail}(I(t,j)),\\ E(t,j)&=\operatorname{Head}(I(t,j)). \end{aligned}

$I$ は $j$ に関する通常の原始再帰であり、 $E$ は合成なので、ともに原始再帰的である。

$H(\vec x,n)$ を、先頭から $F(\vec x,n-1),\ldots,F(\vec x,0)$ を並べた逆向きの履歴符号とする。 $H$ を次の通常の原始再帰で同時に構成する。

\begin{aligned} H(\vec x,0)&=0,\\ H(\vec x,n+1)&=\operatorname{Cons}(V(\vec x,n),H(\vec x,n)), \end{aligned}

ここで

V(\vec x,0)=B(\vec x),

$n>0$ では

V(\vec x,n)= G\bigl(\vec x,n, E(H(\vec x,n),n-1-D(\vec x,n))\bigr)

とする。条件 $D(\vec x,n)<n$ により添字は自然数である。切捨て減法と零判定による場合分けを用いれば $V$ の右辺は原始再帰関数の合成である。したがって $H$ は通常の原始再帰によって得る。

$n$ に関するメタ理論の帰納法により、 $H(\vec x,n)$ の第 $n-1-d$ 成分は $F(\vec x,d)$ であることが分かる。特に $d=D(\vec x,n)$ とすれば、 $V(\vec x,n)$ は定義式どおり $F(\vec x,n)$ になる。よって

F(\vec x,n)=E(H(\vec x,n+1),0)

であり、 $F$ は原始再帰的である。用いた再帰はすべて通常の原始再帰であり、 $\vec x$ が空のときは基底値 $B=c$ を一つの自然数として指定する規約に従う。▨

一つの小さい引数の値だけを読む前補題では、二つの直下構文の値を同時に必要とする再帰や、再帰呼出しごとに環境を更新する再帰を直接扱うことができない。次の有限スタック・接頭トレースによる還元を用いる。

補題 3.2. $K$ を固定した標準自然数とする。要求 $q$ に対して、階数 $r(q)$ 、子の個数 $m(q)\le K$ 、 $j<m(q)$ に対する第 $j$ 子 $d(q,j)$ 、および子の値の有限列 $h$ から親の値を返す $C(q,h)$ が原始再帰関数であるとする。すべての実際の子について

r(d(q,j))<r(q)\qquad(j<m(q))

が成り立つなら、各子を左から評価して $C$ へ渡す有限分岐コース再帰の値 $\operatorname{Eval}(q)$ は原始再帰全関数である。要求 $q$ は、主引数だけでなく、種類タグ、補助パラメータ、および子へ渡す更新済み有限環境を含んでよい。

証明. 要求、未処理の子の位置をもつ継続枠、および計算済みの値を、それぞれ固定タグを先頭にもつ

\operatorname{Req}(q),\qquad \operatorname{Frame}(q,j,h),\qquad \operatorname{Val}(a)

という固定長列で符号化する。計算状態は、これらを上端から並べた有限スタックとする。子の値は逆順の列 $h$ へ保存し、 $C$ が Entry により左からの順序へ読み直す規約を固定する。

一段遷移 Step を次のように定める。上端が Req $(q)$ で $m(q)=0$ なら、これを Val $(C(q,0))$ へ置き換える。 $m(q)>0$ なら、Req $(q)$ を

\operatorname{Req}(d(q,0)),\quad \operatorname{Frame}(q,1,0)

へ置き換える。上端二要素が Val $(a)$ 、Frame $(q,j,h)$ なら、 $a$ を $h$ の先頭へ追加する。 $j<m(q)$ なら次に Req $(d(q,j))$ と Frame $(q,j+1,\operatorname{Cons}(a,h))$ を積み、 $j=m(q)$ なら両要素を Val $(C(q,\operatorname{Cons}(a,h)))$ へ置き換える。スタックが一要素 Val $(a)$ だけになった停止状態では Step を恒等写像とし、不正な状態の値も $0$ への場合分けによって固定する。タグ照合、Head、Tail、Entry、Cons、有界比較、および $r,m,d,C$ だけを用いるため、Step は原始再帰的である。

停止までの一様な原始再帰的上界を与える。次の関数を通常の原始再帰で定める。

N_K(0)=1,\qquad N_K(s+1)=1+K\,N_K(s).

階数が $s$ 以下の一要求から展開される要求木の節点数は、 $s$ に関するメタ理論の帰納法により $N_K(s)$ 以下である。各節点は一度だけ Req として展開され、各辺は子の値を親の Frame へ戻すときに一度だけ処理される。したがって $3N_K(r(q))$ 回の遷移後には必ず停止状態にある。

開始状態とその接頭トレースを

\begin{aligned} R(q,0)&=\operatorname{SeqCode}(\operatorname{Req}(q)),\\ R(q,n+1)&=\operatorname{Step}(R(q,n)) \end{aligned}

と通常の原始再帰で定める。 $R(q,3N_K(r(q)))$ の唯一の Val の成分を取り出す関数は、合成により原始再帰的である。これを $\operatorname{Eval}(q)$ とする。

正しさは階数に関するメタ理論の帰納法で示す。階数 $0$ の要求は子をもたず、最初の遷移で $C(q,0)$ を返す。階数 $s+1$ では各子の階数が $s+1$ より小さいため、帰納法の仮定により各 Req は定義どおりの値を Val として返す。Frame は返った値を左から漏れなく逆順列へ保存するので、最後に $C$ が受け取る値列は定義されたすべての子の値である。要求に含めた環境やほかの補助パラメータは $d(q,j)$ が子ごとに自由に更新することができる。この証明で用いた対象言語上の再帰は、接頭長 $n$ に関する $R$ と上界 $N_K$ の通常の原始再帰だけである。▨

4 長さ、成分取得、連結

定義 4.1 (有限列の全域操作).

\begin{aligned} \operatorname{Len}(0)&=0,\\ \operatorname{Len}(\operatorname{Cons}(a,t))&=1+\operatorname{Len}(t),\\[2mm] \operatorname{Entry}(\operatorname{Cons}(a,t),0)&=a,\\ \operatorname{Entry}(\operatorname{Cons}(a,t),i+1)&=\operatorname{Entry}(t,i),\\[2mm] \operatorname{Concat}(0,t)&=t,\\ \operatorname{Concat}(\operatorname{Cons}(a,s),t) &=\operatorname{Cons}(a,\operatorname{Concat}(s,t)). \end{aligned}

$\operatorname{Len}$ 、 $\operatorname{Entry}$ 、 $\operatorname{Concat}$ をそれぞれ長さ関数 (length function)、成分取得関数 (entry function)、連結関数 (concatenation function) という。

空列に対して $\operatorname{Entry}(0,i)=0$ とする。したがって、列の長さ以上の添字に対する値も $0$ である。

定理 4.2. $\operatorname{Head}$ 、 $\operatorname{Tail}$ 、 $\operatorname{Len}$ 、 $\operatorname{Entry}$ 、 $\operatorname{Concat}$ は正のアリティをもつ原始再帰全関数である。

証明. Head と Tail の原始再帰性は補題 1.2と零判定による場合分けから既に従う。 Len は

\operatorname{Len}(s)= \begin{cases} 0&(s=0),\\ 1+\operatorname{Len}(\operatorname{Tail}(s))&(s>0) \end{cases}

というコース再帰であり、 $s>0$ では $\operatorname{Tail}(s)<s$ である。補題 3.1を適用して原始再帰性を得る。

成分取得について、反復尾 $I$ を同補題の証明と同じ通常の原始再帰で定めると

\operatorname{Entry}(s,i)=\operatorname{Head}(I(s,i))

である。したがって Entry は原始再帰的である。 $i\ge\operatorname{Len}(s)$ なら反復尾は既に $0$ へ達し、その後も $0$ にとどまるので範囲外の値は $0$ になる。

$t$ をパラメータとして、Concat は第1引数 $s$ に関するコース再帰

C(t,0)=t, \qquad C(t,s)=\operatorname{Cons}(\operatorname{Head}(s),C(t,\operatorname{Tail}(s)))\quad(s>0)

である。再び Tail の真の減少と補題 3.1を用いれば $C(t,s)$ は原始再帰的であり、 $\operatorname{Concat}(s,t)=C(t,s)$ は射影の交換との合成で得る。各構成は全域関数からの合成と通常の原始再帰だけを用いるので、すべて全域である。▨

例 4.3 (復号と連結). $c=\operatorname{SeqCode}(4,1,7)$ とすると

\operatorname{Len}(c)=3, \quad \operatorname{Entry}(c,0)=4, \quad \operatorname{Entry}(c,2)=7, \quad \operatorname{Entry}(c,5)=0.

$d=\operatorname{SeqCode}(2,8)$ なら $\operatorname{Concat}(c,d)=\operatorname{SeqCode}(4,1,7,2,8)$ である。

注意 4.4 (下流で符号を変更しない). 以後、自然数上の有限列には、本記事で定めた右入れ子の Cons 符号と Len、Entry、Concat を用いる。下流でこの符号を算術式によって表す場合にも外側の符号値を維持する。素因数分解符号または β 関数へ取り替えると、構文符号、計算列、証明列の数詞が一致しなくなるため、別の符号を併用しない。

5 演習

問題 5.1.

$\operatorname{Tail}(s)<s$ がすべての自然数の有限復号を保証する理由を説明せよ。
補題 3.1で履歴を逆向きに保存した理由を説明せよ。
Entry が範囲外で $0$ を返すことを、反復尾 $I$ から証明せよ。
補題 3.2で $3N_K(r(q))$ 回の遷移が停止の上界になる理由を説明せよ。

解答 (確認問題の解答).

正の符号で Tail を取るたびに自然数が真に減少し、自然数には無限の真の降下列がないからである。
段階 $n$ で既に計算した $F(0),\ldots,F(n-1)$ のうち、 $F(d)$ を先頭から $n-1-d$ 回の Tail で取り出せるようにするためである。
$i\ge\operatorname{Len}(s)$ では $I(s,i)=0$ である。Tail(0)=0 なので以後も 0 にとどまり、Head(0)=0 から Entry(s,i)=0 となる。
階数が $s$ 以下の要求木の節点数は $N_K(s)$ 以下である。各節点の要求展開と各辺から親への値の返却を数えると、各節点につき三回以内の遷移で処理することができるためである。

▨

§E16.17Gödel 符号化と有限列

1 Cantor の対関数

2 すべての自然数を有限列として読む

3 コース再帰を通常の原始再帰へ還元する

4 長さ、成分取得、連結

5 演習

参考文献

前提記事