不动点组合子 | Y Combinator

在现代编程语言中,函数都是具名的,而在传统的Lambda Calculus中,函数都是没有名字的。这样就出现了一个问题 —— 如何在Lambda Calculus中实现递归函数,即匿名递归函数。Haskell B. Curry发现了一种不动点组合子 —— Y Combinator,用于解决匿名递归函数实现的问题。

Fixed-point combinator

我们先来看看不动点组合子的定义。不动点组合子(fixed-point combinator)是一个满足以下等式的高阶函数$y$:

$$\forall f, \ y \ f = f \ (y \ f)$$

如果令 $x = f \ x$,那么这其实就是一个求解函数不动点的问题:

$$x = f \ x$$

Y Combinator

那么不动点组合子有什么用呢?假设我们想要求阶乘,我们通常会用递归来实现:

1
2
3
factorial :: Int -> Int
factorial 0 = 0
factorial n = n * factorial (n - 1)

在上面的例子中,factorial函数体里面引用了自身。用pseudo lambda calculus可以表示为:

$$f = \lambda n. \ if \ (n == 0) \ 0 \ else \ n * f(n - 1)$$

但是Lambda演算中函数是没有名字的,所以这个地方是没法在函数体内调用f的。那怎么处理呢?我们可以通过某种“黑魔法”实现间接递归 —— 把自己算出来。我们不妨假设一个函数self代表一个“Lambda Calculus中真正的”递归函数,则上式可以改写为:

$$f = \lambda n. \ if \ (n == 0) \ 0 \ else \ n * self(n - 1)$$

我们现在把self函数参数化,设此函数为G

$$G = \lambda n \ \lambda g. \ if \ (n == 0) \ 0 \ else \ n * g(n - 1)$$

应用 $\beta-reduction$,我们会发现:

$$G \ f = \lambda n. \ if \ (n == 0) \ 0 \ else \ n * f(n - 1)$$

即 $G \ f = f$。

然而这还不够,这里就需要引入不动点组合子了。假设不动点组合子 $Y = \lambda \ f. f (Y \ f)$,且 $f = Y \ G$,那么 $Y G = G (Y \ G) = G \ f = f$,这就表示出f来了!

所以我们需要找到一个与 $Y$ 等效的闭合Lambda表达式,其中最著名的就是Curry发现的 Y Combinator:

$$Y = \lambda f. (\lambda x . f \ (x \ x)) (\lambda x. f \ (x \ x))$$

通过 $\beta-reduction$ 验证:

$$Y \ g = \lambda f. (\lambda x . f \ (x \ x)) (\lambda x. f \ (x \ x)) \ g$$

$$= (\lambda x. g \ (x \ x)) (\lambda x. g \ (x \ x)$$

$$= g \ ((\lambda x. g \ (x \ x) \ (\lambda x. g \ (x \ x))$$

$$= g \ (Y \ g)$$

一颗赛艇!至于Y Combinator是如何推出来的,可以参考 康托尔、哥德尔、图灵——永恒的金色对角线 这篇文章,写的非常完美。

Haskell实现

我们先尝试直接用函数表示:

1
fix f = (\x -> f (x x)) (\x -> f (x x))

GHC会提示错误:

1
2
3
4
5
6
7
8
9
10
<interactive>:6:25:
Occurs check: cannot construct the infinite type: r0 ~ r0 -> t
Expected type: r0 -> t
Actual type: (r0 -> t) -> t
Relevant bindings include
x :: (r0 -> t) -> t (bound at <interactive>:6:15)
f :: t -> t (bound at <interactive>:6:9)
fix :: (t -> t) -> t (bound at <interactive>:6:5)
In the first argument of ‘x’, namely ‘x’
In the first argument of ‘f’, namely ‘(x x)’

这里的问题在于x的类型是infinite type,无法在Haskell表示出来(Hindley–Milner类型系统的限制)。参考Reddit上的解决方案,我们需要绕个弯,定义一个Mu算子来绕过类型检查:

1
2
3
newtype Mu a = Mu (Mu a -> a)
y f -> (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)

当然还有个更加贴近Y Combinator原本意思的实现:

1
2
3
4
5
6
7
8
9
10
newtype Mu f = Mu {unMu :: f (Mu f)}
unfold = unMu
fold = Mu
newtype X' b a = {unX :: a -> b}
type X a = Mu (X' a)
unfold' = unX . unfold
fold' = fold . X'
y f = (\x -> f (unfold' x x)) $ fold' (\x -> f (unfold' x x))

References

文章目录
  1. 1. Fixed-point combinator
  2. 2. Y Combinator
  3. 3. Haskell实现
  4. 4. References