エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

アッカーマン関数(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' が存在します。