λ演算与组合子：编程语言理论基础

"Lambda-Calculus and Combinators，an Introduction" 本书主要介绍λ-演算与组合逻辑这两种逻辑系统，它们既是抽象的编程语言，也是描述程序如何修改其他程序的一般性质的工具，不受具体实现细节的干扰。λ-演算由美国逻辑学家阿隆佐·丘奇在1930年代左右发明，作为包含高阶操作符的综合逻辑系统的一部分，这些操作符作用于其他操作符。λ-演算的语言或等价符号是大多数高阶逻辑和计算机编程语言的关键组成部分。实际上，最早发现的不可计算问题并非通过图灵机描述，而是用λ-演算来表述的。 组合逻辑与λ-演算有着相同的目标，可以表达相同的计算概念，但其语法规则更为简单。这个基本思想最初由莫西·舒昂芬克尔在1920年提出，哈斯凯尔·柯里在七年后独立重新发现并将其发展成可行的技术。 本书的目标是引导读者了解这两个领域的基本方法和结果。预期读者对命题逻辑、谓词逻辑和递归函数有一定了解，并具备数学归纳法的经验。书中有练习题，大部分带有标记（*）的答案在书末的附录中给出。早期章节还有额外的练习题，供需要更多常规练习的读者使用。 书中详细讨论了组合逻辑和λ-演算的语法及基本性质，随后引入了类型理论。介绍了有类型和无类型的版本以及它们之间的差异。还深入讲解了λ-演算模型，这些模型在编程语言的语义基础中起着关键作用。 作者尽量以非技术性的手法阐述主要思想，并通过示例进行说明。书中包含大量练习题，涵盖从基础到挑战性的各种难度，以帮助读者巩固理解。这本书不仅是对λ-演算初学者的重要参考，而且经过全面修订，确保了内容的最新性，适合现代编程语言研究者和开发者阅读。