一般たらいまわし関数の停止性証明解説

CS

えーと、

とかtweetしたのでやります。論文のフルバージョンはこちら→[1007.0467] Notes on higher-dimensional tarai functions。全部だと10ページ超えていますが、停止性だけなら最初の5ページくらいで終了です。

一般たらいまわし関数の定義と背景に関してはd.y.d.を参照のこと。もうずいぶん前ですねぇ。
これの何が難しいかって、基本的にはただひとつ。x[1]>x[2]の場合に外側のtが停止することをどういうか、ということです。そのためには、まだ停止することすらわかっていない関数tの値を把握しなければいけません。
xを整数n個からなる組とします。x[1]>x[2]として、この場合の外側のtに与えられるのはどのような引数かを考えます。
任意のi=1,...,nに対して、y_i=(x[i]-1, x[i+1], ..., x[n], x[1], ..., x[i-1])と定義します。すると、t(x)=t(t(y_1), t(y_2), ..., t(y_n))となるわけですね。さて、t(y_i)に関しては何がわかっているでしょうか？
まあ、この時点ではほぼ何もわかってないわけですが、まず確実なのは、x[i]-1<=x[i+1]ならば、y_i[1]<=y_i[2]となるのでt(y_i)=x[i+1]になるってことです。
それ以外に関しては、まあ多分t(y_i)<=max y_i<=max xくらいはいえているだろうと。max x=max{x[1], ..., x[n]}ってことでよろしくどうぞ。これは証明が必要ですが、直感的に見てtの定義には1を引くこと、ローテーションすること、値を取り出すことしか使われていないので、組の中に出てくるものより大きくなるってのは変ですよね。というわけで、それを仮定しておきます。
さてと、max x=x[j]となるような最小のjをとっておきます。すると、全てのi=1,...,nに対してt(y_i)<=x[j]かつt(y_{j-1})=x[j]が言えているので、t(x)=t(<=x[j], <=x[j], ..., <=x[j], x[j], <=x[j], ..., <=x[j])って形になるわけですね。ここで、x[j]が出てくる位置は、j-1番目です。
z[i]=t(y_i)と置きましょう。すると、z[j-1]=x[j]=max zになります。ということは、maxが出てくる場所がひとつ前に動いたということです。だったら、maxが出てくる位置を使って帰納法してやればいいじゃないか！

アイデアとしてはこれで終了です。この議論自体は穴と間違いだらけなんですが、それを埋めたり修正したりしてあげればあの証明が出てきます。もう夜遅いし、どこが穴でどこが間違いかは練習問題ということで。