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

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

たらい回し関数(2)

前回の説明ではたらい回し関数が「定義されている」とはどういうことなのかという説明が不足していました。たらい回し関数の定義
 \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}
は、以下の関数「tarai」の呼び出し回数(count)が有限(「tarai」が有限時間で終了する)のとき「定義されている」とします。ここで float は(コンピューター上の実数ではなく)数学的な実数と同じものとします。

        public static string Test()
        {
            int count = 0;
            float tarai(float x, float y, float z)
            {
                count++;
                if (x <= y)
                {
                    return y;
                }
                else
                {
                    float a = tarai(x - 1, y, z);
                    float b = tarai(y - 1, z, x);
                    float c = tarai(z - 1, x, y);
                    return tarai(a, b, c);
                }
            }
            return $"{tarai(12, 6, 0)}, count = {count}";
        }

 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) = t'(x, y, z) であることを示します。

 x \setminus y = \min\{m \in \mathbb{N} \mid x-m \leq y\} とおきます。

 \delta(x, y, z) = (x \setminus \min \{ x, y, z \}) + (y \setminus \min \{ x, y, z \}) + (z \setminus \min \{ x, y, z \}) とおいて  \delta(x, y, z) に関する帰納法で証明します。 \delta(x, y, z) = 0 のときは  x = y = z となるので  t(x, y, z) = y = t'(x, y, z) が成り立っています。

 \delta(x, y, z) \ge 1 として  \delta(x, y, z) - 1 では成り立っていると仮定します。(*)

(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)) \\
\end{eqnarray*}
となって、 z - 1 \le x のときは定義の(1)の場合から  t(z-1, x, y) = x であり  z - 1 > x のときは仮定(*)から  t(z-1, x, y) は定義されているので、 t(y, z, t(z-1, x, y)) は定義されていて  t(y, z, t(z-1, x, y)) = z となります。

(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)) \\
\end{eqnarray*}
となって、 z - 1 \le x のときは定義の(1)の場合から  t(z-1, x, y) = x であり  z - 1 > x のときは仮定(*)から  t(z-1, x, y) は定義されているので、 t(y, z, t(z-1, x, y)) は定義されていて  t(y, z, t(z-1, x, y)) = z となります。

(2-3) (2)の証明

 m = x \setminus 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 = x \setminus 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 = x \setminus 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) となります。

よって  \delta(x, y, z) の場合も成り立ちます。