タグ : Algorithm

たらいまわし関数の停止性

たらいよ, とまれ!

Curry-Howardの対応について調べてたはずなのに, なぜかこの記事 によってたらいまわし関数に興味が出たので.

f(x,y,z) =
 if x <= y then y
           else f(f(x-1,y,z), f(y-1,z,x), f(z-1,x,y))

これがたらい回し関数, 竹内関数とも(あの竹内先生?).

 

場合分けでいけそう?

f(x, y, z) について, 「最小の引数」について場合分け.

case1
x <= y, z 

  1. x <= y なので y を返して停止.
case2
y <= x, z ∧ not case1
fで再帰. それぞれの引数についてさらに考える. 

  1. f(x-1, y, z) : は, x-1=y となる場合 case1(停止). それ以外は case2に帰着.
  2. f(y-1, z, x) : は, y-1 が最も小さい値なのでcase1(停止)
  3. f(z-1, x, y) : は, z-1=y となる場合 case1(停止), それ以外は case3に帰着.
case3
z <= x, y ∧ not case1 ∧ not case2
fで再帰. それぞれの引数についてさらに考える. 

  1. f(x-1, y, z) : は, x-1=z となる場合 case1(停止). それ以外は case3に帰着.
  2. f(y-1, z, x) : は, y-1=z となる場合 case1(停止). それ以外は case2に帰着.
  3. f(z-1, x, y) : は, z-1 が最も小さい値なのでcase1(停止).

 

case2, case3 でそれぞれ帰着が再帰しちゃってる. このままだとだめ.

ただ, case2, case3 の停止性が自分自身に帰着してる場合は停止する, というのも case2-1とcase3-1両方でxの値は常に減少, なのでいつかは x<=y,z を満たし case1(停止) に帰着.

ここまでは割と楽勝, 厄介なのは case2, case3 の相互再帰する場合. むむむ,,, そうだ図を書いてみよう. せっかくホワイトボード買ったんだし ;-)

tarai_args_flow

おぉ, case2のy, case3のz は相互再帰において単に交換しあってるだけでそれぞれ値が不変ではないか!!
かつcase2,3におけるxは常に減少しつづける(再帰が往復して-1)ので, 有限回の相互再帰呼び出しで case2, case3 は x <= y,z に辿り着きcase1(停止)に帰着する.

 

 

停止性が証明できた?

恐らく, これでどのような計算木も網羅して停止することを証明したと思う. 思うのですが.. (思っちゃだめ..?) 間違ってたら ツッコミ お願いします. というかそのためのブログ :-)

追記 たらいは止まってなかった.

コメントにてつっこみがあり, 一番外側の f の停止性を示さなきゃだめでしょと. その通りだ…
ということで再思考中….

 

 

 

なにやら

皆さん一般化して考えたり, Coq を使って証明してたりする感じ. 面白い. ふーん, 一般化たらいは止まらないのか.

証明が知りたいのでとりあえず元論文を読みます.

 
Better Tag Cloud