Church 数のメモ - つづき。

しかし、ここでの特徴は、「普通の数値に戻す」ことではなくて、「関数をそのまま数として扱う」ということにある。これで、数そのものの「作り方」はわかったが、そこから任意の数を作るための「演算」はどうしたらよいのだろう?

例えば、自然数は、次の数を求める一般的手法が一つあれば、あとはドミノ倒し式に作れる。「1は0の次、2は1の次....」といった具合である。次の数を求める関数をSUCCと名付けると、SUCCの定義はこんな風になる。

SUCC := λ n f x . f(n f x)

数の定義は一応かたがついたけど、10000 とかを定義するには 10000 回 f を書かないといけないし、後々演算とか負数を定義しなければいけないので、SUCC(後者)関数は当然必要になってくるよなーと考えていたら、さすが、ちゃんと書いてました。確かに後者を返します。
で、ちょっと疑問なんですが、この SUCC は引数を 3 つ取る関数だけど、単に数の後者を与えるという意味からいくと、引数は 1 つ(SUCC を取る数)であるべきじゃないのかなと。と、つらつら考えてましたが、よく分からず。修行が足りん。