形式陈述

项由语法 $t::=x\mid \lambda x.t\mid tt$ 生成。核心计算规则是 β-归约：

$$(\lambda x.t)s{\to }_{\beta }t[x:=s],$$

即把函数体中自由出现的 $x$ 替换为实参项 $s$，同时避免变量捕获。这是无约束的 β-归约；调用值策略才额外要求实参先成为值。

直觉

函数就是值，计算就是把实参代入函数体。极少的语法足以编码布尔值、自然数、递归和数据结构。

例子与边界

$(\lambda x.x)y\to y$。项 $(\lambda x.xx)(\lambda x.xx)$ 会无限归约，说明无类型 λ 演算不保证终止。

推论与应用

λ 演算是函数式编程、操作语义、类型系统和 Curry–Howard 对应的共同基础。

参考资料

• Henk Barendregt, The Lambda Calculus: Its Syntax and Semantics, revised ed.
• Benjamin C. Pierce, Types and Programming Languages, Chapter 5.