不动点组合子
前言
相信接触过Lambda演算的朋友都或多或少听说过不动点组合子。不动点组合子的抽象性使它较为难以理解,因此本文旨在用较为朴素的语言解释不动点组合子的特点、应用以及推导过程。
不动点与不动点组合子
不动点,即某个函数的自变量,它让函数值等于它自身:
对于函数f,若存在a使得f(a) = a,则称a是f的不动点。
在Lambda演算体系内,可以这样定义:
对于函数f,若存在a使得f a = a,则称a是f的不动点。
不动点组合子则提供了一种求解不动点的通用方法:
若Y是不动点组合子,
对于函数g = λx.M,其中M是Lambda表达式,
有Y g = f,其中g f = f。
由此可见,不动点组合子实际上提供了一种方法,它能够解出目标函数g的不动点f。
一个有趣的结论
对于函数g = λx.M,其中M是Lambda表达式,
有Y g = f,其中g f = f。
上面的结论,有什么用呢?要探索不动点组合子的用途,不妨顺着结论继续推导:
对于函数g = λx.M,其中M是Lambda表达式,
有Y g = f,其中g f = f。
因此f = Y g = g f = M,其中M中的自由变量x = f = M。
(由于f = M,因此有x = f = M。)
(请读者耐心理解上面的推导过程。)
这是一个令人激动的结论:f = M,并且M中的自由变量x = f = M
。
这意味着Lambda表达式M引用了它自身!
整理上面得出的结论:
对于函数g = λx.M,其中M是Lambda表达式,
有f = Y g = M,其中M中的自由变量x = f = M。
或者进一步简化:
f = Y (λx.M) = M,其中M是Lambda表达式,M中的自由变量x = f = M。
匿名函数的递归
通过上面的推导,我们成功地让一个表达式通过引用更高阶函数的绑定变量的方式来引用其自身。
为了便于直观理解,我们将上面的结论中的f改名为F,x改名为f,即:
F = Y (λf.M) = M,其中M是Lambda表达式,M中的自由变量f = F = M。
(改名并不影响结论的正确性,这里仅仅希望能够和下面例子中的名字对应,从而更加容易理解。)
由此,我们可以尝试让一个没有名字的函数实现递归:
F = Y (λf.λx.(...f a...))
(备注:M = λx.(...f a...))
上面的表达式实际上相当于:
F = λx.(...F a...)
也许会有人说,第一个表达式不是依然有名字——大写F吗?其实这并没有什么影响,因为表达式Y (λf.λx.(...f a...))
内部并没有引用大写F。
推导不动点组合子
首先考虑一个一般意义上的递归函数:
F = λx.(...F a...)
如何将函数F改写为非递归形式?由上文的启发,我们可以想办法让函数体中对F的引用变为对更高阶函数的绑定变量的引用。
这里直接给出方法:
F' = λf.(λx.(...(f f) a...))
F = F' F'
验证如下:
F = F' F' = λx.(...(F' F') a...) = λx.(...F a...)
接下来考虑不动点组合子的特点:
Y g = f,其中g f = f,
于是有Y g = f = g f = g (Y g)。
由Y g = g (Y g)
可以看出,不动点组合子本身可以被描述为递归形式。
接着,通过Y g = g (Y g)
写出不动点组合子的定义:
Y = λg.g (Y g)
将上面的递归定义通过上文介绍的方法改写为非递归形式:
Y' = λy.(λg.g ((y y) g))
Y = Y' Y'
对上式进行简化:
Y
= Y' Y'
= (λy.(λg.g ((y y) g))) (λy.(λg.g ((y y) g)))
= (λyg.g (y y g)) (λyg.g (y y g))
= (λux.x (u u x)) (λux.x (u u x))
到这里,我们完成了不动点组合子的推导。
需要说明的是不动点组合子并不是指某一个函数,而是指一系列满足方程Y g = g (Y g)
的解Y
。不动点组合子的个数是无限的!上文仅仅推导出了其中一个不动点组合子,该不动点组合子由Alan Turing在1937年给出。
容易产生的误解
读者可能已经发现,本文首先介绍了不动点组合子的一个经典应用——实现匿名递归函数。接着,本文又说明了不动点组合子本身可以被描述为递归形式。这里似乎陷入了一个怪圈:我们用不动点组合子来实现递归函数,可是不动点组合子本身又可以被描述为递归函数!
陷入这种怪圈的原因是错误地认为是不动点组合子赋予Lambda演算递归的能力。
事实上Lambda演算的递归能力在于其本身的不一致性,不动点组合子仅仅给予我们一种通用的方法,这种方法能够更方便的实现匿名递归函数!
自我引用与不一致性
(未完待续)