1910 年的 Principia Mathematica 竟预言了 Lambda 演算

Principia Mathematica is modern and insightful

重读 1910 年出版的 Principia Mathematica，我惊讶地发现它读起来像是一本现代编程语言教材。Whitehead 和 Russell 在书中极具洞察力地探讨了 referential transparency、extensionality 以及 type 等现代概念，甚至早于 lambda-calculus 的正式提出就引入了 propositional functions。书中对 'any' 与 'all' 的区分暗示了 Intuitionism 的萌芽，而关于存在性证明必须提供具体 witness 的观点，更是与后来的构造主义不谋而合。尽管证明过程繁琐，但其核心思想——如 bound variables、alpha renaming 以及 descriptive functions 的定义——至今仍是计算机科学和逻辑学的基石。