简介

不动点组合子 (Fixed-Point Combinator) 是一种计算其他函数 不动点 (Fixed-Point) 的高阶函数. 有函数 \(f\) 其输入值 \(x\) 若与返回值相同 (同样是返回 \(x\), 即 \(f(x) = x\)), 则称之为函数 \(f\) 上的不动点为 \(x\). 例如现在有 \(f(x) = x ^ 2\), 则其不动点是 \(f(0) = 0 ^ 2 \equiv 0\) 以及 \(f(1) = 1 ^ 2 \equiv 1\). 而对于高阶函数 \(f\), 其拥有 \(g\) 作为不动点使得 \(f(g) = g\).

递归于 \(\lambda\)-演算 上的矛盾

现在假设我们有一阶乘函数 \(fact\):

\[ \begin{aligned} if\_then\_else & := \lambda p. \lambda a. \lambda b. p a b \\ fact & := \lambda x. if\ (x > 0)\ then\ (x * (fact\ (x - 1)))\ else\ 1 \end{aligned} \]

而我们从定义中得知 \(fact\) 于递归时将调用自身, 例如:

\[ \begin{aligned} fact\ 5 & = (\lambda x. if\ (x > 0)\ then\ (x * (fact\ (x - 1)))\ else\ 1)\ 5 \\ & \to_{\beta} 5 * (fact\ 4) \\ & \to_{\beta} 5 * (4 * (fact\ 3)) \\ & \to_{\beta} 5 * (4 * (3 * (fact\ 2))) \\ & \to_{\beta} 5 * (4 * (3 * (2 * (fact\ 1)))) \\ & \to_{\beta} 5 * (4 * (3 * (2 * 1))) \\ & \twoheadrightarrow_{\beta} 120 \end{aligned} \]

但实际在 \(\lambda\)-演算 中, 所有 \(\lambda\)-表达式 本质上是都应该是闭合的, 即无 自由变量 (Free Variable, FV) 的介入, 因此又称 匿名函数 (Anonymous function). 但上述例子中 \(fact \in FV\), 此处便会引发一个问题: 若果参数并非被绑定的 (即 \(M[\alpha := fact]\), M 为具体的 \(\lambda\)-表达式), 即我们无法直接透过 \(fact\ x\) 调用自身, 即无法达到递归的效果.

解决方案

但我们对此真的一点办法都没有了吗? 仔细琢磨其实并不, 我们可以在该函数本身多增加一个参数 \(\lambda f\), 并将自身作为值被传入至 \(\lambda f\) 上, 例如:

\[ \lambda f. (\lambda x. if\ (x > 0)\ then\ (x * (f (x - 1)))\ else\ 1) \]

并给该函数起个别名 \(fact'\)

\[ fact' := \lambda f. (\lambda x. if\ (x > 0)\ then\ (x * (f (x - 1)))\ else\ 1) \]

然后调用:

\[ \begin{aligned} fact'\ fact'\ 5 & = (\lambda f. (\lambda x. if\ (x > 0)\ then\ (x * (f\ (x - 1)))\ else\ 1))\ fact'\ 5 \\ & \to_{\beta} (\lambda x. if\ (x > 0)\ then\ (x * (fact'\ (x - 1)))\ else\ 1)\ 5 \end{aligned} \]

此时意外发生了! 仔细观察 \(fact'\ (x - 1)\) 的位置, 实际上 \(fact'\) 接受的是两个参数, 分别是 \(\lambda f\) 以及 \(\lambda x\), 但于函数内部的这个 \(fact'\) 却只传入了一个 \((x - 1)\) 的值而导致出错. 因此我们把 \(fact'\) 的定义修改为:

\[ fact' := \lambda f. (\lambda x. if\ (x > 0)\ then\ (x * (f\ f\ (x - 1)))\ else\ 1) \]

然后再次调用:

\[ \begin{aligned} fact'\ fact'\ 5 & = (\lambda f. (\lambda x. if\ (x > 0)\ then\ (x * (f\ f\ (x - 1)))\ else\ 1))\ fact'\ 5 \\ & \to_{\beta} (\lambda x. if\ (x > 0)\ then\ (x * (fact'\ fact'\ (x - 1)))\ else\ 1)\ 5 \\ & \to_{\beta} 5 * (fact'\ fact'\ 4) \\ & \to_{\beta} 5 * (4 * (fact'\ fact'\ 3)) \\ & \to_{\beta} 5 * (4 * (3 * (fact'\ fact'\ 2))) \\ & \to_{\beta} 5 * (4 * (3 * (2 * (fact'\ fact'\ 1)))) \\ & \to_{\beta} 5 * (4 * (3 * (2 * 1))) \\ & \twoheadrightarrow_{\beta} 120 \end{aligned} \]

由此可见, 该方法的语义与递归是完全一致的, \(\lambda\)-演算 的计算能力并没有因此而被削弱, 反而见到其强大的一面!

引出不动点

虽然我们已经成功地写出一个替代递归的解决方案, 但该方案并不太完美, 于 \(fact' fact' (x - 1)\) 的部分, 这里会多传一个值 \(fact'\) 作为 \(fact'\) 的参数, 就好像重复了两次一样, 那有没有什么办法让这个 \(fact'\) 函数只接受一个整数参数 \(x\) 且达到类似的效果? 现在当我们回想一下递归函数的定义 \(fact := \lambda x. if\ (x > 0)\ then\ (x * (fact\ (x - 1)))\ else\ 1\), 这不正正就是接受一个参数的函数嘛, 于是乎我们可以试图将其定义改回去再寻找新办法:

\[ fact' = \lambda f. (\lambda x. if\ (x > 0)\ then\ (x * (f\ (x - 1)))\ else\ 1) \]

然后再传入参数:

\[ \begin{aligned} fact'\ fact\ 5 & = (\lambda f. (\lambda x. if\ (x > 0)\ then\ (x * (f\ (x - 1)))\ else\ 1))\ fact\ 5 \\ & \to_{\beta} (\lambda x. if\ (x > 0)\ then\ (x * (fact\ (x - 1)))\ else\ 1)\ 5 \end{aligned} \]

\(\beta-reduction\) 之后的这一步, 我们会惊奇的发现 当中的 \((\lambda x. if\ (x > 0)\ then\ (x * (fact\ (x - 1)))\ else\ 1)\) 其定义与 \(fact\) 完全一致, 而当尝试只传入一个参数 \(fact\) 进行 部分求值 (Partial evaluation) 时, 即:

\[ \begin{aligned} fact'\ fact\ & = (\lambda f. (\lambda x. if\ (x > 0)\ then\ (x * (f\ (x - 1)))\ else\ 1))\ fact\ \\ & \to_{\beta} (\lambda x. if\ (x > 0)\ then\ (x * (fact\ (x - 1)))\ else\ 1) \\ & = fact \end{aligned} \]

这里我们会发现 \(fact'\) 于传入 \(fact\) 时, 则会返回 \(fact\), 即 \(fact\)\(fact'\) 的不动点!

构造 Y-组合子

最终于知道不动点的性质之后, 我们尝试去构造出一个真正能使用的 \(Y\)-组合子 吧! 首先设有一递归函数 \(r\) :

\[ r = r\ r\ r...\ r \]

然后由于 \(\lambda\)-演算 中递归引发出自由变量的问题, 现在把递归函数作为参数传入, 因此将定义改为:

\[ \begin{aligned} Y & = \underbrace{(\lambda r. r\ r\ r\ ...\ r)}_{f}\ f \\ & = \underbrace{(\lambda r. r\ r\ r\ ...\ r)}_{f} \underbrace{(\lambda r. r\ r\ r\ ...\ r)}_{f} \end{aligned} \]

但此处的 \(r\) 的第一个参数应为自身, 正如上面 \(fact'\) 的例子一样, 修正为:

\[ Y = \underbrace{(\lambda r. (rr)\ (rr)\ (rr)\ ...\ (rr))}_{f'} \underbrace{(\lambda r. (rr)\ (rr)\ (rr)\ ...\ (rr))}_{f'} \]

虽然到此步时, 该定义已经能用了, 但始终每一个 \(rr\) 都将重复传入而不够完美 (具体参照 \(fact'\) 的例子), 我们可再将其化简为:

\[ Y = (\underbrace{(\lambda r. r\ r\ r\ ...\ r)}_{f} (xx)) (\underbrace{(\lambda r. r\ r\ r\ ...\ r)}_{f} (xx)) \]

最后我们把递归函数的部分改成 \(f\) 并作为参数传入, 则其定义最终为:

\[ Y := \lambda f. (\lambda x. f (xx)) (\lambda x. f (xx)) \]

定义

常规的形式化定义

\[ \forall F \exists X. F X = X \]
对于所有的 \(F \in \Lambda\), 存在 \(X \in \Lambda\) 使得 \(F X = X\).
\[ fix\ f = f\ (fix\ f) \]
展开则为 \(fix\ f = f\ (f\ (...\ f\ (fix\ f)\ ...))\).

\(Y\)-组合子的定义

\[ Y \equiv \lambda f. (\lambda x. f(xx)) (\lambda x. f(xx)) \]
这里的 \(f\) 为任意需要被找出一个或多个不动点的函数, 而其中 \(x\) 必定为一高阶函数.


不动点定理 (Fixed Point Theorem) 的证明

首先应用实际函数 \(F\)\(Y\)-组合子 上:

\[ Y F \equiv (\lambda f. (\lambda x. f(xx)) (\lambda x. f(xx)))\ F = (\lambda x. F(xx)) (\lambda x. F(xx)) \]

现在假设 \(W\)\(X\) 组合子以辅助证明, 例如:

\[ W \equiv \lambda x. F(xx) \\ X \equiv WW \]

开始证明:

\[ X \equiv WW \equiv (\lambda x. F(xx))\ W = F(WW) \equiv F X \]

然后可得 \(X \equiv F X\), 而因为:

\[Y F = (\lambda x. F(xx)) (\lambda x. F(xx)) \equiv WW \equiv X\]

因此 \(X \equiv Y F\), 所以可以把 \(X\) 替换成 \(Y F\), 最终得到:

\[ Y F \equiv F (Y F) \]

从证明的结论中得知 $ Y F = F (Y F) $, \(F\) 这个函数将会不断地自我递归:

\[ Y F \equiv F (Y F) \equiv F (F (Y F)) \equiv (F (F ... F (Y F) ...)) \]

应用

实际例子

阶乘函数

\[ \begin{aligned} fact & := \lambda f\ x. if\ (x > 0)\ then\ (x * (f\ (x - 1)))\ else\ 1 \\ Y\ fact\ 5 & = (\lambda f. (\lambda x. f\ (xx)) (\lambda x. f\ (xx)))\ fact\ 5 \\ & \to_{\beta} ((\lambda x. fact\ (xx)) (\lambda x. fact\ (xx)))\ 5 \\ & \to_{\beta} (fact\ ((\lambda x. fact\ (xx)) (\lambda x. fact\ (xx))))\ 5 \\ & \to_{\beta} ((\lambda f\ x. if\ (x > 0)\ then\ (x * (f\ (x - 1)))\ else\ 1)\ ((\lambda x. fact\ (xx)) (\lambda x. fact\ (xx))))\ 5 \\ & \to_{\beta} (\lambda x. if\ (x > 0)\ then\ (x * (((\lambda x. fact\ (xx)) (\lambda x. fact\ (xx)))\ (x - 1)))\ else\ 1)\ 5 \\ & \to_{\beta} 5 * (((\lambda x. fact\ (xx)) (\lambda x. fact\ (xx)))\ 4) \\ & \twoheadrightarrow_{\beta} 5 * (4 * (((\lambda x. fact\ (xx)) (\lambda x. fact\ (xx)))\ 3)) \\ & \twoheadrightarrow_{\beta} 5 * (4 * (3 * (((\lambda x. fact\ (xx)) (\lambda x. fact\ (xx)))\ 2))) \\ & \twoheadrightarrow_{\beta} 5 * (4 * (3 * (2 * (((\lambda x. fact\ (xx)) (\lambda x. fact\ (xx)))\ 1)))) \\ & \twoheadrightarrow_{\beta} 5 * (4 * (3 * (2 * 1))) \\ & \twoheadrightarrow_{\beta} 120 \end{aligned} \]

编程上的应用

不动点函数

由于在实际编程中, 绝大多数带静态类型的语言均不支持 递归类型 (Recursive Type), 就如 Haskell 等, 因此就无法避免于函数应用于自身时所带来的函数类型无限递归引致停机问题, 因此于实现 \(Y\)-组合子 (不动点组合子) 时我们多采用了编程语言本身的特性, 例如 Haskell 的 \(fix\) 函数定义如下:

1
2
fix :: (a -> a) -> a
fix f = let x = f x in x

Recursive Scheme

透过不动点的概念定义出 Recursive Scheme, 我们不仅仅能够于项上定义出不动点, 同样地亦可于类型上定义出来, 例如透过 Free monad, Catamorphism, Anamorphism 等等的抽象结构, 可以站在高处以俯视的角度宏观地看待某些问题, 例如在处理抽象语法树时, 可利用该种方式消除 模板代码 (boilerplate) 等等.

外部链接

本文部分内容参考或引用至下列网页,也可供作为额外的延伸资源帮助阅读: