不动点组合子与递归

形式陈述 ​

给定函数公理库函数Function · Map · Mapping由定义域、陪域和单值图共同组成，并把每个输入送到唯一输出的映射。 $f$，若 $x=f(x)$，则 $x$ 是 $f$ 的不动点。不动点组合子则是一个闭合 λ 项 $\mathrm{\Phi }$，它对任意项 $f$ 都满足

$$\mathrm{\Phi }f{=}_{\beta }f(\mathrm{\Phi }f),$$

也就是 $\mathrm{\Phi }f$ 经有限次β-归约公理库β-归约Beta reduction把函数抽象应用于实参时用无捕获替换消去应用的核心归约规则。可与 $f(\mathrm{\Phi }f)$ 相互转换。Curry 的 $Y$ 组合子为

$$Y\equiv \lambda f.(\lambda x.f(xx))(\lambda x.f(xx)).$$

对任意 $f$，完整展开为

$$\begin{array}{rl}Yf& {\to }_{\beta }(\lambda x.f(xx))(\lambda x.f(xx))\\ & {\to }_{\beta }f((\lambda x.f(xx))(\lambda x.f(xx)))=f(Yf).\end{array}$$

这个等式只保证组合子产生一个不动点，不保证 $f$ 的不动点唯一，更不保证任意求值策略都能算出它。正常序可先展开最外层的 $f$；传值调用公理库传值调用Call by value · CBV仅当实参先求值为值后才进行函数体替换的求值策略。却会在把参数交给 $f$ 前不断求值 $M_f{M}_f$。适合传值求值的一个变体是

$$Z\equiv \lambda f.(\lambda x.f(\lambda v.xxv))(\lambda x.f(\lambda v.xxv)).$$

对已经是值的 $f$，$Zf$ 可求值到 $f(\lambda v.Zfv)$；额外的 λ 抽象把下一次自展开推迟到递归函数真正接收参数时。这是传值语义下的延迟不动点性质，不应与 $Yf\to f(Yf)$ 的正常序展开逐步混写。

直觉 ​

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

这种构造揭示了语法递归与语义不动点的联系，却没有把二者合并。$Y$ 是无类型 λ 演算公理库λ 演算Lambda calculus · Untyped lambda calculus只用变量、函数抽象和函数应用表达计算的极简形式系统。中的项；最小不动点语义公理库最小不动点语义Least-fixed-point semantics · Least fixed point semantics · Kleene fixed-point semantics以递归定义的有限展开链之上确界选取不凭空加入行为的最小语义解。则在带序的语义域中选择由有限近似得到的最小解。前者提供递归表达式，后者解释递归方程为何代表特定程序含义。

例子与边界 ​

把阶乘的递归体写成

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

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

类型边界同样关键。若一般不动点组合子在简单类型 λ 演算中有类型 $(A\to A)\to A$，取恒等函数即可构造良类型的无限展开项，这与简单类型 λ 演算的强正规化公理库简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个有类型的简单 λ 项的所有 β-归约序列都有限并到达正规形。矛盾。因此纯简单类型系统不能给一般 $Y$ 定型；带一般递归的语言必须加入固定点原语、递归类型或其他足以打破该终止结论的机制。

推论与应用 ​

不动点组合子说明“递归”不是无类型函数计算必须额外假设的语法能力：只靠抽象、应用和自应用就能编码递归。它也让传名调用公理库传名调用Call by name · CBN把尚未求值的实参表达式直接替入函数体且只在需要时展开的策略。与传值调用的差别变得可观察——二者共享 β-规则，却对先展开函数体还是先求实参作出不同选择。

在编程语言中，具名 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。