Ackermann関数は原始再帰的ではない
参考文献
1. 0変数関数$ Z() = 0
2. 後者関数$ S(x) = x+1
3. 射影関数$ \mathrm{proj}^n_i(x_1,\dots,x_n) = x_i
4. 関数$ f_1,\dots,f_m:\N^n \to \Nと関数$ g:\N^m \to \Nの合成関数$ \mathrm{comp}_{f_1,\dots,f_m,g}(\vec{x}) = g(f_1(\vec{x}),\dots,f_m(\vec{x}))
5. 関数$ f:\N^n \to \Nと関数$ g:\N^{n+2} \to \Nの原始再帰$ \mathrm{prec}_{f,g}
$ \mathrm{prec}(\vec{x},0) = f(\vec{x})
$ \mathrm{prec}(\vec{x},n+1) = g(\vec{x},n,\mathrm{prec}(\vec{x},n))
1. $ A(0,y) = y + 1
2. $ A(x+1,0) = A(x,1)
3. $ A(x+1,y+1) = A(x,A(x+1,y))
Lem.1
1. $ m+n+1 \leq A(m,n)
2. $ A(m,n) < A(m,n+1)
3. $ A(m,n+1) \leq A(m+1,n)
4. $ A(m,n) < A(m+1,n)
Thm 1.
任意の原始再帰関数$ f:\N^n \to \Nに対し，ある自然数$ cが存在し，任意の自然数$ x_1,\dots,x_nに対し
$ f(x_1,\dots,x_n) < A(c,\max(x_1,\dots,x_n))
ただし，$ n=0のとき，$ \max() = 0とする．（正確には何でも構わない）
proof:
原始再帰関数の定義に閉じていることを確認すれば良い．
1. $ Z()
$ A(0,\max()) = A(0,0) = 1であるので$ Z() < A(0,0)
2. $ S(x) = x+1
$ c=0とすれば$ A(0,y) = y+1 = S(y)であるので，
$ c=1とすればLem 2より$ S(y) = A(0,y) < A(1,y)
3. $ \mathrm{proj}^n_i(x_1,\dots,x_n) = x_i
$ c = 0とすれば$ A(0,\max(x_1,\dots,x_n)) = \max(x_1,\dots,x_n) + 1．
よって任意の$ iに対して$ \mathrm{proj}^n_i(x_1,\dots,x_n) < A(0,\max(x_1,\dots,x_n))
4. $ \mathrm{comp}_{f_1,\dots,f_m,g}(\vec{x}) = g(f_1(\vec{x}),\dots,f_m(\vec{x}))
$ \mathrm{comp}_{f_1,\dots,f_m,g}(\vec{x}) = g(f_1(\vec{x}),\dots,f_m(\vec{x})) < A(c,\max(\vec{x}))な$ cが存在することをチェックする
関数$ f_1,\dots,f_m,gについて成り立つとし，それぞれ$ c_1,\dots,c_m,dとして存在するとする．
$ g(f_1(\vec{x}),\dots,f_m(\vec{x}))
$ < A(d,\max(f_1(\vec{x}),\dots,f_m(\vec{x})))(仮定)
$ < A(d,\max(A(c_1,\max(\vec{x})),\dots,A(c_m,\max(\vec{x}))))(線型性)
$ f_1(\vec{x}) < A(c_1,\max(\vec{x})),\dots,f_m(\vec{x}) < A(c_m,\max(\vec{x}))(仮定)
$ \max(f_1(\vec{x}),\dots,f_m(\vec{x})) < \max(A(c_1,\max(\vec{x})),\dots,A(c_m,\max(\vec{x})))
5. 原始再帰
関数$ f:\N^n \to \Nと関数$ g:\N^{n+2} \to \Nの原始再帰$ \mathrm{prec}_{f,g}
$ \mathrm{prec}(\vec{x},0) = f(\vec{x})
$ \mathrm{prec}(\vec{x},n+1) = g(\vec{x},n,\mathrm{prec}(\vec{x},n))
次を仮定する．
$ f(\vec{x}) < A(c_f,\max{\vec{x}})なる$ c_fの存在
$ g(\vec{x},y,z) < A(c_g,\max({\vec{x},y,z}))なる$ c_gの存在
$ n = 0のとき
$ \mathrm{prec}(\vec{x},0) = f(\vec{x}) < A(c_f,\max{\vec{x}})より$ c_f < cとすれば
線型性より$ A(c_f,\max{\vec{x}}) < A(c,\max{\vec{x}})．
したがって$ \mathrm{prec}(\vec{x},0) < A(c,\max{\vec{x}})．
$ n = kのとき$ \mathrm{prec}(\vec{x},k) < A(c,\max{\vec{x}})を仮定して，$ n = k+1の時$ \mathrm{prec}(\vec{x},k+1) < A(c,\max{\vec{x}})か？
$ \mathrm{prec}(\vec{x},k+1)
$ = g(\vec{x},k,\mathrm{prec}(\vec{x},k))
$ < A(c_g, \max(\vec{x},k,\mathrm{prec}(\vec{x},k)))
$ \leq A(c_g, \max(\vec{x},k,A(c,\max{\vec{x}}))
仮定より$ \max(\vec{x},k,\mathrm{prec}(\vec{x},k)) \leq \max(\vec{x},k,A(c,\max{\vec{x}}))なので線型性より
$ < A(c_g+1,\max(\vec{x},k,A(c,\max{\vec{x}})))．線型性より
$ = A(c_g,A(c_g+1,\max(\vec{x},k,A(c,\max{\vec{x}}))))
Thm 2.
$ Aは原始再帰関数ではない．
proof
1. 仮に$ Aが原始再帰関数であるとする．
2. $ A'(x) \coloneqq A(x,x)とする．$ A'は原始再帰関数．
3. Thm1より任意の$ xに対して$ A'(x) < A(c,\max(x,x)) = A(c,x)
すなわち$ A(x,x) < A(c,x)が成り立つ．
4. $ x = c+1とすると
右辺$ A(c+1,c+1) = A(c,A(c+1,c)) > A(c+1,c)(Lem 1)
左辺$ A(c,c+1) < A(c+1,c+1)(Lem 2)
すなわち$ A(c+1,c) < A(c+1,c+1) < A(c,c+1) < A(c+1,c+1)となり，明らかに破綻する．
5. よって，$ Aは原始再帰関数ではない．
Lem 1:
任意の$ x,yに対し，$ A(x,y) > y
proof
1. $ x = 0で任意の$ yについて
$ x=0のときは自明
2, 任意の$ xと$ y = 0のとき
1. 任意の$ kで$ A(k,y) > yを仮定し(hyp1)，$ A(k+1,y) > yを示す．
2. $ A(k+1,0) = A(k,1) > 1 > 0であるので，$ A(k+1,0) > 0．
hyp1の$ k = 0のケースは1で正当化される．
3. 任意の$ x,yについて
1. 任意の$ kで$ A(x+1,k) > kを仮定し(hyp2)，$ A(x+1,k+1) > k+1を示す．
2. $ A(x+1,k+1) = A(x,A(x+1,k)) > A(x+1,k)(hyp1)
3. $ A(x+1,k) > k(hyp2)
4. $ A(x+1,k+1) > A(x+1,k) > kより，$ A(x+1,k+1) > k+1
$ A(x+1,k) > k \implies A(x+1,k) \ge k+1
$ A(x+1,k+1) > A(x+1,k) \ge k+1 \implies A(x+1,k+1) > k+1
hyp2の$ k=0のケースは2で正当化される．