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

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

たらい回し関数(1)

たらい回し関数

たらい回し関数は変数を取り除く例としては使えそうにないので別の項目にすることにしました。ここでは帰納法のパターンについて調べていきます。まず普通に帰納法で証明しようと思ったのですが、以下の順にしないとうまく証明できないようです。

たらい回し関数の定義

たらい回し関数は以下のように定義されます(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)、下の関数を t'(x, y, z) とおきます。
t(x, y, z) = \begin{cases} y & (x \leq y\ のとき) & (1) \\ t(t(x-1, y, z), t(y-1, z, x), t(z-1, x, y)) & (x > y \ のとき) & (2) \\ \end{cases}
t'(x, y, z) = \begin{cases} y & (x \leq y\ のとき) \\ z & (x > y \ かつ \ y \leq z \ のとき) \\ x & (x > y \ かつ \ y > z \ のとき) \\ \end{cases}
と書きます。

\mathbb{R} を実数全体の集合、 \mathbb{N} を自然数(負ではない整数)全体の集合)とします。任意の x, y, z \in \mathbb{R} に対して t(x, y, z) = t'(x, y, z) であることを示します。

(1) x \le y ならば t(x, y, z) = y

定義の(1)の場合から成り立ちます。

(2) x > y かつ y \le z ならば t(x, y, z) = z

定義の(1)の場合から t(y-1, z, *) = z となります。

(2-1) x - 1 \le y のとき

定義の(1)の場合から t(x-1, y, *) = y、 t(y, z, *) = z となります。よって
\begin{eqnarray*} t(x, y, z) & = & t(t(x-1, y, z), t(y-1, z, x), t(z-1, x, y)) \\ & = & t(y, z, t(z-1, x, y)) \\ & = & z \end{eqnarray*}

(2-2) x - 1 > y かつ t(x-1, y, z) = z のとき

定義の(1)の場合から t(z, z, *) = z となります。よって
\begin{eqnarray*} t(x, y, z) & = & t(t(x-1, y, z), t(y-1, z, x), t(z-1, x, y)) \\ & = & t(z, z, t(z-1, x, y)) \\ & = & z \end{eqnarray*}

(2-3) (2)の証明

m = \min\{m \in \mathbb{N} \mid x-m \leq y\} とおくと m \ge 1 となります。(2-1)から m = 1 のときは成り立ちます。 m \ge 2 として m - 1 のとき成り立つと仮定すると(2-2)から m のときも成り立ちます。よって帰納法により(2)が成り立ちます。

(3) x > y かつ y > z ならば t(x, y, z) = x

定義の(1)の場合から t(z-1, x, *) = x となります。

(3-1) y - 1 \le z のとき

定義の(1)の場合から t(y-1, z, *) = z となります。

(3-1-1) x - 1 \le y のとき

定義の(1)の場合から t(x-1, y, *) = y となり、(2)から t(y, z, x) = x となります。よって
\begin{eqnarray*} t(x, y, z) & = & t(t(x-1, y, z), t(y-1, z, x), t(z-1, x, y)) \\ & = & t(y, z, x) \\ & = & x \end{eqnarray*}

(3-1-2) x - 1 > y かつ t(x-1, y, z) = x のとき

(2)から t(x, z, x) = x となります。よって
\begin{eqnarray*} t(x, y, z) & = & t(t(x-1, y, z), t(y-1, z, x), t(z-1, x, y)) \\ & = & t(x, z, x) \\ & = & x \end{eqnarray*}

(3-1-3) (3-1)の証明

m = \min\{m \in \mathbb{N} \mid x-m \leq y\} とおくと m \ge 1 となります。(3-1-1)から m = 1 のときは成り立ちます。 m \ge 2 として m - 1 のとき成り立つと仮定すると(3-1-2)から m のときも成り立ちます。よって帰納法により(3-1)が成り立ちます。

(3-2) y - 1 > z のとき

(2)から t(y-1, z, x) = x となります。

(3-2-1) x - 1 \le y のとき

定義の(1)の場合から t(x-1, y, *) = y となり、(2)から t(y, x, x) = x となります。よって
\begin{eqnarray*} t(x, y, z) & = & t(t(x-1, y, z), t(y-1, z, x), t(z-1, x, y)) \\ & = & t(y, x, x) \\ & = & x \end{eqnarray*}

(3-2-2) x - 1 > y かつ t(x-1, y, z) = x のとき

定義の(1)の場合から t(x, x, *) = x となります。よって
\begin{eqnarray*} t(x, y, z) & = & t(t(x-1, y, z), t(y-1, z, x), t(z-1, x, y)) \\ & = & t(x, x, x) \\ & = & x \end{eqnarray*}

(3-2-3) (3-2)の証明

m = \min\{m \in \mathbb{N} \mid x-m \leq y\} とおくと m \ge 1 となります。(3-2-1)から m = 1 のときは成り立ちます。 m \ge 2 として m - 1 のとき成り立つと仮定すると(3-2-2)から m のときも成り立ちます。よって帰納法により(3-2)が成り立ちます。

(3-1)と(3-2)から(3)がわかります。(1)と(2)と(3)から t(x, y, z) = t'(x, y, z) となります。