λ 演算

定义

λ 演算(Lambda Calculus)是 Alonzo Church 在 20 世纪 30 年代提出的形式计算系统,只包含三种构造:变量、函数抽象(λx.M)与函数应用(M N)。尽管极度精简,它与图灵机计算能力等价,是可计算性理论的两大基石之一。

原理

计算通过 β-归约进行:把实参代入函数体中被绑定的变量。α-变换处理绑定变量重命名,η-变换刻画函数外延相等。归约顺序的不同对应不同求值策略,如正则序与应用序,分别启发了惰性求值与严格求值。

扩展

无类型 λ 演算之上发展出简单类型 λ 演算、System F(多态 λ 演算)、构造演算等类型化系统,构成现代类型理论与证明助手的骨架。

影响

Lisp、ML、Haskell 等函数式语言直接以 λ 演算为核心模型;主流语言中的"lambda 表达式"命名亦源于此。它同时是编程语言语义研究的标准工具。