アッカーマン関数が原始帰納的関数ではないことの証明
アッカーマン関数をA(m,n)と表記する
Theorem1 (以下T1)
f(x_1,\cdots,x_n)\le A(c, \max(x_1,\cdots,x_n))
補足
引数がない場合は、\max()=0とする
T1を使うことで、以下が示される
f(x)=A(x,x)が原始帰納的関数だと仮定すると
f(x)=A(x,x)\le A(c,\max(x))=A(c,x)が成り立つ
ここに、x=c+1を代入すれば、
A(c+1,c+1)\le A(c,c+1)となるが
Ackの補題L5よりに矛盾する
故に、アッカーマン関数は原始帰納的関数ではない
Ackの補題を用いて上のT1を証明する
以下の2つを示せばいい
①3つの初期関数が、T1を満たす
↓↓証明↓↓
①3つの初期関数が、T1を満たすことを示す
c=0とすればいずれも成り立つ
定数ゼロ関数について
任意のxについて、c_0(x)=0\lt A(0, x)=A(0,\max(0))になる
アッカーマン関数の取りうる最小値は1
後者関数について
s(x)=x+1= A(0, x)=A(0, \max(x))
射影関数について
u^{(n)}_i(x_1,\cdots,x_n)=x_i\lt A(0, x_i)\le A(0, \max(x_1,\cdots,x_n))
②-1 合成で得られる関数が、T1を満たすことを示す
具体的にはh, g_1,\cdots,g_mがT1を満たすとき、以下の関数fもT1を満たすことを示す
f(\vec{x})=h(g_1(\vec{x}), \cdots, g_m(\vec{x}))
m=0のとき
つまり、fの引数がなにもないとき
定義には書かれていないが、fは自然数上の関数なので何かしらの自然数dになる
f()=d\lt A(0,d)
=A(d, \max())
m\gt0のとき、c',c_1,\cdots,c_mを以下を満たす定数が存在する
A: h(\vec{y})\le A(c', \max(y))
Bi: g_i(\vec{x})\le A(c_i,\max(\vec{x}))
最初にh,g_1\cdots,g_mは満たすことを仮定しているからね
ここで、適当な定数cを選ぶと、以下の式が成り立つ
f(x)=h(g_1(\vec{x}),\cdots,g_m(\vec{x}))
\le A(c',\max\{g_1(\vec{x}),\cdots,g_m(\vec{x})\}) ∵A
従って、fはT1を満たす
②-2 原始帰納で得られる関数が、T1を満たすことを示す
具体的にはh,gがT1を満たすとき、以下の関数hもT1を満たすことを示す
f(0,\vec{y})=g(\vec{y})
f(x+1,\vec{y})=h(x,f(x,\vec{y}),\vec{y})
c_1,c_2を、以下を満たす定数とする
C: g(\vec{y})\le A(c_1,\max(\vec{y}))
D: h(x,u,\vec{y})\le A(c_2, \max\{x,u,\vec{y}\})
h,gがT1を満たすと仮定しているからね
また、c'を以下を満たす定数とする
E: 1\le c'
F: c_1\le c'
G: c_2\le c'-1
f(x,\vec{y})\le A(c', x+\max(\vec{y}))が成り立つことを、xに関する数学的帰納法で証明する
↑この式をHとする
x=0のとき
f(0,\vec{y})=g(\vec{y})
\lt A(c_1,\max(\vec{y})) ∵C
= A(c',0+\max(\vec{y}))
故に、x=0のとき、Hが成り立つ
あるxについて、Hが成り立つとすると
f(x+1,\vec{y})=h(x,f(x,\vec{y}), \vec{y})
\le A(c_2,\max\{x,f(x,\vec{y}),\vec{y}\}) ∵D
故に、x+1でもHが成り立つ
故に、全てのxに対し、Hが成り立つ
この時点では、Hが成り立つことは言えたが、fがT1を満たすことはまだ言えていない
従って適当な定数cに対し、以下の式が成り立つ
↓第2引数の大小比較に着目すればいい
f(x,\vec{y})\le A(c',x+\max(\vec{y})) ∵H
\le A(c', 2\max\{x,\vec{y}\}) ∵普通にa+b\le 2\max\{a,b\}
故にfはT1を満たす
↑↑証明終わり↑↑
参考
『計算可能性入門』 p.159~
親切でわかりやすい