Alonzo Church アロンゾチャーチ

アロンゾ・チャーチ（Alonzo Church, 1903–1995）は、計算のエンジンを設計した論理学者です。

1. ラムダ計算（lambda-calculus）の創始

1930年代、チャーチは数学的な「関数」を極限まで抽象化した ラムダ計算 を考案しました。

• 「変数」と「関数」の等価性： 彼は、あらゆる計算が「変数の置き換え（ベータ簡約）」だけで記述できることを証明しました。
• 宇宙の最小単位： チャーチは宇宙のあらゆる事象を「関数への入力と出力」という最小限の論理形式に圧縮しました。

2. チャーチ＝チューリングのテーゼ

チャーチは、教え子であったアラン・チューリングとともに、「計算可能性」の限界を定義しました。

• 思考の限界： 「アルゴリズム（計算手順）で解ける問題とは何か？」という問いに対し、ラムダ計算で記述できるものこそが計算の本質であると断じました。

3. 単純型理論（Simple Theory of Types）と HOL

チャーチの最大の功績の一つは、ラムダ計算に 「型（Type）」 を導入したことです。

• 階層の秩序： 無秩序な関数に「型」というラベルを貼ることで、論理的な矛盾（パラドックス）を排除しました。
• 高階論理の完成： これにより、個体（一階）から述語（二階）、さらにその上の階層（高階）へと、Mathematical Descent（降下）の階段がシステマチックに整備されました。