不动点组合子与递归

形式陈述

给定函数 $f$ ，若 $x=f(x)$ ，则 $x$ 是 $f$ 的不动点。不动点组合子则是一个闭合 λ 项 $\Phi$ ，它对任意项 $f$ 都满足

\Phi f =_\beta f(\Phi f),

也就是 $\Phi f$ 经有限次β-归约可与 $f(\Phi f)$ 相互转换。Curry 的 $Y$ 组合子为

Y\equiv\lambda f.(\lambda x.f(x\,x))(\lambda x.f(x\,x)).

对任意 $f$ ，取对 $f$ 新鲜的 $x$ ，记 $M_f=\lambda x.f(x\,x)$ 。完整 β-归约给出

\begin{aligned} Yf &\to_\beta M_fM_f \to_\beta f(M_fM_f),\\ f(Yf)&\to_\beta f(M_fM_f). \end{aligned}

两边有共同归约结果，所以 $Yf=_\beta f(Yf)$ ；这里不是把 $M_fM_f$ 与 $Yf$ 当成字面相同，也没有声称 Curry 的这个 $Yf$ 沿纯收缩步骤直接变成 $f(Yf)$ 。这个等式只保证组合子产生一个不动点，不保证 $f$ 的不动点唯一，更不保证任意求值策略都能算出它。正常序可先展开最外层的 $f$ ；传值调用却会在把参数交给 $f$ 前不断求值 $M_fM_f$ 。适合传值求值的一个变体是

Z\equiv\lambda f.(\lambda x.f(\lambda v.x\,x\,v)) (\lambda x.f(\lambda v.x\,x\,v)).

记 $N_f=\lambda x.f(\lambda v.x\,x\,v)$ 。对已经是值的 $f$ ，传值求值的两步是

Zf\to_v N_fN_f\to_v f(\lambda v.N_fN_f\,v).

递归参数 $\lambda v.N_fN_f\,v$ 已是值，下一次自展开被推迟到它真正接收实参时。这是延迟的传值递归接口；若再允许适当的函数 η 等式，可把延迟包装与其外延行为联系起来，但不能把这个 $Z$ 的条款直接冒充开头不含 η 的一般 β-不动点方程。

直觉

递归定义常写成“函数在函数体里调用自己”，但这里没有函数名可供自引用。组合子改写问题：先把递归体写成一个接收 self 的普通高阶函数 $g$ ，再寻找满足 $h=g(h)$ 的函数 $h$ 。 $Yg$ 正是这样的 $h$ 。自应用 $x\,x$ 并不是递归业务逻辑，而是一套把当前生成器重新送回自身的布线装置。

这种构造揭示了语法递归与语义不动点的联系，却没有把二者合并。 $Y$ 是无类型 λ 演算中的项；最小不动点语义则在带序的语义域中选择由有限近似得到的最小解。前者提供递归表达式，后者解释递归方程为何代表特定程序含义。

例子与边界

把阶乘的递归体写成

G\equiv\lambda self.\lambda n. \mathsf{if}\;(n=0)\;\mathsf{then}\;1\;\mathsf{else}\;n\cdot self(n-1).

在正常序下， $YG$ 先展开为 $G(M_GM_G)$ ，其中 $M_GM_G$ 再现相同的递归展开；因此 $(YG)\,3$ 只在进入非零分支后才继续展开下一层 $YG$ ，最终得到 $6$ 。同一个 $Y$ 直接放进严格语言时，运行会困在自应用的无限展开中，尚未进入 $G$ 的条件分支；改用 $ZG$ 才把这次展开藏到参数 λ 后面。

类型边界同样关键。若某个满足开头 β-方程的闭组合子 $\Phi$ 在纯简单类型 λ 演算中有类型 $(A\to A)\to A$ ，在上下文 $f:A\to A$ 下，强正规化使 $\Phi f$ 归约到某个 β-正规形 $n$ 。由不动点方程和合流性， $n$ 必须与 $f\,n$ 有相同正规形；但 $f$ 是变量， $f\,n$ 本身已经正规，有限语法树 $n$ 不可能与多了一个外层应用的 $f\,n$ α-等价，矛盾。不能仅从 $\Phi I=_\beta I(\Phi I)$ 就断言有无限运行，因为对恒等函数 $I$ ，任何项都满足这条可转换等式。因此纯简单类型系统不能给这样的组合子定型；带一般递归的语言必须加入固定点原语、递归类型或其他足以打破该终止结论的机制。

推论与应用

不动点组合子说明“递归”不是无类型函数计算必须额外假设的语法能力：只靠抽象、应用和自应用就能编码递归。它也让传名调用与传值调用的差别变得可观察——二者共享 β-规则，却对先展开函数体还是先求实参作出不同选择。

在编程语言中，具名 let rec 或 fix 通常比直接展开 $Y/Z$ 更适合作为源语言构造，因为实现可以分配递归闭包并保留清晰的调试信息。证明递归程序性质时，还需另行给出终止度量、归纳原理或域论解释；组合子本身只建立递归方程，不自动提供终止性、唯一性或最小性。

参考资料

H. B. Curry and Robert Feys, Combinatory Logic, Vol. I, North-Holland, 1958，fixed-point combinators。
Henk Barendregt, The Lambda Calculus: Its Syntax and Semantics, revised ed., North-Holland, 1984，fixed-point combinators and reduction strategies。
Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，untyped recursion and typed fixed-point operators。

形式陈述 ​

反向链接

形式陈述