エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を表すことを考えていくブロクです。

アッカーマン関数(1)

アッカーマン関数についても調査します。

アッカーマン関数は以下のように非負整数  x y に対して帰納的に定義された関数です(wikipedia:アッカーマン関数計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座) 参照)。
\begin{cases}
f(0, y) & = & y + 1 & (a1) \\
f(x + 1, 0) & = & f(x, 1) & (a2) \\
f(x + 1, y + 1) & = & f(x, f(x + 1, y)) & (a3) \\
\end{cases}

  •  f(x, y) \widehat{f}(x)(y)
  •  \widehat{f}(x_1) ( \widehat{f}(x_2) ( \cdots \widehat{f}(x_n) (y) \cdots )) をかっこを省略して  \widehat{f}(x_1) \widehat{f}(x_2) \cdots \widehat{f}(x_n) (y)
  •  \underbrace {\widehat{f}(x) \cdots \widehat{f}(x)} _{n \ 個} (y) \widehat{f}(x)^n(y)

と書くことにするとアッカーマン関数の定義は
\begin{cases}
\widehat{f}(0)(y) & = & y + 1 & (a1') \\
\widehat{f}(x + 1)(0) & = & \widehat{f}(x)(1) & (a2') \\
\widehat{f}(x + 1)(y + 1) & = & \widehat{f}(x) \widehat{f}(x + 1)(y) & (a3') \\
\end{cases}
となります。
\begin{eqnarray*}
f(x, y) & = & \widehat{f}(x)(y) \\
& \underset{(a3')}{=} & \widehat{f}(x-1) \widehat{f}(x) (y-1) \\
& \underset{(a3')}{=} & \widehat{f}(x-1)^2 \widehat{f}(x) (y-2) \\
& \vdots & \\
& \underset{(a3')}{=} & \widehat{f}(x-1)^y \widehat{f}(x) (0) \\
& \underset{(a2')}{=} & \widehat{f}(x-1)^y \widehat{f}(x-1) (1) \\
& = & \widehat{f}(x-1)^{y+1} (1) \\
\end{eqnarray*}
が成り立ちます。(a4')

アッカーマン関数は原始帰納的関数ではない帰納的関数であるということの証明が計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)の問題にあるのでそれを見ていきます。

まず  f(1, y) f(2, y) f(3, y) f(4, y) がどうなるか調べます。

 f(1, y)

 \widehat{f}(0)(y) = y + 1 n 回繰り返すと
 \widehat{f}(0)^n (y) = y + \underbrace {1+\cdots +1} _{n \ 個} = y + n
となります。よって
 \widehat{f}(1)(y) = \widehat{f}(0)^{y+1} (1) = 1 + (y + 1) = y + 2

 f(2, y)

 \widehat{f}(1)(y) = y + 2 n 回繰り返すと
 \widehat{f}(1)^n (y) = y + \underbrace {2+\cdots +2} _{n \ 個} = y + 2n
となります。よって
 \widehat{f}(2)(y) = \widehat{f}(1)^{y+1} (1) = 1 + 2(y + 1) = 2y + 3

 f(3, y)

 \widehat{f}(2)(y) + 3 = 2(y + 3) となるので、これを  n 回繰り返すと
 \widehat{f}(2)^n(y) = (y + 3) \cdot \underbrace {2 \cdot \cdots \cdot 2} _{n \ 個} - 3 = 2^n(y + 3) - 3
となります。よって
 \widehat{f}(3)(y) = \widehat{f}(2)^{y+1} (1) = 2^{y+1}(1 + 3) - 3 = 2^{y+3} - 3

 f(4, y)

 a^b a \wedge b と書くと、 \widehat{f}(3)(y) + 3 = 2^{y + 3} = 2 \wedge (y + 3) となります。これを  n 回繰り返すと
 \widehat{f}(3)^n(y) =  \underbrace {2 \wedge ( \cdots \wedge (2} _{n \ 個} \wedge (y + 3)) \cdots ) - 3
このかっこは省略することにします。
 \widehat{f}(3)^n(y) =  \underbrace {2 \wedge \cdots \wedge 2} _{n \ 個} \wedge (y + 3) - 3
 \underbrace {a \wedge \cdots \wedge a} _{b \ 個}  a \barwedge b と書くことにすると
 \widehat{f}(4)(y) = \widehat{f}(3)^{y+1} (1) = \underbrace {2 \wedge \cdots \wedge 2} _{y+1 \ 個} \wedge (1 + 3) - 3 = 2 \barwedge (y+3) - 3

問 1.3.17 について考えます。

(1)  x + y + 1 \le f(x, y)

 x = 0 のとき

 f(0, y) \underset{(a1)}{=} y + 1 = x + y + 1

 x - 1 のとき成り立つ(1-1)として  x \ (\ge 1) のとき

 y = 0 のとき

 f(x, 0) \underset{(a2)}{=} f(x-1, 1) \underset{(1-1)}{\ge} (x-1) + 1 + 1 = x + y + 1

 y - 1 のとき成り立つ(1-2)として  y \ (\ge 1) のとき

 \begin{eqnarray*}
f(x, y) & \underset{(a3)}{=} & f(x-1, f(x, y-1)) \\
 & \underset{(1-1)}{\ge} & (x-1) + f(x, y-1) + 1 \\
 & \underset{(1-2)}{\ge} & (x-1) + (x + (y-1) + 1) + 1 \\
 & = & 2x + y \ge x + y + 1
\end{eqnarray*}

(2)  f(x, y) < f(x, y+1) \le f(x + 1, y)

(2-1)  f(x, y) < f(x, y+1)

 x = 0 のとき

 f(0, y) \underset{(a1)}{=} y + 1 < y + 2 \underset{(a1)}{=} f(0, y + 1)

 x \ \ge 1 のとき

 \begin{eqnarray*}
f(x, y+1) & \underset{(a3)}{=} & f(x-1, f(x, y)) \\
 & \underset{(1)}{\ge} & (x-1) + f(x, y) + 1 \\
 & = & x + f(x, y) > f(x, y)
\end{eqnarray*}

(2-2)  f(x, y+1) \le f(x + 1, y)

 x = 0 のとき

 f(x, y+1) = f(0, y+1) \underset{(a1)}{=} y + 2 = f(1, y) = f(x+1, y)

 y = 0 のとき

 f(x, y+1) = f(x, 1) \underset{(a2)}{=} f(x+1, 0) = f(x+1, y)

 x, y \ge 1 のとき

 f(x+1, y-1) \underset{(1)}{\ge} (x+1) + (y-1) + 1 = x + y + 1
よって
 f(x+1, y) \underset{(a3)}{=} f(x, f(x+1, y-1)) \underset{(2-1)}{>} f(x, y+1)

(3) 任意の  a, b \ge 0 に対して  f(a, f(b, y)) < f(c, y) ( \forall y \in \mathbb{N})を満たす  c \ge 0 がある

 b = 0 のとき

 f(a, f(0, y)) \underset{(a1)}{=} f(a, y + 1) \underset{(2-2)}{\le} f(a + 1, y) \underset{(2)}{<} f(a + 2, y)

 b のとき成り立つ(3-1)と仮定して  b + 1 のとき

 y = 0 のとき

 f(a, f(b+1, 0)) \underset{(a2)}{=} f(a, f(b, 1)) \underset{(3-1)}{<} f(c, 1) \underset{(a2)}{=} f(c+1, 0)
を満たす  c が存在します。

 y のとき成り立つ(3-2)と仮定して  y + 1 のとき

 f(a, f(b+1, y+1)) \underset{(a3)}{=} f(a, f(b, f(b+1, y))) \underset{(3-1)}{<} f(c, f(b+1, y)) \underset{(3-2)}{<} f(c', y)
を満たす  c, c' が存在します。