たらいまわし関数の停止性
>
>http://www.kmonos.net/wlog/61.html#_1445060501
> 記憶が曖昧&探しても出てこなかったのですが、竹内先生の何かの発表資料で「たらいまわし関数は実はこんな関数」という定義が説明されていたと思いました。それこそ
>
>if x < y then y else if y < z then z else x
>
>みたいな、いや正式には覚えていないのでいいかげんですがそんな感じの大小比較があってそれぞれの条件にしたがって x か y か z が返る関数。その定義をたらいまわし関数の定義である
>
>tak x y z | x <= y = y
| otherwise = tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) z y) > >に当て嵌めてみると、確かにそれが成立するとゆー。で、 tak は↑のように定義されているので、ある f があって f が↑の性質を満たしているわけですから、 tak は f であって、どんな引数であっても x か y か z のどれかを大小関係に応じて返す、ということになります。 > >どこで見たんだったかなぁ。 >
| otherwise = tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) z y) > >に当て嵌めてみると、確かにそれが成立するとゆー。で、 tak は↑のように定義されているので、ある f があって f が↑の性質を満たしているわけですから、 tak は f であって、どんな引数であっても x か y か z のどれかを大小関係に応じて返す、ということになります。 > >どこで見たんだったかなぁ。 >