アロンゾ・チャーチ

チャーチはプリンストンの数学者で、1930年代初頭にラムダ計算を考案した。すべてを関数とみなし、計算を式の書き換えとする形式体系である。1936年春、彼はこれを用いて決定問題に解がないことを示した。チューリングも同じ年にまったく別のモデルで同じ結論に達し、1936年から1938年までチャーチの博士課程の学生となった。二つの体系は、計算できるものが完全に一致することが分かった。これが今日のチャーチ=チューリングのテーゼである。

ラムダ計算は証明の中にとどまらなかった。1940年の単純型付きの変種は、その後のあらゆる型システムの祖先であり、LISP、ML、Haskell、さらにC++、Java、Pythonにまで広がったラムダ式は、すべてチャーチの無名関数の記法の直系である。

教え子の顔ぶれは、もしかすると業績より大きな遺産かもしれない。チューリング、クリーネ、ロッサー、ダナ・スコット、マイケル・ラビン、レイモンド・スマリヤンらだ。几帳面さは逸話になるほどで、すでに綺麗な黒板でも、書く前に洗ったという。1936年には『Journal of Symbolic Logic』を創刊し、以後40年間その面倒を見続けた。