CSの授業でもやると思うんだけど少し歴史をおさらいしよう。以下、長いので２回に分ける。
微積分や複素解析の発展とともに解析の基礎が数学の大きな問題となった時期があった。
その時期に活躍したのがデデキントとカントールだ。デデキントはまず実数をデデキント切断を導入して定義し、
続いて整数を公理論的に定義した。この時、五つほどの公理から推論されるように定義した。
この定義には無限集合という罠があることがカントールから指摘され、集合論を厳密に定義することが問題になった。
これに答えたのがフレーゲやラッセルだった。
ラッセルはプリンキピア・マセマティカのなかで算術を説明するためにΛ「ラムダ」記号を導入した。
このラッセルの仕事を受けてゲーデルが不完全性定理を証明した。
この仕事でゲーデル独特の定理証明機とゲーデル数による計算可能関数を導入している。
さらにゲーデルの仕事を受けて、アロンゾ・チャーチとチューリングが登場する。
チャーチはラッセルのΛをさらに洗練させたラムダ算法を構築してλ記号を導入し、
ゲーデルの計算可能関数がλ記述可能関数と同等であることを示した。
チューリングはチューリング機械を導入して、ゲーデル＆チャーチと同様に
計算可能関数が再帰関数と同等であることを示し、チューリング完全という概念を得た。
今日の一般的なプログラミング言語はチューリング完全で、ゲーデル＆チャーチ＆チューリングの仕事を基礎にしている。