Lambda Calculus基础：Henk Barendregt与Erik Barendsen

"introduction to lambda calculus.Henk Barendregt Erik Barendsen" 《Lambda Calculus简介》由Henk Barendregt和Erik Barendsen撰写，这是一本介绍lambda演算的书籍，修订版发布于1998年12月和2000年3月。Lambda演算是数学领域中的一个重要概念，与函数计算和逻辑理论密切相关。 Lambda演算（Lambda Calculus）是逻辑和计算机科学的基础之一，由数学家阿尔弗雷德·诺斯·怀特海德和伯特兰·罗素在发展类型理论时引入，后来由阿隆佐·丘奇进一步发展，用来解决莱布尼茨的理想：创建一种通用语言来表述所有问题，并找到解决这些问题的方法，即所谓的“决定问题”（Entscheidungsproblem）。 本书的章节结构如下： 1. 引言 - 阐述了lambda演算的历史背景，包括莱布尼茨的理想以及与决定问题的关系。 2. 转换 - 介绍了lambda演算中的主要操作，包括函数的应用和α转换、β转换、η转换等，这些转换规则是lambda演算的核心。 3. Lambda的力量 - 解释了lambda演算的强大之处，它可以表达任何可计算函数，形成了计算的普遍模型。 4. 归约 - 详细讨论了函数应用的过程，即归约，包括正常形式、平凡归约和最左归约等策略。 5. 类型赋值 - 介绍了类型系统，用于确保lambda表达式的正确性，防止类型错误，如Church-Rosser定理和λ-可类型性。 6. 扩展 - 探讨了lambda演算的扩展，包括附加的构造或规则，如组合子逻辑和类型理论的其他形式。 7. 归约系统 - 讨论了不同类型的归约系统，如简单归约和强归约，它们影响lambda表达式的计算行为。 8. 参考文献 - 列出了相关的学术资料，供读者进一步研究。 通过阅读这本书，读者将深入理解lambda演算的基本原理、操作规则以及它在理论计算机科学中的应用。Lambda演算不仅对理论研究具有重要意义，还在实际编程语言设计中起着重要作用，如Lisp、Haskell等函数式编程语言就深受其影响。