λ 演算

本文是 λ 演算的介绍。

• 1. 什么是 λ 演算
• 邱奇编码

1. 什么是 λ 演算

λ 演算（lambda calculus，λ-calculus）是一套从数学逻辑中发展，以变量绑定和替换的规则，来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。它由数学家 阿隆佐·邱奇 在 20 世纪 30 年代首次发表。λ 演算作为一种广泛用途的计算模型，可以清晰地定义什么是一个可计算函数，而任何可计算函数都能以这种形式表达和求值，它能模拟单一磁带图灵机的计算过程；尽管如此，λ 演算强调的是变换规则的运用，而非实现它们的具体机器。^[1]

lambda 演算包括了建构 lambda 项，和对 lambda 项执行归约的操作。在最简单的 lambda 演算中，只使用以下的规则来建构 lambda 项：

语法	名称	描述
x	变量	用字符或字符串来表示参数或者数学上的值或者表示逻辑上的值
(λx.M)	抽象化	一个完整的函数定义（M 是一个 lambda 项），在表达式中的 x 都会绑定为变量 x
(M N)	应用	将函数 M 作用于参数 N，M 和 N 是 lambda 项

产生了诸如 λf.λx.(f (f x)) 的表达式。如果表达式是明确而没有歧义的，则括号可以省略。

为了方便理解和计算，我们在代码中使用 JavaScript 箭头函数来表示 lambda 演算中的抽象化和应用：

f => x => f(f(x))

例如：

(f => x => f(f(x)))(x => x + 1)(1) // 计算结果为 3

邱奇编码

邱奇编码（Church Encoding）

为了更方便地进行下面的讨论，我们可以给一个 λ 项命名，例如：

swap := λx.λy.y x

这等价于 JS 中的：

const swap = x => y => y(x)
swap(a)(b) // b(a)

那么

swap a b ≡ (λx.λy.y x) a b → b a

---

1. Λ 演算，维基百科，https://zh.wikipedia.org/wiki/Λ演算 ↩︎