English version
λ計算は Churchさんと Kleene さんが 1930 年代にこれを考えたと Wikipedia
(日本語
) にはある．彼らは最初これを数学の基礎を築こうとして考えたとある．
ところで私は素人なのであまりここに書いていることを鵜呑みにしないようにお願いする．これは私が理解する限りにおいての話である．この blog の元ネタはWikipedia
である．かっこ良く言えば，Wikipedia に inspire されて書いているのである．もし，あなたがこの Wikipedia の Page の内容をわかってしまったのであればこの blog よりももっと面白いものは沢山あるのでそちらをおすすめする．たとえば，「数学の基礎を築こうとしてλ計算は考えられた」で「なるほど，そうかそうか」，と思う人はこの blog を読む必要はない．しかし，「1930 年というと数学の歴史からするとかなり最近のことだ．どうしてこの時に数学の基礎なんてものを考えようとしたのだろう．いったい数学の基礎というのはなんなのだろう．ピタゴラスやアポロニウス，ユークリッドとかが数学の基礎を作ったりしたのではないのだろうか」とか思うのであればもう少し読んでもいいかもしれない．
数学の基礎というのは数学はどこから出発できるかということと，どういう出発ならば問題がないかという疑問に端を発っする．数学はある定義から出発する．これは人が決めるものである．まず，数学で最も基本的なものは何かと言うと数であろう．他にはある「命題」が真とか偽とかいう論理や，計算とは何かとかいうものも基本的である．こういうものはあまりにあたりまえすぎてかなり後の時代になるまで注目されなかった．
しかし，あたりまえのことに注目してどうするというのだろうか．数学者達はこの時，形式化ということについて考えるようになっていた．あたりまえに思える数であるが，たとえば，それは言語によって違うのかもしれない．日本語での 1と英語の 1 は本当に同じものだろうか? そこで数というものから定義しなおすことを考えた．ところで数を定義する時には数は使えない．もし使えると，「数とは数である」と書けば良くなってしまうからである．「愛とは愛である」「自意識とは自意識を自意識できるものである．」は真かもしれないが，こういう定義では数学の基礎としては使えないのである．数というものを数を使わないで定義できるのか? ここまでくると数学者は偏執狂かという感まである．
私がこの考えを面白いと思うのは，これが十分に形式化されているので，機械でそれを作って実行できるという点である．計算する機械を作ろうとすると，それをなんとかして物質(鉄とか水とか石とか)で作らなくてはいけない．Zaphod ならば 2つの頭で「わかるだろう，1 とか 2 とか 3 だよ，そういうのをとりあえず計算してみせる機械をちゃちゃっと作ってみてくれよ」と言うかもしれないが，どうやって 1 とか2を示せば良いのだろうか．数というのは驚くほど抽象化された概念である．抽象化されているというのは，非常に応用範囲が広いということである．「地球と人間とパンと信号機とZaphodの頭と教会の共通点は?」という問いに，「どれも数えられるものだ」という答えは正しい．繰り返しになるが，私には数をどうやって子供に教えたら良いのか見当がつかないのである．これは高度に抽象化された考えである．
λ計算の動機は数学の基礎を築くためにあった．というのは，それまであたりまえと考えられていた数や計算を形式化して1から考え直すということであったのだ．当時の数学者には数学のシステムの正しさを単純なルールだけで示すことが目的であったようだが，このルールは十分単純化されており，機械でも作れる．私がλ計算に興味を持ったのはこの「機械としても作れる」という所である．λ計算が現代の計算機言語の基礎理論の一つであるのはそういうわけである．
次回は数(自然数)を 1, 2, 3 などを使わずに定義してみよう．