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

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

たらい回し関数(6)

while の繰り返しが2回以下であることを考えると、以下のように書き直すことができます。これを見ると a2 と c2 は計算する必要がありません。

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

たらい回し関数(5)

たらい回し関数についてはクロージャーの説明には使えそうにないので変数を使わないように書き直す意味はあまりないとは思いますが、やってみます。

たらい回し関数をできるだけ変数を使わないように書き直します。このために前回「呼び出しの深さ」について考えました。「呼び出しの深さ」別に tarai_0、tarai_1、tarai_2 のように関数を作っていきます。以下では「呼び出しの深さ」2 でかなり複雑になるので以下の関数では 2 までしかありません.が、これが無限に続くと考えると擬似的に無限の場合を表しています。

C# ではあまりうまく書くことができないのでわかりにくいですし、「呼び出しの深さ」2 までしかないので「幅」0 の場合しか計算できません(これはあまり意味がありません)。これが続いていくことを想像できるようコードを掲載します。

        public static string Test()
        {
            float tarai_0(float x, float y, float z)
            {
                return (x <= y ?
                        y :
                        0);
            }
            float tarai_1(float x, float y, float z)
            {
                return (x <= y ?
                        y :
                        ((x - 1 <= y ?
                            y :
                            0) <= (y - 1 <= z ?
                            z :
                            0) ?
                            (y - 1 <= z ?
                                z :
                                0) :
                            0));
            }
            float tarai_2(float x, float y, float z)
            {
                return (x <= y ?
                        y :
                        ((x - 1 <= y ?
                            y :
                            ((x - 1 - 1 <= y ?
                                y :
                                0) <= (y - 1 <= z ?
                                z :
                                0) ?
                                (y - 1 <= z ?
                                    z :
                                    0) :
                                0)) <= (y - 1 <= z ?
                            z :
                            ((y - 1 - 1 <= z ?
                                z :
                                0) <= (z - 1 <= x ?
                                x :
                                0) ?
                                (z - 1 <= x ?
                                    x :
                                    0) :
                                0)) ?
                            (y - 1 <= z ?
                                z :
                                ((y - 1 - 1 <= z ?
                                    z :
                                    0) <= (z - 1 <= x ?
                                    x :
                                    0) ?
                                    (z - 1 <= x ?
                                        x :
                                        0) :
                                    0)) :
                            (((x - 1 <= y ?
                                y :
                                ((x - 1 - 1 <= y ?
                                    y :
                                    0) <= (y - 1 <= z ?
                                    z :
                                    0) ?
                                    (y - 1 <= z ?
                                        z :
                                        0) :
                                    0)) - 1 <= (y - 1 <= z ?
                                z :
                                ((y - 1 - 1 <= z ?
                                    z :
                                    0) <= (z - 1 <= x ?
                                    x :
                                    0) ?
                                    (z - 1 <= x ?
                                        x :
                                        0) :
                                    0)) ?
                                (y - 1 <= z ?
                                    z :
                                    ((y - 1 - 1 <= z ?
                                        z :
                                        0) <= (z - 1 <= x ?
                                        x :
                                        0) ?
                                        (z - 1 <= x ?
                                            x :
                                            0) :
                                        0)) :
                                0) <= ((y - 1 <= z ?
                                z :
                                ((y - 1 - 1 <= z ?
                                    z :
                                    0) <= (z - 1 <= x ?
                                    x :
                                    0) ?
                                    (z - 1 <= x ?
                                        x :
                                        0) :
                                    0)) - 1 <= (z - 1 <= x ?
                                x :
                                ((z - 1 - 1 <= x ?
                                    x :
                                    0) <= (x - 1 <= y ?
                                    y :
                                    0) ?
                                    (x - 1 <= y ?
                                        y :
                                        0) :
                                    0)) ?
                                (z - 1 <= x ?
                                    x :
                                    ((z - 1 - 1 <= x ?
                                        x :
                                        0) <= (x - 1 <= y ?
                                        y :
                                        0) ?
                                        (x - 1 <= y ?
                                            y :
                                            0) :
                                        0)) :
                                0) ?
                                ((y - 1 <= z ?
                                    z :
                                    ((y - 1 - 1 <= z ?
                                        z :
                                        0) <= (z - 1 <= x ?
                                        x :
                                        0) ?
                                        (z - 1 <= x ?
                                            x :
                                            0) :
                                        0)) - 1 <= (z - 1 <= x ?
                                    x :
                                    ((z - 1 - 1 <= x ?
                                        x :
                                        0) <= (x - 1 <= y ?
                                        y :
                                        0) ?
                                        (x - 1 <= y ?
                                            y :
                                            0) :
                                        0)) ?
                                    (z - 1 <= x ?
                                        x :
                                        ((z - 1 - 1 <= x ?
                                            x :
                                            0) <= (x - 1 <= y ?
                                            y :
                                            0) ?
                                            (x - 1 <= y ?
                                                y :
                                                0) :
                                            0)) :
                                    0) :
                                0)));
            }
            int diff(float x, float y)
            {
                if (x <= y)
                {
                    return 0;
                }
                else
                {
                    return (int)Math.Ceiling(x - y);
                }
            }
            int dist(float x, float y, float z)
            {
                float m = Math.Min(Math.Min(x, y), z);
                return diff(x, m) + diff(y, m) + diff(z, m);
            }
            float tarai(float x, float y, float z)
            {
                switch (dist(x, y, z) * 3 + 1)
                {
                    case 0:
                        return tarai_0(x, y, z);
                    case 1:
                        return tarai_1(x, y, z);
                    case 2:
                        return tarai_2(x, y, z);
                }
                return -1;
            }
            return tarai(0, 0, 0).ToString();
        }

このように x、y、z 以外の変数を使わないように書き直すことができました。

たらい回し関数(4)

たらい回し関数(以下の  t または tarai)の呼び出しが重なっている(呼び出しが終了する前に呼び出しが行われる)回数の最大値を「呼び出しの深さ」と呼ぶことにします(以下の depth)。

        public static string Test()
        {
            int count = 0;
            int depth = 0;
            float tarai(float x, float y, float z, int d)
            {
                count++;
                depth = d + 1 > depth ? d + 1 : depth;
                if (x <= y)
                {
                    return y;
                }
                else
                {
                    return tarai(tarai(x - 1, y, z, d + 1), tarai(y - 1, z, x, d + 1), tarai(z - 1, x, y, d + 1), d + 1);
                }
            }
            return $"{tarai(12, 6, 0, 0)}, count = {count}, depth = {depth}";
        }

 \mathbb{R} を実数全体の集合、 \mathbb{N}自然数(負ではない整数)全体の集合)とします。 x, y \in \mathbb{R} に対して  x \setminus y = \min\{m \in \mathbb{N} \mid x-m \leq y\} とおきます。 x, y, z \in \mathbb{R} に対して  x, y, z の「幅」  \delta(x, y, z) \delta(x, y, z) = (x \setminus \min \{ x, y, z \}) + (y \setminus \min \{ x, y, z \}) + (z \setminus \min \{ x, y, z \}) と定義します。 x, y, z の「幅」と「呼び出し深さ」(depth)、「呼び出しの回数」(count)の関係を考えます。

上記の C# のコードを while を使って書き直します。

        public static string Test()
        {
            int count = 0;
            int depth = 0;
            float tarai(float x, float y, float z, int d)
            {
                count++;
                d++;
                depth = d > depth ? d : depth;
                while (x > y)
                {
                    float a = tarai(x - 1, y, z, d);
                    float b = tarai(y - 1, z, x, d);
                    float c = tarai(z - 1, x, y, d);
                    (x, y, z) = (a, b, c);
                    count++;
                    d++;
                    depth = d > depth ? d : depth;
                }
                return y;
            }
            return $"{tarai(12, 6, 0, 0)}, count = {count}, depth = {depth}";
        }

while の中の繰り返しの回数を考えます。

 x > y とします。

「幅」が  \delta(x, y, z) - 1 以下のときの「呼び出しの深さ」は  d 以下、「呼び出しの回数」は  c 以下であるとします。

「幅」が  \delta(x, y, z) - 1 以下である  x', y', z' に対して
 \begin{eqnarray*}
t(x', y', z')
 & = &
\begin{cases}
y' & (x' \leq y') \\
z' & (x' > y', & y' \leq z') & \cdots (*)\\
x' & (x' > y', & y' > z') \\
\end{cases} \\
\end{eqnarray*}
が成り立っているとします。

(1)  t(x-1, y, z) = x - 1 のとき

(*)より  t(x-1, y, z) = x-1, y, \operatorname{or} z で、 t(x-1, y, z) = x - 1 となるのは  x -1 > y > z の場合となります。このとき
 \begin{eqnarray*}
t(y-1, z, x)
 & = &
\begin{cases}
z & (y-1 \leq z) \\
x & (y-1 > z, & z \leq x) \\
y-1 & (y-1 > z, & z > x) \\
\end{cases} \\
 & = &
\begin{cases}
z & (y-1 \leq z) \\
x & (y-1 > z) \\
\end{cases} \\
\end{eqnarray*}
 \begin{eqnarray*}
t(z-1, x, y)
 & = &
\begin{cases}
x & (z-1 \leq x) \\
y & (z-1 > x, & x \leq y) \\
z-1 & (z-1 > x, & x > y) \\
\end{cases} \\
 & = & x
\end{eqnarray*}
となります。よって  t(x-1, y, z) = x - 1 のとき  t(y-1, z, x) t(z-1, x, y) x, z のどれかとなります。(*)より  t(t(x-1, y, z), t(y-1, z, x), t(z-1, x, y)) の引数の「呼び出しの深さ」は  d 以下、「呼び出しの回数」は  3c 以下となります。

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

(*)より  t(y-1, z, x) = y-1, z, \operatorname{or} x で、 t(y-1, z, x) = y - 1 となるのは  y -1 > z > x の場合となりますが、 x > y なのでこれは起こりません。

(3)  t(z-1, x, y) = z - 1 のとき

(*)より  t(z-1, x, y) = z-1, x, \operatorname{or} y で、 t(z-1, x, y) = z - 1 となるのは  z -1 > x > y の場合となります。このとき
 \begin{eqnarray*}
t(x-1, y, z)
 & = &
\begin{cases}
y & (x-1 \leq y) \\
z & (x-1 > y, & y \leq z) \\
x-1 & (x-1 > y, & y > z) \\
\end{cases} \\
 & = &
\begin{cases}
y & (x-1 \leq y) \\
z & (x-1 > y, & y \leq z) \\
\end{cases} \\
\end{eqnarray*}
 \begin{eqnarray*}
t(y-1, z, x)
 & = &
\begin{cases}
z & (y-1 \leq z) \\
x & (y-1 > z, & z \leq x) \\
y-1 & (y-1 > z, & z > x) \\
\end{cases} \\
 & = &
\begin{cases}
z & (y-1 \leq z) \\
x & (y-1 > z, & z \leq x) \\
\end{cases} \\
\end{eqnarray*}
となります。よって  t(z-1, x, y) = z - 1 のとき  t(y-1, z, x) t(z-1, x, y) x, y, z のどれかとなります。(*)より  t(t(x-1, y, z), t(y-1, z, x), t(z-1, x, y)) の引数の「呼び出しの深さ」は  d 以下、「呼び出しの回数」は  3c 以下となります。

(4) それ以外のとき

(1)(2)(3)以外のとき、 t(x-1, y, z) t(y-1, z, x) t(z-1, x, y) x, y, z のどれかとなります。
 \begin{eqnarray*}
a = t(x-1, y, z)
 & = &
\begin{cases}
y & (x-1 \leq y, & x > y) \\
z & (x-1 > y, & y \leq z, & x > y) \\
\end{cases} \\
\end{eqnarray*}
 \begin{eqnarray*}
b = t(y-1, z, x)
 & = &
\begin{cases}
z & (y-1 \leq z, & x > y) \\
x & (y-1 > z, & z \leq x, & x > y) \\
\end{cases} \\
\end{eqnarray*}
 \begin{eqnarray*}
c = t(z-1, x, y)
 & = &
\begin{cases}
x & (z-1 \leq x, & x > y) \\
\end{cases} \\
\end{eqnarray*}

(4-1)  a = y b = x のとき

 a \le b となるので  t(a, b, c) = b = x となります。

(4-2)  a = z b = z のとき

 a \le b となるので  t(a, b, c) = b = z となります。

(4-3)  a = z b = x のとき

 z \le x であり、よって  a \le b となるので  t(a, b, c) = b = x となります。

(4-4)  a = y b = z y \le z のとき

 a \le b となるので  t(a, b, c) = b = x となります。

(4-5)  a = y b = z y > z のとき

while の繰り返しを抜けずに次の段階に進むことになります。しかし  x > y > z なので次の繰り返しの段階では   a > b かつ  b < c となり、(4-5)の状態は起こりません。よって繰り返しの回数は最大2回となります。

よって「幅」が  \delta(x, y, z) ときの「呼び出しの深さ」は  d + 3 以下、「呼び出しの回数」は  6c + 3 以下となります。

帰納法によって「幅」が  \delta(x, y, z) ときの「呼び出しの深さ」は  3 \delta(x, y, z) + 1 以下、「呼び出しの回数」は  \frac{8}{5} \cdot 6^{\delta(x, y, z)} - \frac{3}{5} 以下となります。

たらい回し関数(3)

(3)の場合を  \delta(x, y, z) に関する帰納法の仮定から証明することができます。

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

 x - 1 \le y のときは定義より  t(x-1, y, z) = y x - 1 > y のときは  \delta(x, y, z) に関する帰納法の仮定(*)より  t(x-1, y, z) は定義されていて
 t(x-1, y, z) =
\begin{cases}
y & (x-1 \leq y\  のとき) \\
z & (x-1 > y \ かつ \ y \leq z \ のとき) \\
x-1 & (x-1 > y \ かつ \ y > z \ のとき) \\
\end{cases}
となります。よって
 \begin{eqnarray*}
t(x, y, z) & = & t(t(x-1, y, z), t(y-1, z, x), t(z-1, x, y)) \\
 & = & 
\begin{cases}
 t(y, z, x) & (x - 1 \le y \ かつ \ y - 1 \le z \ のとき) \\
 t(y, x, x) & (x - 1 \le y \ かつ \ y - 1 > z \ のとき) \\
 t(x-1, z, x) & (x - 1 > y \ かつ \ y - 1 \le z \ のとき) \\
 t(x-1, x, x) & (x - 1 > y \ かつ \ y - 1 > z \ のとき) \\
\end{cases} \\
 & = & 
\begin{cases}
x & (x - 1 \le y \ かつ \ y - 1 \le z \ のとき) \\
x & (x - 1 \le y \ かつ \ y - 1 > z \ のとき) \\
x & (x - 1 > y \ かつ \ y - 1 \le z \ のとき) \\
x & (x - 1 > y \ かつ \ y - 1 > z \ のとき) \\
\end{cases} \\
 & = & x
\end{eqnarray*}

たらい回し関数(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) の場合も成り立ちます。

たらい回し関数(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) となります。

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

たらい回し関数の調査

たらい回し関数は変数を使わない例には使えそうにないですが、調査を継続します。「wikipedia:竹内関数」に書かれている高速化をやってみます。C# で書いた以下のプログラムについて考えます。

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

普通に  \mathrm{tarai}(12, 6, 0) を実行すると結果は以下のようになります。

12, count = 12604861

呼ばれている回数は 12604861 回となります。

遅延評価

 x \le y のときは  z を計算する必要はないので、 zクロージャー化すると呼び出し回数を減らすことができます。

        public static string Test()
        {
            int count = 0;
            int tarai(int x, int y, Func<int> zf)
            {
                count++;
                if (x <= y)
                {
                    return y;
                }
                else
                {
                    return tarai(tarai(x - 1, y, zf), tarai(y - 1, zf(), () => x), () => tarai(zf() - 1, x, () => y));
                }
            }
            return $"{tarai(12, 6, () => 0)}, count = {count}";
        }

結果

12, count = 109

呼び出し回数は 109 回になりました。

メモ化

Dictionary に  (x, y, z) の組を保存し、同じ組に対しては一度しか計算をしないようにします。

        public static string Test()
        {
            Dictionary<(int, int, int), int> dic = new Dictionary<(int, int, int), int>();
            int count = 0;
            int tarai(int x, int y, int z)
            {
                count++;
                if (x <= y)
                {
                    return y;
                }
                else
                {
                    if (dic.ContainsKey((x, y, z)))
                    {
                        return dic[(x, y, z)];
                    }
                    else
                    {
                        int val = tarai(tarai(x - 1, y, z), tarai(y - 1, z, x), tarai(z - 1, x, y));
                        dic[(x, y, z)] = val;
                        return val;
                    }
                }
            }
            return $"{tarai(12, 6, 0)}, count = {count}";
        }

結果

12, count = 449

呼び出し回数は 449 回になりました。