λ演算

λ演算（也写作λ-calculus）是数学逻辑中的一个形式系统，用于表达基于函数抽象和应用的计算，使用变量绑定和替换。 它是一种通用计算模型，可用于模拟任何图灵机。 它由数学家阿朗佐丘奇在 1930 年代引入，作为他对数学基础研究的一部分。

λ演算包括构造 § lambda 项并对它们执行 § 缩减操作。 在最简单的 lambda 演算形式中，项仅使用以下规则构建：

• x {\displaystyle x} – 变量，表示参数或数学/逻辑值的字符或字符串。
• ( λ x . M ) {\textstyle (\lambda x.M)} – 抽象，函数定义（M {\textstyle M} 是一个 lambda 项）。 变量 x {\textstyle x} 在表达式中绑定。
• ( M N ) {\displaystyle (M\ N)} – 应用程序，将函数 M {\textstyle M} 应用于参数 N {\textstyle N} 。 M {\textstyle M} 和 N {\textstyle N} 是 lambda 项。

减少操作包括：

• ( λ x . M [ x ] ) → ( λ y . M [ y ] ) {\textstyle (\lambda x.M[x])\rightarrow (\lambda y.M[y])} – α -转换，重命名表达式中的绑定变量。 用于避免名称冲突。
• ( ( λ x . M ) E ) → ( M [ x := E ] ) {\textstyle ((\lambda x.M)\ E)\rightarrow (M[x:=E])} – β-reduction，用抽象主体中的参数表达式替换绑定变量。

如果使用 De Bruijn 索引，则不再需要 α 转换，因为不会发生名称冲突。 如果减少步骤的重复应用最终终止，那么根据 Church-Rosser 定理，它将产生 β-正规形式。

如果使用通用的 lambda 函数（例如 Iota 和 Jot），则不需要变量名，它们可以通过以各种组合调用自身来创建任何函数行为。

λ演算是图灵完备的，也就是说，它是一个通用的计算模型，可以用来模拟任何图灵机。 与它同名的希腊字母 lambda (λ) 在 lambda 表达式和 lambda 术语中用于表示绑定函数中的变量。

λ演算可以是无类型的或有类型的。 在类型化 lambda 演算中，只有当函数能够接受给定输入的数据类型时才能应用函数。 有类型的 lambda 演算比无类型的 lambda 演算弱，这是本文的主要主题，因为有类型的 lambda 演算可以表达的比无类型的演算少，但另一方面，有类型的 lambda 演算可以证明更多的东西 ; 例如，在简单类型的 lambda 演算中，它是一个定理，即每个评估策略都会针对每个简单类型的 lambda 项终止，而无类型 lambda 项的评估不需要终止。 有许多不同类型的 lambda 演算的原因之一是希望在不放弃能够证明关于微积分的强定理的情况下做更多（无类型演算可以做的事情）。

λ演算在数学、哲学、语言学和计算机科学的许多不同领域都有应用。 λ演算在编程语言理论的发展中发挥了重要作用。 函数式编程语言实现了 lambda 演算。 λ演算也是范畴论当前的一个研究课题。

lambda 演算由数学家 Alonzo Church 在 1930 年代引入，作为对数学基础研究的一部分。 1935 年，斯蒂芬·克林 (Stephen Kleene) 和 J. B. 罗瑟 (J. B. Rosser) 提出了克林-罗瑟悖论，证明原始系统在逻辑上是不一致的。

随后，丘奇在 1936 年分离并发表了与计算相关的部分，即现在所谓的无类型 lambda 演算。 1940 年，他还引入了一种计算能力较弱但逻辑一致的系统，称为简单类型 lambda 演算。

直到 1960 年代它与编程语言的关系被阐明之前，lambda 演算只是一种形式主义。

由于 Richard Montague 等语言学家在自然语言语义学上的应用，lambda 演算开始在语言学和计算机科学中享有重要地位。

Church 使用希腊字母 lambda (λ) 作为 lambda 演算中函数抽象符号的原因尚不确定，部分原因可能是 Church 自己的解释相互矛盾。 根据 Cardone 和 Hindley (2006)：

顺便问一下，丘奇为什么选择符号“λ”？ 在 [一封未发表的 1964 年写给 Harald Dickson 的信中]，他明确指出它来自怀特海和罗素用于类抽象的符号“ x ^ {\displaystyle {\hat {x}}} ”，首先修改“ x ^ {\displaystyle {\hat {x}}} ” 到 “ ∧ x {\displaystyle \land x} ” 来区分函数。