English version
Peano の定理で重要だったのは Successor 函数であった.覚えているだろうか.次の数を作るという函数である.実際に SUCC1 という機械の手順を既に説明した.
何が数かという意味で数を定義する際,全部の数を並べることで数を定義してもかまわない.しかし数学者は怠けることが仕事であるし,無限のものを並べるのはたいへん難しい.こういう問題に対して数学者は最初の数と「次の数を出すもの」を作って,あとはそれぞれの人に適当にしてもらうことをする.具体的な数1,2,3, ... をそのまま使うのではなく,「数」というものの性質を抽象化してそれを数の定義にするのだ.抽象化の話は覚えているだろうか?
「次の数」を作るもの,そういうものは函数であるのでλである.最初の数とこのようなλがあれば,全部の数が出せるはずだ.自動販売機gensym3141は,自動販売機を入れると,次の自動販売機を出す自動販売機(自動販売機6931471805)も売っている.自動販売機 1 は「ニシン販売機」であり,自動販売機 2 は「サンドイッチ販売機」であり,自動販売機 3 は「ニシンサンドイッチ販売機」である.自動販売機6931471805 は自動販売機 1 を入れると自動販売機 2 を出す販売機である.これはまた,自動販売機 2 を入れると自動販売機 3 出す.じゃあ,自動販売機6931471805 を入れるとどうなるか,もちろん自動販売機6931471806 を出すに決まっている.これは数ある自動販売機の一種に過ぎないが,次の自動販売機を出す自動販売機は知的生命体には特別なのものとして感じるので,SUCC と呼んだりする.それはこんな形のλとして書くことができる.
SUCC := λn f x. f (n f x)
多分 Wikipedia を読んだ人は,このλ式を適用しようとしただろう.で,簡単に適用できた人はここから先を読む必要はない.私はできなかったので一週間考えてしまった.それで,多分こうだろうというのがわかったので,この文章を書いている.Wikipedia の補足のようなものだが,もし実際に適用してみたい人にはきっと面白いだろう.