Lambda 演算

Lambda 演算是可计算函数的理论，即一个形式系统，它形式化了可计算函数的抽象概念。该演算由阿隆佐·丘奇在 1930 年代开发，当时其他研究人员也开发了其他计算模型，这些模型后来被证明是等效的。S. C. 克莱尼开发了递归函数，艾伦·麦席森·图灵开发了一种通用抽象机器，后来被称为通用图灵机，以及其他形式系统。递归函数可以在 lambda 演算中表达，反之亦然，通用图灵机也可以在 lambda 演算中定义，递归函数和 lambda 演算可以在通用图灵机中定义，其他未在此处描述的计算模型也是如此。每次尝试构建一个系统来捕捉计算概念的结果都是一个等效的理论，这是一个强烈的迹象，表明不存在其他“更强大”的系统，这无法被证明，因此被称为丘奇-图灵论题。换句话说，它指出任何可计算函数都可以在这些系统中的任何一个中被定义。你可能注意到形式系统、理论和模型用于指代这些形式主义，让我们说一下这意味着什么。形式理论是一个形式系统，它捕捉了可计算函数的抽象概念。

Lambda 演算是计算机科学的一个基础，就像微积分是牛顿物理学的基础一样。另一个基础是冯·诺依曼机，它是通用图灵机的硬件实现，当然作为任何物理实现，它具有有限的内存。

Lambda 演算作为函数式编程语言的基础，就像冯·诺依曼机是命令式编程语言的基础一样。

计算机科学中一个重要的主题是编程语言的语义，即如何说明编程语言的含义。Lambda 演算是丹娜·斯科特开发的指称语义的基础。

在 lambda 演算中研究了不同的 lambda 理论。无类型 lambda 演算导致了一个不一致的理论，因为存在一个等价于朴素集合论中罗素悖论的悖论。这促使人们开发了有类型 lambda 理论。

无类型 lambda 演算公式是从一个无限的变量集 $x,y,z,\ldots ,x_{0},y_{0},z_{0},\ldots$、形式为 $\lambda v.M$ 的抽象，其中 $v$ 是一个变量，而 $M$ 是 lambda 演算公式，也称为 lambda 项，最后一个是形式为 $(MN)$ 的应用，其中 $M$ 和 $N$ 也是 lambda 项，仅此而已。

存在转换规则，$\alpha ,\beta$ 和 $\eta$ 定义如下

目录

1. 语法
2. 等价公式