不动点组合子Y-Combinator

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

Y Combinator当然不是那个著名的公司啦,事实上,如果f(x) = x那么xf的不动点
考虑计算阶乘,python可以很容易写出下面的代码:

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

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

lambda演算

首先需要简单了解lambda演算(Lambda Calculus)。lambda演算是图灵完备的,邱奇利用lambda演算证伪了可判定性问题。

形式化定义

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

引用标识符(Variable)

$a$

定义函数(Abstraction)

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

应用函数(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 -> t[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$中的自由出现。