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

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

ラムダ計算と無限ラムダ多項式(17)

たらい回し関数の例

フィボナッチ数列の例ではクロージャーを変数を使わずに書く例としては単純すぎてわかりにくかったので、たらい回し関数が使えるかどうか調べてみます。まずたらい回し関数自体について調べてみます。たらい回し関数は以下のように定義された関数です(wikipedia:竹内関数参照)。
 \mathrm{tarai}(x,y,z)= \\
\begin{cases}
y & (x \leq y \ のとき) \\
\mathrm{tarai}(\mathrm{tarai}(x-1,y,z), \mathrm{tarai}(y-1,z,x), \mathrm{tarai}(z-1,x,y)) & (x > y \ のとき) \\
\end{cases}

 \mathrm{tarai}(x,y,z)=
\begin{cases}
y & (x \leq y\  のとき) \\
z & (x > y \ かつ \ y \leq z \ のとき) \\
x & (x > y \ かつ \ y > z \ のとき) \\
\end{cases}
が成り立ちます。まずこれが成り立つことを示します。 \mathrm{tarai}(x,y,z) t(x, y, z) と書きます。

ハッカーの遺言状──竹内郁雄の徒然苔第18回:問題児も悪くない | サイボウズ式によると整数でなくても成り立つということなので、そのような形で示します。うまくパターン化できるかと思ったのですができなかったので長くなっています。

 x \leq y のとき

定義より  x \leq y のとき  t(x,y,z)=y が成り立ちます。

 x > y かつ  y \leq z のとき

 c_n = t(x-n, y, z) d_n = t(z-1,x-n,y) とおきます。 y-1 < y \leq z となるので定義より   t(y-1,z,x-n) = z となります。よって
 c_n = t(x-n, y, z) \\
= t(t(x-(n+1),y,z), t(y-1,z,x-n), t(z-1,x-n,y)) \\
= t(c_{n+1}, z, d_n)
が成り立ちます。

 n = \min\{n \mid x-n \leq y\} \ (n \ge 1) とおくと
 c_n = t(x-n, y, z) = y
 c_{n-1} = t(c_n, z, d_{n-1}) = t(y, z, d_{n-1}) = z
が成り立ちます。

帰納法により  c_{i} = z \ (i = 0, 1, \cdots , n-1) を示します。 i = n-1 の場合は上に書いた通りです。 i=k のときに成り立つと仮定すると
 c_{k-1} = t(c_{k}, z, d_{k-1}) = t(z, z, d_{k-1}) = z
となって  i=k-1 のときにも成り立ちます。よって  c_{i} = z \ (i = 0, 1, \cdots , n-1) が成り立ちます。

よって  t(x,y,z) = c_{0} = z が成り立ちます。

 x > y かつ   y > z のとき

 a_{m} = t(x-m, y, z)
 b_{m} = \begin{cases}
z & (y-1 \le z \ のとき) \\
x-m & (y-1 > z \ のとき)
\end{cases}
とおきます。

 x-m > y かつ   y > z のとき
 a_{m} = t(x-m, y, z) \\
= t(t(x-(m+1), y, z), t(y-1, z, x-m), t(z-1, x-m, y)) \\
= t(a_{m+1}, b_{m}, x-m)
となります。

 m = \min\{m \mid x-m \leq y\} \ (m \ge 1) とおくと  x-(m-1) > y かつ  x-m \le y かつ   y > z となります。
 a_{m} = t(x-m, y, z) = y
 a_{m-1} = t(a_{m}, b_{m-1}, x-(m-1)) = t(y, b_{m-1}, x-(m-1))
が成り立ちます。ここで
 b_{m-1} = \begin{cases}
z & < & y &(y-1 \le z \ のとき) & (1) \\
x-(m-1) & > & y & (y-1 > z \ のとき) & (2)
\end{cases}
なので (2) のときは  a_{m-1} = x-(m-1) となります。(1) のときは
 a_{m-1} = t(y, z, x-(m-1)) = x-(m-1)
となります。

帰納法により  a_{i} = x-i \ (i = 0, 1, \cdots , m-1) を示します。 i = m-1 の場合は上に書いた通りです。 i=k のときに成り立つと仮定すると
 a_{k-1} = t(a_{k}, b_{k-1}, x-(k-1)) = t(x-k, b_{k-1}, x-(k-1))
 b_{k-1} = \begin{cases}
z & < & x-k &(y-1 \le z \ のとき) & (1) \\
x-(k-1) & > & x-k & (y-1 > z \ のとき) & (2)
\end{cases}
となるので (2) のときは  a_{k-1} = x-(k-1) となります。(1) のときは
 a_{k-1} = t(x-k, z, x-(k-1)) = x-(k-1)
となります。よって  a_{i} = x-i \ (i = 0, 1, \cdots , m-1) が成り立ちます。

よって  t(x, y, z) = a_{0} = x が成り立ちます。