《Lambda 函数演算简介》由 Henk Barendregt 和 Erik Barendsen 合著，这本著作是深入理解 Lambda 函数演算的基础读物。Lambda 函数演算是数学和计算机科学领域的一个核心概念，它起源于莱布尼茨的理想——创建一种“通用语言”来表述所有可能的问题，并找到解决这些问题的方法。该书分为多个章节，涵盖了从基本概念到高级主题的广泛内容。
第一章“引言”简述了 Lambda 演算的历史背景。莱布尼茨的理想在数学问题中得到了实现，即通过一阶谓词逻辑的形式化集合论来表述所有问题。然而，他的第二个理想——找到解决所有问题的决策方法，即著名的“Entscheidungsproblem（决定性问题）”，在1936年被Alonzo Church和Alan Turing分别用不同的方法否定。他们引入了计算模型来定义“可决定性”或等价的“可计算性”。
(1) Church 的贡献在于他发明了 Lambda 演算，这是一种形式系统，通过它定义了可计算函数的概念。
(2) Turing 提出了后来被称为图灵机的机器类，同样定义了可计算函数，通过这些机器。
Turing 进一步证明了 Lambda 演算和图灵机在定义可计算函数的能力上是等价的，奠定了现代计算机科学的基础。现代的冯·诺依曼计算机设计理念，以及诸如 Fortran、Pascal 等命令式编程语言和汇编语言，都是基于图灵机的工作原理，尤其是具有随机访问存储器的扩展。
第二章“转换”可能涉及 Lambda 表达式的重写规则，如 β-还原，这是 Lambda 演算中的关键操作，用于计算函数的应用。
第三章“Lambda 演算的力量”可能探讨了 Lambda 演算的表达能力和通用性，展示了它可以模拟各种数学和计算构造。
第四章“减少”深入介绍了 Lambda 演算中的计算过程，包括正常化和归约策略。
第五章“类型赋值”可能涉及了类型系统，这对于确保 Lambda 演算中的计算是安全和有效的至关重要。
第六章“扩展”可能涵盖了 Lambda 演算的变种和应用，如系统F和其他更复杂的类型理论。
第七章“减少系统”则可能讨论了不同类型的减少策略和演算系统，以及它们对 Lambda 演算性质的影响。
通过阅读这本书，读者不仅可以了解 Lambda 演算的基本概念，还能深入理解其在理论计算机科学和类型理论中的重要地位，以及它如何为现代计算机科学提供理论基础。Lambda 演算的精妙之处在于它的简洁性和表达力，它能够模拟任何可计算的过程，是理解计算本质的关键工具。
