不动点组合子Y-Combinator

Python中的lambda用起来还是很爽的,不过坑也有很多,比如说这个early binding和late binding的问题,或者lambda中只能有一个语句(实际上是表达式)。
不管怎样,可以把lambda当做一个匿名函数来看待,那么这个匿名函数如何在递归调用的时候引用自己呢?Haskell B. Curry给出了Y不动点组合子(Y Combinator, 当然不是那个著名的公司啦)可以解决这个问题。

定义问题

考虑计算阶乘函数,Python可以很容易写出下面的代码:

1
fac = lambda x: 1 if x <= 1 else x * fac(x - 1)

我们注意到在lambda中存在对自己的引用fac。不过对于某些其他的语言,例如C#,就没那么轻松了,于是我们希望有一个类似this指针的东西,能够在lambda函数体中用来表示自己。

函数的不动点

不动点的数学定义

如果f(x) = x那么xf的不动点,因此不动点指的是那些被函数仍然映射到自身的点。当然并不是所有函数都有不动点,因为上面给出的方程不一定有解。
容易发现不动点和我们的问题之间有明显的关联性,因为我们实际上是要在函数fac递归地调用fac,因此我们函数调用的形式是fac(fac(...))这样的。如果我们能把这个递归

构造函数F

下面我们考虑下面的函数F,我们看到F的功能是和fac相同的。F对原版的fac进行了一番封装,将原版的fac作为了自己的第一个参数,将原版fac的参数x作为自己的第二个参数,在函数体中,我们简单地复制了之前的定义。

1
2
3
#define B 1 if x <= 1 else x * fac(x - 1)
fac = lambda x: B
F = lambda fac, x: B

审查这个函数,我们发现非常奇怪的一点是我们找不到fac的定义了。如果我们把Ffac视为未知数,那么就定义了Ffac之间的一个方程。下面我们将F柯里化成下面的等价形式,也就是说F接受了一个函数作为参数,并且返回了这个作为参数的函数的定义

1
F = lambda fac: lambda x: B

因此我们可以得到下面的等式

1
F(fac) = fac

因此我们将如何在lambda内部引用fac的问题转化为求函数F的不动点的问题。而这个就借助于Y不动点组合子,它满足下面的特性,对于任意的函数F,存在不动点Y F

1
(Y F) = F (Y F)

定义lambda演算

为了能够将上面的数学思路推广到lambda中,首先需要简单了解lambda演算(Lambda Calculus)。lambda演算是图灵完备的,邱奇利用lambda演算证伪了可判定性问题。

形式化定义

lambda演算文法非常简单,只由下面三个lambda term组成

  1. 引用标识符(Variable)
    $a$

  2. 定义函数(Abstraction)
    $(\lambda x. M)$,括号可省略。
    此时变量$x$被绑定到了这个lambda表达式,而这个绑定的作用域便以括号为界。

  3. 应用函数(Application)
    $(M \, N)$
    在lambda演算中函数作用是左结合的,即$s\,t\,x$实际上是$(s\,t)x$。
    例如$\omega$组合子$\lambda x.x\,x$,它可以被看做$(\lambda x.x) (x)$,而不是$\lambda x.(x\,x)$

括号

lambda演算中的括号在无歧义的情况下是可以省略的。因此式子$(\lambda x.x \, x)(\lambda y.y)$可以写成$\lambda(x.x\,x) \lambda y.\,y$。
式子$\lambda x.((\lambda x.x)x)$和式子$(\lambda x.(\lambda x.x))x$并不能作为同一个lambda term。其中第一个式子中外面的lambda是返回的一个值,而第二个式子中外面的lambda是返回的一个lambda。

绑定

一个合法的lambda函数不应当出现自由变量。如$\lambda x.(x\,y)$中,$x$是被绑定的,但是$y$没有被绑定到在表达式中的任何一个$\lambda$上。

lambda演算规则

首先定义$E[V:=W]$,这表示一个表达式$E$,这个表达式中的所有$V$的自由出现都替换成$W$。

α-转换(Alpha equivalence)

这个变换的意义是被绑定变量的名称是不重要的,所以我们可以用任何的其他名字来替换,其定义为$\lambda V.E = \lambda W.E[V:=W]$。
当然,前提是首先要是被绑定的,我们看前面的一个例子$\lambda x.x\,x$,它相当于$(\lambda x.x) (x)$。这里面有两个$x$,但这两个变量却不是一个变量,因为只有前一个变量被绑定到了$\lambda$上,而后一个是自由变量

β-归约(Beta reduction)

这个类似于C等语言中的传参,或者数学里面的代入。其定义是$\lambda x.t$能够归约成$t[x:=s]$,这个beta reduce过程表示为$(\lambda x.t)s \rightarrow t[x:=s]$。在这时,相当于我们将$x$的值赋为了$s$。这个过程必须要确保$E’$再替换后仍然是自由的。

绑定与自由

例如$\lambda z.(\lambda x . x + z)(x + 2)$,和我们在α-转换中看到的例子一样,$(\lambda x . x + z)$中出现的$x$是绑定的,但是$x + 2$中的却是自由的,因此我们不能直接把这个自由的$x$代入到绑定的$x$里面去。
如对于任意的“自变量”$s$,有$(\lambda x.x)s \rightarrow x[x:=s] = s$,因此该函数是个恒等函数。又如$(\lambda x.y)s \rightarrow y[x:=s] = y$,这说明$\lambda x.y$是个常量函数。

通常形式

beta可归约式(redex)具有以下的形式$((\lambda x.A(x))t)$。例如$(\lambda x.x\,x)(\lambda y.z) \leftarrow (\lambda y.z)(\lambda y.z)$
对于无类型的lambda演算来说,这个规约过程还可能是无法终止的。考虑下面的$\Omega$算子$\Omega = (\lambda x.x\,x)(\lambda x.x\,x)$

$$
\begin{equation}\begin{split}
& (\lambda x.x\,x)(\lambda x.x\,x) \\
\rightarrow & (x\,x)[x:=\lambda x.x\,x] \\
= & (x[x:=\lambda x.x\,x])(x[x:=\lambda x.x\,x]) \\
= & (\lambda x.x\,x)(\lambda x.x\,x)
\end{split}\end{equation}
$$

η-变换(Eta conversion)

η-变换体现了外延性(extensionality)的思想,即两个数学对象是相等的,如果没有区分它们的检验。对于lambda中的函数来说,如果两个函数对于任意的输入都能产生相同的行为(即返回相同的结果),那么可以认为这两个函数是相等的。
η-变换的一个用途是$\lambda x.f\,x$和$f$是等价的(注意它们不一定性能相同,详见Haskel里有关where的一个例子),只要$x$不是$f$中的自由出现。

Y Combinator的实现

我们定义Y组合子为
$$
Y = \lambda f . (\lambda x. f(x \, x)) (\lambda x. f(x \, x))
$$

证明

我们证明这样的$Y$满足
$$
(Y g) = g (Y g)
$$
首先我们根据beta归约,将函数$g$带入
$$
Y g = (\lambda x . g (x \, x)) (\lambda x . g (x \, x))
$$
下面我们使用alpha法则来修改一下绑定的变量名字,以便后面的带入,有
$$
Y g = (\lambda y . g (y \, y)) (\lambda x . g (x \, x))
$$
下面我们将所有的$y$替换成$(\lambda x . g (x x))$,同样是根据beta法则
$$
Y g = g ((\lambda x . g (x \, x)) (\lambda x . g (x \, x)))
$$
而后面的又是一个$Y g$,于是得证。

类型分析

下面我们进一步探究一下我们这样的构造为什么能得到一个递归。y接受一个函数,返回这个函数的不动点,因此类型应该是这样的。

1
y :: (a -> a) -> a

\x -> f (x x)作为一个整体g,那么y的工作就是将g作为唯一参数来调用自己,这有点像我们证明停机问题的时候的操作。

1
y = \f -> g g

现在我们查看这个g,它接受一个可调用的x作为参数,并且做f (x x)这样的调用。首先我们看x x这个调用,我们令

1
x x :: a

则有

1
x :: b -> a

其中ab为未知类型。在另一方面,我们还能推导出

1
b :: b -> a

这是因为我们作为函数来考虑x,它接受一个b类型的x作为参数,而根据前面的式子x又具有类型b -> a,所以我们可以得出b的类型是b -> a。因此这个类型是递归

备注

递归类型

List就可以看做一种递归类型

1
data List a = Nil | Cons a (List a)

在函数式语言例如Haskell/OCaml中,递归是不能以type synonyms的形式来实现的,例如下面这些使用type的语句是不合法的。我们可以简单地想象在C++里面的typedef关键字定义的“类型”,在实际上他们并不是正在的类型,而是alias构成的语法糖。如果我们使用这样的定义,那么在编译时就会因为简单的替换而导致死循环的发生

1
2
type Bad = (Int, Bad)
type Evil = Bool -> Evil

解决之道就是按照下面的方式去新建一个ADT(Algebraic data type)

1
2
data Good = Pair Int Good
data Fine = Fun (Bool->Fine)