Ackの補題 - mrsekut-p

Ackの補題

アッカーマン関数が原始帰納的関数ではないことの証明の為に使う

アッカーマン関数を$ A(m,n)と表記する

「L」は「Lemma (補題)」の「L」

$ y+2\le A(x+1,y)

証明の流れ

2変数の数学的帰納法をするmrsekut.icon

$ xについては、

仮定: $ A(x+1,y)\ge y+2

目的: $ A(x+2,y)\ge y+2を示す

$ yについては、

仮定: $ A(x+2,y)\ge y+2

この時点で$ xも$ yも仮定されていることになるmrsekut.icon

目的: $ A(x+2,y+1)\ge (y+1)+2を示す

証明

$ xについての数学的帰納法で示す

$ x=0の場合、L1の式は$ A(1,y)=y+2なので成り立つ

$ x\gt0の場合、全ての$ yについて$ A(x+2,y)\ge y+2であると仮定する

これを$ yについての数学的帰納法で示す

$ y=0のとき、

$ A(x+1,0)=A(x+1,1) ∵アッカーマン関数の定義

$ \ge 1+2 ∵$ xに関する帰納法の仮定

$ \ge 0+2

故に成り立つ

$ y>0の場合、$ A(x+2,y)\ge y+2が成り立つと仮定すると

$ A(x+2,y+1)=A(x+1,A(x+2,y)) ∵アッカーマン関数の定義

$ \ge A(x+2,y)+2 ∵$ xに関する帰納法の仮定

$ \ge (y+2)+2 ∵$ yに関する帰納法の仮定

$ \ge (y+1)+2

故に成り立つ

$ y+1\le A(x,y)

証明

$ x=0のとき、$ A(0,y)=y+1なので成立

$ x\gt0のとき、

$ A(x,y)=A((x-1)+1,y)\ge y+2\ge y+1なので成立

↑$ x=x-1+1 ↑L1

$ y \lt y'\Rightarrow A(x,y)\lt A(x,y')

証明

$ x=0のとき

$ A(0,y)=y+1\lt y'+1=A(0,y')だから成立

$ x+1のとき

$ A(x+1,y+1)=A(x,A(x+1,y))∵アッカーマン関数の定義

$ \ge A(x+1,y)+1 ∵L2

$ \gt A(x+1,y)

が成り立つ

これを繰り返し使用すれば$ y\lt y'\Rightarrow A(x+1,y)\lt A(x+1,y')が得られる

$ A(x, y+1)\le A(x+1, y)

証明

$ y=0のとき

$ A(x+1,0)=A(x,1)だから成立

$ y\gt0のとき

$ A(x+1,y)=A(x,A(x+1,y-1)) ∵アッカーマン関数の定義

$ \ge A(x,(y-1)+2) ∵外部がL3, 内部がL1

$ \ge A(x,y+1)

よって成立

$ x\lt x'\Rightarrow A(x,y)\lt A(x', y)

証明

$ A(x,y)\lt A(x,y+1)\le A(x+1,y)

↑L3 ↑L4

よって成り立つ

これを繰り返せばいい

$ \forall a,b\exist c[A(a, A(b, x))\le A(c,x )] が成り立つ

$ a,bがわかっている上で、内部の式を満たすような$ cが存在するmrsekut.icon

証明

$ a\le c',b\le c'+1であるような$ c'を選ぶと、

$ A(a,A(b,x))\le A(c',A(c'+1,x)) ∵↑の仮定

$ = A(c'+1,x+1) ∵アッカーマン関数の定義

$ \le A(c'+2,x) ∵L4

が成り立つ。従って$ c=c'+2とすれば良い

$ \max\{A(c_1,a),\cdots,A(c_m,a)\}=A(\max\{c_1,\cdots,c_m\},a)

自明

L3とL4とL5の図的理解

それぞれアッカーマン関数の引数でマトリックスにしたときの、横、斜め、縦の大小関係を表している

アッカーマン関数#5ee6352219827000003379b8のような表

https://gyazo.com/0dc01642877c212a70f1e7ca13d288d0

table:参考との対応表

このノート『計算可能性入門』「原始帰納的函数とアッカーマン関数」のPDF

L1 性質1 -

L2 性質2 補題3

L3 性質3 補題4

L4 性質4 補題8

L5 性質5 補題5

L6 性質6 -

L7 - -

参考

『計算可能性入門』 p.159~

親切でわかりやすい

原始帰納的函数とアッカーマン函数