在传统方法下,我们很难在无类型 $\lambda$ - 演算这样的匿名上下文中进行函数的递归。
为解决此问题,我们希望有一个函数用以“得到函数自身”,即为 Y - 组合子。
Y - 组合子使用 $\lambda$ - 演算定义为:
$$ Y=\lambda f.(\lambda x.f(x\space x))\space(\lambda x.f(x\space x)) $$
Y - 组合子应用于函数:
$$ \begin{align} Y\space f &=(\lambda x.f(x\space x))\space(\lambda x.f(x\space x))\newline &=f\space((\lambda x.f(x\space x)\space(\lambda x.f(x\space x)))\newline &=f(Y\space f) \end{align} $$
即进行两次 $\beta$ - 规约并将 (1) 代入 (3)。最终我们得到:
$$ Y\space f=f\space(Y\space f) $$
Y - 组合子或称不动点组合子,因其将函数映射到其不动点上。
若 $f\space x=x$ ,则称 $x$ 是 $f$ 的一个不动点。
推导
Y - 组合子的推导过程实质上就是解不动点方程 $Y\space f=f\space(Y\space f)$ 的过程。
考虑不断迭代该不动点方程:
$$ Y\space f=f\space(Y\space f)=f\space f\space(Y\space f)=f\space f\space f\space… $$
将这个无限长的序列称作 $g$ ,则有 $g = f\space g$.
由于序列无限长,不妨将其截半,设 $g=g’\space g’$. 这是因为我们希望可以得一个带有函数的参数的表达式在方程中,以便于解得函数。
则有
$$ g’\space g’=f(g’\space g’) $$
如此构成了一个合法的函数定义:
$$ g’=\lambda x.f(x\space x) $$
代入原方程即可得:
$$ Y\space f=g=g’\space g’=(\lambda x.f(x\space x))\space(\lambda x.f(x\space x))\ Y=\lambda f.(\lambda x.f(x\space x))\space(\lambda x.f(x\space x)) $$
这样就得到了 $Y$ 的定义。