λ演算中的不动点定理 我们先从λ演算中的基本概念开始。λ演算是一种形式系统，用于描述函数定义、函数应用和递归。它的表达式（称为λ项）由变量（如x）、抽象（如λx.M，表示函数定义）和应用（如M N，表示将函数M应用于参数N）构成。 接下来需要理解的是λ演算中的替换操作。当函数应用(λx.M)N发生时，我们需要将M中所有自由出现的x替换为N，这个过程称为β归约。例如(λx.xy)N会归约为Ny。但替换时需要小心变量捕获的问题，这通过α转换（重命名绑定变量）来避免。 现在我们来探讨一个关键概念：组合子。组合子是不含自由变量的λ项。特别重要的是不动点组合子——一个能够为任意函数找到不动点的λ项。具体来说，如果Y是一个不动点组合子，那么对于任意函数F，都有YF = F(YF)，这意味着YF是F的一个不动点。 最著名的不动点组合子是Y组合子：Y = λf.(λx.f(xx))(λx.f(xx))。让我们验证其不动点性质：对任意F，有YF = (λx.F(xx))(λx.F(xx)) = F((λx.F(xx))(λx.F(xx))) = F(YF)，确实满足不动点的定义。 λ演算中的不动点定理指出：在无类型的λ演算中，每个项F都有一个不动点，即存在项X使得FX = X。这个定理的证明就是通过构造Y组合子来实现的——Y就是这样一个"不动点发现器"。 这个定理的重要性在于它使得在λ演片中定义递归函数成为可能。例如，我们可以定义阶乘函数fact = Y(λf.λn.if n=0 then 1 else n×f(n-1))。通过不动点性质，fact会展开为真正的递归计算过程。 最后，不动点定理揭示了λ演算的表达力——尽管系统本身很简单，但通过不动点组合子，它能够表达所有的可计算函数，包括递归函数，这为理解计算本质和程序语言语义提供了理论基础。