1 历史与背景
1.1 邱奇与形式系统
阿隆佐·邱奇在20世纪30年代早期致力于构建一个统一的数学基础形式系统。受哥德尔不完备定理的启发，邱奇试图设计一种足够简单但表达力强大的符号系统，用以严格定义“有效可计算”的概念。λ演算最初作为这种探索的副产品诞生，其核心思想是将所有数学对象统一表达为函数，并通过函数抽象和应用两个基本操作完成一切计算。邱奇在1932年发表了相关论文，随后在1936年正式确立了λ演算的完整形式。
1.2 λ演算与可计算性
λ演算的提出直接推动了可计算性理论的形成。邱奇证明，λ演算能够表达一切可计算的函数——即任何直观上“能通过有限步骤机械地完成”的计算，都可以用λ项来表示。这一论断后来被称为邱奇论题。与此同时，邱奇还利用λ演算首次证明了停机问题的不可判定性：不存在一个通用的算法，能够判断任意λ项是否最终会归约到一个范式。
1.2.1 与图灵机的等价性（邱奇-图灵论题）
1936年，艾伦·图灵独立提出了图灵机模型，并证明了图灵机与λ演算在计算能力上是等价的。两者都能定义所有可计算函数，并且任何在一种模型中可定义的计算都能在另一种模型中模拟。这一等价性构成了邱奇-图灵论题的核心：任何直观上“有效可计算”的函数，都可以被λ演算或图灵机计算。这一论题至今未被证伪，成为计算机科学理论的基石之一。
1.3 早期争议与修正
λ演算在早期面临两项重大挑战。首先，邱奇最初的形式系统中包含一个被称为“邱奇的λ-K演算”的版本，允许自由地引入常量，但后来发现这会导致不一致性（如能定义出悖论）。其次，邱奇与图灵关于“计算本质”有过学术争论，但最终两人达成共识。此外，1935年斯蒂芬·克莱尼和J. B. 罗瑟指出了原始λ演算中某些替换规则的不严谨性，促使邱奇在后续工作中进行了修正，最终形成了今天标准化的无类型λ演算。
2 语法与基本概念
2.1 表达式（项）的构成
λ演算的语法极为简洁，只包含三类表达式（通常称为λ项）：
* 变量：如 x, y, z 等，表示一个参数或占位符。 * 抽象：形如 λx.M，表示将变量 x 绑定在表达式 M 中，定义了一个以 x 为参数的函数。 * 应用：形如 M N，表示将函数 M 应用于参数 N（即调用函数）。
2.1.1 变量（Variable）
变量是λ演算中最基本的元素，通常用小写字母表示。变量的含义完全由它在表达式中的出现位置决定——它可以是绑定变量（由λ抽象引入），也可以是自由变量（没有对应的λ抽象）。变量本身没有任何预定义的值，一切意义都由后续的归约操作赋予。
2.1.2 抽象（Abstraction，λx.M）
抽象是λ演算中构造函数的唯一方式。表达式 λx.M 的含义是：“对于任意参数 x，输出 M”。这里的 x 是形式参数，M 是函数体。例如，λx.x 表示一个恒等函数（输入什么就返回什么）。抽象使得函数的定义不再依赖函数名，完全由表达式本身替代。
2.1.3 应用（Application，M N）
应用是将函数应用于参数的操作。如果 M 是一个函数（通常是一个抽象），N 是其参数，则 M N 表示计算结果。应用遵循左结合规则，即 M N P 等价于 (M N) P。例如，(λx.x) y 的结果就是 y——将恒等函数应用于 y 得到 y。
2.2 自由变量与绑定变量
2.2.1 作用域规则
在抽象 λx.M 中，变量 x 在 M 中的所有出现都被称为“绑定”的，λx 的“作用域”就是整个 M。如果一个变量出现在表达式中的某个位置，但不在任何外层抽象的绑定范围之内，则称为“自由变量”。例如，在表达式 (λx. x y) 中，x 是绑定变量，y 是自由变量。
2.2.2 α-等价（重命名）
λ演算中，只改变绑定变量名称的表达式被认为是等价的，这就是α-等价。例如，λx.x 与 λy.y 是同一个函数，因为∀参数的行为相同。α-等价允许在不改变语义的前提下重命名绑定变量，这对于避免变量捕获（见后文）至关重要。
2.3 括号与约定（左结合、括号省略）
为了减少括号数量，λ演算采用了以下约定：
* 应用是左结合的：M N P 表示 (M N) P，而不是 M (N P)。 * 抽象的作用域尽可能向右扩展：λx. M N 表示 λx.(M N)，而不是 (λx.M) N。 * 连续抽象可缩写：λx.λy.λz.M 可简写为 λxyz.M。
这些约定使得复杂的λ表达式可读性大大提高。例如 λx.λy.x y 等价于 λx.(λy.(x y))。
3 归约与计算规则
3.1 β-归约（函数应用求值）
β-归约是λ演算的核心计算规则，它描述了如何执行一个函数应用。规则如下：
(λx.M) N → M[x := N]
其中 M[x := N] 表示将 M 中所有自由出现的变量 x 替换为表达式 N。例如，(λx. x x) y → y y（将 λx.x x 应用于 y，得到 y y）。如果 M 中没有 x 出现，则归约结果为 M（不变）。
3.1.1 替换（Substitution）与捕获避免
替换操作必须避免“变量捕获”，即防止被替换的表达式中的自由变量意外地被函数体的绑定变量捕获。例如，在执行 (λx.λy. x y) y 的β-归约时，若直接替换 y 到 λy.x y 中的 x 位置，会得到 λy.y y，其中新出现的 y 被内层的 λy 捕获，改变了原意。正确做法是先在需要替换的表达式上执行α-重命名：将 λy.x y 改为 λz.x z，然后再替换得到 λz.y z。
3.1.2 归一化顺序（最左最外 vs 最右最内）
β-归约的进行顺序有多种选择。最常用的两种策略是：
* 最左最外归约（Normal Order）：总是归约最左边、最外层的可归约子表达式（redex）。这种策略接近惰性求值（见后文）。 * 最右最内归约（Applicative Order）：总是归约最右边、最内层的可归约子表达式。这种策略接近严格求值。
对于某些λ项，不同的归约顺序可能导致不同的终止行为。规范化定理指出：如果一个λ项存在一个范式（即不能再归约的形式），那么最左最外归约一定能找到它。
3.2 η-归约与η-扩展
η-归约描述了函数外延性的概念：如果两个函数对于所有参数都有相同的行为，则它们相等。形式上，若 x 在 M 中不是自由变量，那么 λx.(M x) 可归约为 M。逆操作称为 η-扩展。η-归约常被用于消除冗余的包装函数，例如 λx. (sin x) 可归约为 sin（假设 sin 是基本函数）。
3.3 约简策略与强归一化
3.3.1 惰性求值与传名调用
惰性求值对应最左最外归约策略：只在需要时才计算参数的值，并且如果某个参数从未被使用，则永远不会被计算。这相当于编程语言中的“传名调用”（Call-by-name）。例如，若函数 f(x) = 1，则 f(complex_calculation()) 中的 complex_calculation 永远不会执行。
3.3.2 正则序 vs 应用序
* 正则序（Normal Order）：完全遵循最左最外归约，不预先计算参数。这是λ演算理论中的标准策略，保证能找到范式。 * 应用序（Applicative Order）：遵循最右最内归约，先计算参数的值再传给函数。大部分主流编程语言（如C、Python）采用类似应用序的策略（传值调用），但可能会导致某些表达式永远不会终止，即使正则序能终止。
强归一化性质指：对于所有λ项，所有归约顺序都会终止于一个唯一的范式。这在无类型λ演算中并不成立（不存在强归一化），但在简单类型λ演算中成立。
4 λ演算的威力：表达计算
4.1 丘奇编码（Church Encoding）
由于λ演算中只有函数，没有数字、布尔值等原生数据类型，这些概念必须通过函数来表示，这就是丘奇编码。
4.1.1 丘奇数（Church numerals）
丘奇将自然数n编码为一个接受两个参数 f 和 x 的函数，该函数将 f 应用于 x 恰好 n 次：
* 0 = λf.λx. x * 1 = λf.λx. f x * 2 = λf.λx. f (f x) * 3 = λf.λx. f (f (f x)) * ...
后继函数 succ = λn.λf.λx. f (n f x) 实现了加1操作。
4.1.2 布尔值、条件与运算
布尔值同样编码为函数：
* True = λx.λy. x （返回第一个参数） * False = λx.λy. y （返回第二个参数）
逻辑运算可以轻松实现： * and = λp.λq. p q p （若p为True则返回q，否则返回p即False） * or = λp.λq. p p q * not = λp. p False True
条件语句 if-then-else 其实就是布尔值本身：若条件为True，返回第一个分支；若为False，返回第二个分支。
4.1.3 元组与链表
元组（有序对）的编码如下：pair = λx.λy.λf. f x y，其中的第一个和第二个元素分别通过 fst = λp. p (λx.λy. x) 和 snd = λp. p (λx.λy. y) 提取。链表可以通过嵌套二元组实现，每个节点包含一个元素和指向下一个节点的指针。空列表编码为 False 或一个特殊标记。
4.2 递归与不动点组合子
4.2.1 Y组合子（Y combinator）
由于λ演算不允许函数直接引用自身（无名函数没有名字），递归需要通过不动点组合子实现。邱奇发现的Y组合子是其中最著名的：
Y = λf. (λx. f (x x)) (λx. f (x x))
Y组合子的性质是：Y f = f (Y f)，即它是任何函数f的不动点。这允许用递归方式定义函数：例如，阶乘可以定义为 Y factorial_definition，其中 factorial_definition 是递归定义的非递归版本。
4.2.2 Z组合子与严格求值
在应用序（严格求值）语言中，Y组合子会导致无限递归，因为 (x x) 会立即求值。此时需要使用 Z组合子（也称“严格化Y组合子”）：
Z = λf. (λx. f (λv. x x v)) (λx. f (λv. x x v))
Z组合子的核心改动是将对 (x x) 的调用包装在一个额外的λ中，从而延迟求值。这在模拟类似JavaScript、Scheme等严格求值语言中的递归时非常有用。
4.3 λ演算中的递归函数（阶乘、斐波那契）
利用丘奇编码和Y组合子，可以定义经典递归函数。例如阶乘的λ项定义（用丘奇数表示）：
fact = Y (λf.λn. isZero n 1 (mult n (f (pred n))))
其中isZero是判断丘奇数是否为零，pred是前驱函数，mult是乘法。斐波那契数列类似：
fib = Y (λf.λn. isZero n 0 (isZero (pred n) 1 (add (f (pred n)) (f (pred (pred n))))))
这些定义完全由纯λ项构成，不依赖任何外部数据结构。
5 类型化λ演算
5.1 简单类型λ演算（λ→）
5.1.1 类型规则与类型推导
简单类型λ演算（λ→）为λ项引入了类型标注，确保函数应用的类型安全性。基本类型规则如下：
* 变量 x : σ（如果x的类型是σ） * 若 M : τ，则 λx:σ. M : σ → τ（抽象规则） * 若 M : σ → τ 且 N : σ，则 M N : τ（应用规则）
类型推导根据这些规则自动判断项的类型。例如 λx:Int. x 的类型是 Int → Int。
5.1.2 强归一化性
简单类型λ演算的核心性质是强归一化：所有有类型的λ项无论采用何种归约顺序，都必然在有限步内归约到一个范式。这一性质意味着类型化λ演算中不存在无限递归，所有计算都会终止——但这也意味着它不能表达像Y组合子这样的通用递归，因此计算能力弱于无类型λ演算。
5.2 多态λ演算（System F / λ2）
5.2.1 参数多态与类型抽象
System F（也称二阶λ演算）引入了对类型的抽象，允许定义多态函数。例如，恒等函数可以定义为 Λα. λx:α. x，其中 Λα 表示对类型变量α的抽象。这个函数可以应用于任何类型实例化：如 (Λα. λx:α. x) [Int] 返回类型 Int → Int 的恒等函数。System F 的表达能力远超简单类型λ演算，能编码任意的递归数据类型。
5.2.2 与直觉主义逻辑的对应（柯里-霍华德同构）
柯里-霍华德同构揭示了类型系统与逻辑之间的深刻对应：
* 类型 ≈ 命题 * 项（证明）≈ 命题的证明 * 函数类型 σ → τ ≈ 蕴含式 σ ⇒ τ * 应用规则 ≈ 假言推理（Modus Ponens） * 类型抽象（System F）≈ 全称量化
因此，一个类型化的λ项就是一个直觉主义逻辑中的构造性证明。这使得类型系统成为形式化数学证明的工具。
5.3 依值类型与高阶类型
5.3.1 λP（依赖类型）
λP演算（也称作LF）允许类型依赖于值，即依赖类型。例如，类型 Vec n Int 可以是长度为n的整数向量，其中n本身是一个自然数值。依赖类型使类型系统能够表达诸如“数组访问不会越界”之类的性质，在形式上验证程序正确性。
5.3.2 类型论在证明助手中的应用（Coq、Agda）
依值类型和更高阶的类型系统构成了现代证明助手（如Coq、Agda）的基础。这些工具的核心是一个强类型的λ演算（通常基于 Curry-Howard 同构），允许用户编写代码的同时构造数学证明。例如，在Coq中，可以用λ项定义定理，计算过程即是证明过程。这启发了形式化验证在软件工程中的广泛应用，从操作系统内核到编译器都可以在证明助手中得到完全验证。
6 应用与影响
6.1 作为编程语言的理论基础
6.1.1 Lisp家族与λ表达式的实现
λ演算直接影响了Lisp语言（1958年由约翰·麦卡锡设计）的设计。Lisp中的 lambda 关键字直接借用了λ演算的符号，提供了匿名函数的定义机制。解释器和编译器中的求值策略、作用域规则（词法作用域 vs 动态作用域）以及闭包的概念，都可以追溯到λ演算的理论。后续的Scheme、Common Lisp、Clojure等都沿用了这一设计。
6.1.2 函数式编程的核心理念（纯函数、闭包）
函数式编程语言的三大核心理念均根植于λ演算：
* 纯函数：λ演算中的函数没有副作用，输出仅由输入决定，是现代函数式语言（如Haskell）的核心要求。 * 闭包：λ抽象可以捕获其环境中的自由变量，这一机制在λ演算中通过绑定变量的作用域自然实现。 * 高阶函数：函数可以接受其他函数作为参数或返回函数，正是λ演算中函数作为一等公民的体现。
6.2 在逻辑与范畴论中的角色
6.2.1 笛卡尔闭范畴与λ演算的模型
范畴论为λ演算提供了严格的数学模型。一个笛卡尔闭范畴（CCC）的结构恰好对应于简单类型λ演算的语法。具体地：
* 对象对应类型，态射对应函数（项）。 * 笛卡尔积对应元组/协变积类型。 * 指数对象 B^A 对应函数类型 A → B。 * 抽象和应用的范畴论操作与λ演算的规则一一对应。
这启发了Haskell等语言中类型类（Typeclass）与函子（Functor）等抽象概念的设计。
6.2.2 Curry-Howard-Lambek对应
将Curry-Howard同构扩展到范畴论，得到Curry-Howard-Lambek对应：直觉主义命题逻辑、类型化的λ演算和笛卡尔闭范畴三者是同构的。这揭示了逻辑、计算和数学结构的内在统一性，影响深远。
6.3 当代幽默与梗文化
6.3.1 "λ演算程序员才懂的梗"（如：所有函数都是λ）
在函数式编程社区中，有一种幽默的自嘲：“所有的函数都是λ，所有的递归都是Y组合子。”这种调侃源于λ演算的极端简洁：当你在Haskell中写 f x = x + 1，本质上就是在写 f = λx. x + 1。闭包、高阶函数、柯里化——一切皆λ。另一个经典梗是：“你只需要知道三件事：λ、λ和λ。” 此外，当程序员终于理解Y组合子时，往往会感慨“我看清了宇宙的真相”，然后发现自己仍然不会用它调试bug。
6.3.2 经典段子："如何用λ演算点一杯咖啡"
一个广为流传的段子描述了λ演算程序员的“真实点单”方式：只见他拿起菜单，看了一眼，然后对服务员说：“(λdrink. drink (λshot. shot (λsugar. sugar (λmilk. milk))))) (λx. x)”，服务员心领神会地点点头。这个段子的笑点在于：λ演算程序员把所有事物都看作函数，连“点咖啡”这个动作都被编码为一系列嵌套λ抽象，而真实的需求——拿铁咖啡（一剂浓缩、加糖、加热牛奶）——被嵌套在函数参数之中。最终服务员只能靠“外延等价”来理解（其实他只是猜）。这个段子也催生了“λ演算梗图”：一张λ表达式的图配上文字“这是我周末的计划”，或者“如何写一封情书：λyou.λme. forever”。