Church–Turingのテーゼ

要点：どちらもステップ数についての帰納法で、各命令が次の様相を「命令の番号と 1 つのレジスタの中身」だけで決めることを使う。

整った形で計算できる部分関数の全体を $\mathcal{R}$ とする。$\mathcal{R}$ が基本関数を含み、合成・原始再帰・μ 作用素で閉じていることを示せば、μ再帰関数の全体はそのような集まりのうち最小のもの（μ再帰関数 の記事の定義「μ再帰関数」）なので、$\mathcal{R}$ に含まれる。
以下、部品となるプログラムが使うレジスタの番号の最大値と $k+1$ のどちらよりも大きい $N$ をとり、新しいレジスタは $N$ より大きい番号から選ぶ。部品 $G$ を「出力を $R_u$ に、入力 $i$ を $R_{v_i}$ に、そのほかの作業を $R_{W+i}$ に」置いて動かすとは、$\sigma(0)=u$、$\sigma(i)=v_i$（入力の番号 $i$）、$\sigma(i)=W+i$（それ以外の $i$）となる単射 $\sigma$ による付け替え $G^\sigma$ を動かすことをいう。$R_u$ と $R_{W+i}$ が $0$ の状態からこれを動かすと、lem-ctt-compose の 2 と $G$ が整った形で計算することにより、$G$ の値が定義されるなら停止して $R_u$ に値が入り、入力の箱は元のまま、$R_{W+i}$ は $0$ に戻り、$\sigma$ の像の外の箱は変わらない。値が定義されなければ停止しない。
基本関数． ゼロ関数 $Z$ は長さ $0$ のプログラム（初期様相がすでに停止様相）が整った形で計算する。後者関数 $S$ は $\mathrm{CPY}(1,0;2);\mathrm{INC}(0,1)$（最後の命令は長さ $1$ のプログラム）が、射影 $P^k_i$ は $\mathrm{CPY}(i,0;k+1)$ が整った形で計算する。
合成． $f(\vec x)\simeq g(h_1(\vec x),\dots,h_m(\vec x))$ とし、$g$ を $G$ が、$h_j$ を $H_j$ が整った形で計算するとする。$c_j:=N+j$（$1\le j\le m$）、$W:=N+m$ とおき、次のプログラムを考える。

1. $j=1,\dots,m$ の順に、$H_j$ を「出力を $R_{c_j}$ に、入力 $i$ を $R_i$ に、作業を $R_{W+i}$ に」置いて動かす。
2. $G$ を「出力を $R_0$ に、入力 $j$ を $R_{c_j}$ に、作業を $R_{W+i}$ に」置いて動かす。
3. $\mathrm{CLR}(c_1);\dots;\mathrm{CLR}(c_m)$。
   初期様相では $R_1,\dots,R_k$ に $\vec x$ が入り、ほかは $0$ である。ある $h_j(\vec x)$ が定義されなければ、それより前の段は停止し、段 1 の $j$ 番目で停止しない。このとき $f(\vec x)$ も定義されない。すべての $h_j(\vec x)=y_j$ が定義されるなら、段 1 の後 $R_{c_j}=y_j$、入力は元のまま、作業の箱は $0$ である。$g(\vec y)$ が定義されなければ段 2 で停止せず、$f(\vec x)$ も定義されない。定義されるなら段 2 の後 $R_0=g(\vec y)=f(\vec x)$ で、段 3 で $R_{c_j}$ を空にすると、整った形の停止様相になる。

原始再帰． $f(\vec x,0)\simeq g(\vec x)$、$f(\vec x,y+1)\simeq h(\vec x,y,f(\vec x,y))$ とし、$g$ を $G$ が、$h$ を $H$ が整った形で計算するとする。入力は $R_1,\dots,R_k$ に $\vec x$、$R_{k+1}$ に $y$ である。$a,c,d,b,t$ を $N+1,\dots,N+5$、$W:=N+5$ とおき、次のように動くプログラムを組む。

1. $G$ を「出力を $R_a$ に、入力 $i$ を $R_i$ に」置いて動かし、$\mathrm{CPY}(k+1,d;t)$ を実行する。
2. （ループの先頭）$\mathrm{DEC}(d,\cdot,\cdot)$ で、$R_d>0$ なら $1$ を引いて 3 へ、$R_d=0$ なら 4 へ進む。
3. $H$ を「出力を $R_b$ に、入力 $i\le k$ を $R_i$ に、入力 $k+1$ を $R_c$ に、入力 $k+2$ を $R_a$ に」置いて動かし、$\mathrm{CLR}(a);\mathrm{MOV}(b,a)$ を実行し、$R_c$ に $1$ を足して 2 へ戻る。
4. $\mathrm{MOV}(a,0);\mathrm{CLR}(c)$ を実行して停止する。
   組み立て方は連結と同じで、段 3 の最後の行き先だけを段 2 の命令の番号に替える。lem-ctt-compose の 2・3 により、各部品は単独で動かしたのと同じ変化をし、停止したら指定した次の命令へ進む（下の μ 作用素の組み立ても同じである）。$f(\vec x,y)$ が定義されるときは、段 2 に $i$ 回目に来たとき（$0\le i\le y$）、$R_c=i$、$R_d=y-i$、$R_a=f(\vec x,i)$ で、$R_b$、$R_t$、作業の箱は $0$ である。これは $i$ についての帰納法で確かめられる（$i\to i+1$ では段 3 が $R_a$ を $h(\vec x,i,f(\vec x,i))=f(\vec x,i+1)$ に替え、$R_c$ を $1$ 増やす）。$i=y$ で $R_d=0$ となり、段 4 で $R_0=f(\vec x,y)$ となって整った形で停止する。$f(\vec x,y)$ が定義されないときは、$f(\vec x,i)$ が定義されない最小の $i\le y$ があり、$i=0$ なら段 1 の $G$ が、$i\ge1$ なら $i$ 回目の段 3 の $H$ が停止しない。パラメータのない原始再帰（$f(0)=a_0$）では、段 1 の $G$ の代わりに $\mathrm{INC}(a,\cdot)$ を $a_0$ 回並べる。

μ 作用素． $f(\vec x)\simeq\mu y\,[g(\vec x,y)=0]$ とし、$g$ を $G$ が整った形で計算するとする。$c:=N+1$、$b:=N+2$、$W:=N+2$ とおく。

1. （ループの先頭）$G$ を「出力を $R_b$ に、入力 $i\le k$ を $R_i$ に、入力 $k+1$ を $R_c$ に」置いて動かす。
2. $\mathrm{DEC}(b,\cdot,\cdot)$ で、$R_b>0$ なら 3 へ、$R_b=0$ なら 4 へ進む。
3. $\mathrm{CLR}(b)$ を実行し、$R_c$ に $1$ を足して 1 へ戻る。
4. $\mathrm{MOV}(c,0)$ を実行して停止する。
   段 1 に $z$ 回目に来たとき、$R_c=z$、$R_b=0$ で、すべての $z'< z$ について $g(\vec x,z')$ は定義されて $0$ でない（$z$ についての帰納法）。$g(\vec x,z)$ が定義されなければ段 1 で停止しない。このとき $\mu y$ の定義により $f(\vec x)$ も定義されない。$g(\vec x,z)=0$ なら段 4 で $R_0=z=f(\vec x)$ となり、$R_b=R_c=0$ で整った形で停止する。$g(\vec x,z)>0$ なら段 3 を経て $z+1$ 回目に進む。$g(\vec x,y)=0$ となる $y$ がなく、すべて定義されるなら、ループは止まらず、$f(\vec x)$ も定義されない。$\square$

長さ $n$ のプログラム $P$ が $f\colon\mathbb{N}^k\rightharpoonup\mathbb{N}$ を計算するとする。$P$ に現れるレジスタの番号と $k$ より大きい $m$ をとる。$R_i$（$i\ge m$）は $P$ に現れず、初期様相で $0$ なので、計算の間ずっと $0$ のままである。そこで様相 $(\ell,\rho)$ を
$$ \ulcorner\ell,\rho\urcorner:=\langle\ell,\rho(0),\rho(1),\dots,\rho(m-1)\rangle $$
で表す。
段 1（1 段の変化）． 列の符号 $c$ の $i$ 番目の項を $v$ に替える関数 $\mathrm{rep}(c,i,v):=\bigl\lfloor c/p(i)^{(c)_i+1}\bigr\rfloor\cdot p(i)^{v+1}$ は原始再帰関数である（商 $\lfloor a/b\rfloor$ は有界最小化 $\mu q< a+1\,[\,(q+1)\cdot b>a\,]$ で書ける。原始再帰関数 の記事の命題「有界な和・積・量化・最小化」）。$\mathrm{St}(c)$ を次の場合分けで定める。

• $(c)_0\ge n$ なら $\mathrm{St}(c):=c$。
• $(c)_0=\ell< n$、$I_\ell=\mathrm{INC}(r,j)$ なら $\mathrm{St}(c):=\mathrm{rep}\bigl(\mathrm{rep}(c,r+1,(c)_{r+1}+1),0,j\bigr)$。
• $(c)_0=\ell< n$、$I_\ell=\mathrm{DEC}(r,j,j')$ なら、$(c)_{r+1}>0$ のとき $\mathrm{St}(c):=\mathrm{rep}\bigl(\mathrm{rep}(c,r+1,(c)_{r+1}\mathbin{\dot-}1),0,j\bigr)$、$(c)_{r+1}=0$ のとき $\mathrm{St}(c):=\mathrm{rep}(c,0,j')$。
  $P$ は固定されているので場合は有限個であり、同じ命題の場合分けを有限回使えば $\mathrm{St}$ は原始再帰関数である。定義から、停止様相でない $(\ell,\rho)$ について $\mathrm{St}(\ulcorner\ell,\rho\urcorner)$ は次の様相の符号であり、停止様相の符号は $\mathrm{St}$ で動かない。

段 2（計算をなぞる）． 原始再帰で
$$ \mathrm{cf}(\vec x,0):=\langle0,0,x_1,\dots,x_k,0,\dots,0\rangle,\qquad\mathrm{cf}(\vec x,s+1):=\mathrm{St}(\mathrm{cf}(\vec x,s)) $$
と定める（右辺の列の長さは $m+1$）。$\mathrm{cf}$ は原始再帰関数である。$\mathrm{cf}(\vec x,0)=\ulcorner0,\rho_{\vec x}\urcorner$ であり、段 1 と $s$ についての帰納法により、$P$ の $(0,\rho_{\vec x})$ からの計算の $s$ 番目の様相 $C_s$ が存在すれば $\mathrm{cf}(\vec x,s)$ はその符号であり、計算が $t\le s$ 番目で停止様相に達していれば $\mathrm{cf}(\vec x,s)=\mathrm{cf}(\vec x,t)$ である。
段 3（停止を探す）．
$$ f(\vec x)\simeq\Bigl(\mathrm{cf}\bigl(\vec x,\ \mu s\,[\,(\mathrm{cf}(\vec x,s))_0=n\,]\bigr)\Bigr)_1 $$
を示す。$f(\vec x)$ が定義されるなら、$P$ は停止し、最初に停止様相に達する番号を $t$ とすると、$s< t$ では $(\mathrm{cf}(\vec x,s))_0< n$、$s=t$ では $(\mathrm{cf}(\vec x,t))_0=n$ なので $\mu s$ の値は $t$ であり、右辺は停止様相の $R_0$ の中身 $f(\vec x)$ である。$f(\vec x)$ が定義されないなら $P$ は停止せず、どの $s$ でも $(\mathrm{cf}(\vec x,s))_0< n$ なので右辺は定義されない。μ 作用素を施す関数 $\lvert(\mathrm{cf}(\vec x,s))_0-n\rvert$ は全域的な原始再帰関数なので、右辺は μ再帰関数である。$\square$

1 ⇒ 2 は thm-ctt-mu-to-rm、2 ⇒ 1 は thm-ctt-rm-to-mu である。$\square$