脳ざらし紀行

_ 日本 Ruby カンファレンス 2006 〜ああっ Matz さまっ〜

行けるかな?

_ たらいまわし関数の低姿勢停止性

x, y, z のうちの一番大きい値と小さい値の差に関する帰納法を使えば、x, y, z が整数の時には停止性を証明することが出来るような気がします。

<proof>

x = y = z の時(差が0)は停止して

tak x y z = if x <= y then y else if y <= z then z else x 

であることは明らか。

x, y, z の最大と最小の差がN-1であるときに

tak x y z = if x <= y then y else if y <= z then z else x 

であると仮定する。

x, y, z の最大と最小の差がNであると仮定する。

x <= y のときは ok。以下では、x > y とする。

[i] z > x > y のとき。

tak x y z = tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y)
          = tak (tak (x-1) y z) z (z-1) (帰納法の仮定より tak (z-1) x y = z-1 )

さて、x = y + 1 なら

tak (x-1) y z = tak y y z 
              = y

なので

tak x y z = tak (y+1) y z 
          = tak y z (z-1)
          = z   

。また x = y + 2 でも

tak (y+2) y z = tak (tak (y+1) y z) z (z-1)
              = tak z z (z-1)
              = z

なので、同様にして

tak (y+k) y z = z

[ii] x >= z >= y のとき。

tak x y z = tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y)
          = tak (tak (x-1) y z) z x (帰納法の仮定か[i]の場合に当てはまるので tak (x-1) y z = z)
          = tak z z x
          = z

[iii] x > y > z のとき。

tak x y z = tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y)
          = tak (tak (x-1) y z) (tak (y-1) z x) x (帰納法の仮定より tak (x-1) y z = x-1 )
          = tak (x-1) (tak (y-1) z x) x

y = z + 1 のときは

tak (y-1) z x = tak z z x 
              = z

で

tak x y z = tak (x-1) z x ([i]の場合に当てはまるので)
          = x 

y = z + k のときは

tak (y-1) z x = tak (z+k-1) z x ([i]か[ii]の場合に当てはまるので)
              = x

よって、 [i] [ii] [iii] により

 tak x y z =  if x <= y then y else if y <= z then z else x

である。