前回の説明ではたらい回し関数が「定義されている」とはどういうことなのかという説明が不足していました。たらい回し関数の定義
は、以下の関数「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}"; }
とおきます。
を実数全体の集合、
を自然数(負ではない整数)全体の集合)とします。任意の
に対して
が(上の意味で)定義されていて、
であることを示します。
とおきます。
とおいて
に関する帰納法で証明します。
のときは
となるので
が成り立っています。
として
では成り立っていると仮定します。(*)
(1)
ならば 
定義の(1)の場合から成り立ちます。
(2)
かつ
ならば 
定義の(1)の場合から となります。
(2-1)
のとき
定義の(1)の場合から 、
となります。よって
となって、 のときは定義の(1)の場合から
であり
のときは仮定(*)から
は定義されているので、
は定義されていて
となります。
(2-2)
かつ
のとき
定義の(1)の場合から となります。よって
となって、 のときは定義の(1)の場合から
であり
のときは仮定(*)から
は定義されているので、
は定義されていて
となります。
(2-3) (2)の証明
とおくと
となります。(2-1)から
のときは成り立ちます。
として
のとき成り立つと仮定すると(2-2)から
のときも成り立ちます。よって帰納法により(2)が成り立ちます。
(3)
かつ
ならば 
定義の(1)の場合から となります。
(3-1)
のとき
定義の(1)の場合から となります。
(3-1-1)
のとき
定義の(1)の場合から となり、(2)から
となります。よって
(3-1-2)
かつ
のとき
(2)から となります。よって
(3-1-3) (3-1)の証明
とおくと
となります。(3-1-1)から
のときは成り立ちます。
として
のとき成り立つと仮定すると(3-1-2)から
のときも成り立ちます。よって帰納法により(3-1)が成り立ちます。
(3-2)
のとき
(2)から となります。
(3-2-1)
のとき
定義の(1)の場合から となり、(2)から
となります。よって
(3-2-2)
かつ
のとき
定義の(1)の場合から となります。よって
(3-2-3) (3-2)の証明
とおくと
となります。(3-2-1)から
のときは成り立ちます。
として
のとき成り立つと仮定すると(3-2-2)から
のときも成り立ちます。よって帰納法により(3-2)が成り立ちます。
(3-1)と(3-2)から(3)がわかります。(1)と(2)と(3)から となります。
よって の場合も成り立ちます。