在漫长的编程学习过程中，
你可能会不经意间的，
知道了Y组合子。
它的内部结构极其诡异，
但是它又如此的让你魂牵梦萦，
让你茶饭不思，
为伊消得人憔悴。
这时候，数学基础是很重要的，
概念的差距，产生了无法逾越的鸿沟。
我们还是认真的从头开始吧。
lambda calculus
lambda calculus简称LC，
它是一个形式系统，
用来研究函数的组合和应用。
LC的研究对象称为λ项，
它是这样定义的，
λ项 = 变量
λ项 = λ项 λ项
λ项 = λ变量.λ项
例如：
((λy.y)(λx.(xy)))
(x(λx.(λx.x)))
都是合法的λ项。
我们用小写字母x，y，z表示变量，
大写字母M，N，P，Q表示λ项。
λ项是左结合的，
MNPQ ≡ (((MN)P)Q)，
λx.PQ ≡ (λx.(PQ))
λx尽可能多的向右结合。
其中，“≡”表示语法上相等。
替换规则
[N/x]M
表示把M中所有的x替换成N。
α转换
α转换说的是，
可以将λx.PQ中的x改为其他变量y，
只需要同时将PQ中的自由变量x改为y即可。
α转换定义了一个等价关系，
称为α等价。
注：
这里y不能和PQ中的同名变量y冲突。
α转换相当于变量更名。
β归约
β归约相当于函数调用。
(λx.M)N -> [N/x]M
即，对(λx.M)N进行β归约，
相当于把M中的变量x替换成N。
一个β范式（weak normal form），
是不能再进行β归约的λ项。
Church–Rosser定理
如果λ项P能β归约为M，即P->M，
也能β归约为N，P->N，
则存在λ项T，满足，
M->T且N->T。
它表示了λ项β归约的汇聚性。
而且，λ项在α等价的条件下，至多存在一个β范式。
Combinator logic
Combinator logic简称为CL，
它是一个形式系统，
与lambda calculus具有同样的计算能力。
CL研究了CL项的演算规则，
一个合法的CL项，由以下条件递归定义，
CL项 = 变量 | 基本组合子
CL项 = CL项 CL项
例如：
((S(KS))K)
((S(Kx))((SY)K))
都是合法的CL项。
我们用小写字母x，y，z表示变量，
大写字母X，Y，Z表示CL项。
CL项是左结合的，
UVWX ≡ (((UV)W)X)，
其中，“≡”表示语法上相等。
替换规则
[U/x]Y
表示把Y中所有的x替换成U。
例如：
[(SK)/x](yxx) ≡ y(SK)(SK)
弱归约（Weak reduction）
以下形式的CL项可以进行弱归约，
IX -> X
KXY -> X
SXYZ -> XZ(YZ)
如果进行这些变换可以使U变成U'，
就称CL项U可以弱归约为U'。
一个弱范式（weak normal form），
是不能再进行弱归约的CL项。
Church–Rosser定理
与lambda calculus一样，
对于CL，也有类似的定理，
如果CL项U可以弱归约为X，即U->X，
也可以弱归约为Y，即U->Y，
则存在CL项T，满足，
X->T且Y->T。
这表示了CL项弱归约的汇聚性。
而且，CL项至多存在一个弱范式。
CL项的抽象
为了和lambda演算进行对比，
我们定义CL项的抽象，
[x].M ≡ KM，如果x不是M中的自由变量
[x].x ≡ I
[x].Ux ≡ U，如果x不是U中的自由变量
[x].UV ≡ S([x].U)([x].V)，如果不满足(a)或(c)
可以证明，
([x].M)N可以弱归约为[N/x]M。
这里，我们只是用原始的CL项来定义了CL项的抽象，
[x]并不是CL语法的一部分，
而对于lambda calculus中的λ项λx.xy，
λx是λ项的一部分。
LC和CL的相似性
经过以上学习，
我们发现，
LC中的α等价，对应着CL中的语法等价，
LC中的β归约，对应着CL中的弱归约，
LC中的λx，对应着CL中的[x]。
我们就可以统一的，
用LC中的符号来说明问题了。
组合子
LC中的组合子，
表示一个闭项（closed pure term），
它不是一个原子，也不包含自由变量。
例如：
λxyz.x(yz)
λxy.x
CL中的组合子，
只有3个，I，K，S。
在LC中，可以这样表示，
I ≡ λx.x
K ≡ λxy.x
S ≡ λxyz.xz(yz)
不动点定理
在LC和CL中，
对于任意x，存在它的不动点Yx，满足，
Yx -> x(Yx)
其中，
“->”表示LC中的β归约，
或CL中的弱归约。
证明：
取Y ≡ UU
U ≡ λux.x(uux)
Yx ->
UUx ->
(λux.x(uux))Ux ->
(λx.x(UUx))x ->
x(UUx) ->
x(Yx)
不动点组合子
不动点组合子并不是唯一的，
存在不止一个Y，
使得对于任意x，Yx -> x(Yx)。
例如：
Turing组合子
Y ≡ UU，U ≡ λux.x(uux)
Curry-Ros组合子
Y ≡ λx.VV，V ≡ λy.x(yy)
不动点定理的用法
根据不动点定理，
我们能得到任意LC项或CL项的不动点，
所以，不动点方程总是有解的。
例如：
给定方程，x = M，M中可能包含x，
我们可以将它转换成不动点方程，
x = (λx.M)x，
解为：x = Y(λx.M) = Y(λt.[t/x]M)
它消除了M中的x。
例如：M ≡ yxz
x = Y(λx.M) = Y(λx.yxz) = Y(λt.ytz)，
等式右边就不包含自由变量x了。
所以，形如x = M的方程，
我们可以使用Y来消除M中的x。
这也表明可以不依赖于副作用，
用Y来定义匿名递归函数。
用Y组合子解递归方程
Haskell中的Turing Y组合子定义如下：
import Unsafe.Coerce
u = -> x $ u (unsafeCoerce u) x
y = u u
斐波那契函数fib的递归定义，
fib = -> if n<2 then 1 else (n*) $ fib $ n-1
为了消除等式右边fib，
我们把它转换成不动点方程，
fib = (> -> if n<2 then 1 else (n*) $ f $ n-1) fib
用Y组合子求解，得到了一个匿名的递归函数，
fib = y $ > -> if n<2 then 1 else (n*) $ f $ n-1
验证一下运行结果，
fib 5
=> 120
不动点存在性的疑问
方程解的性质是由方程决定的，
解法无法改变解的性质。
例如：
a = undefined = (-> undefined) a
解为：a = y $ -> undefined = undefined
add = -> add n+1
这个一个无限递归函数。
转换为不动点方程的形式，
add = (> -> f n+1) add
解为：add = y $ (> -> f n+1)
这个add仍然是一个无限递归函数。
初等函数的不动点
另外，对于初等函数的不动点方程，
x = f(x)
程序中直接写成x = f(x)会导致无限递归，
因为初等函数方程给出来的是约束，
而不是计算过程。
例如：
求解f(x) = 2x的不动点，
**直接写x = 2*x是一个无限的递归**，并不能解出x = 0来，
因此，x = 2*x实际表示的是一个无限递归的计算过程。
然而，仍然会存在满足这个方程的解。
不动点方程形式如下，
x = (-> 2*x) x
解为：x = y $ -> 2*x
确实可以使等式成立，
但它同样表示的是一个无限递归的计算过程。
f(x) = 2x的不动点方程，对应的“计算过程”应该是，
x = 0
不动点方程的形式如下，
x = (-> 0) x
解为：x = y $ -> 0 = 0
因此，
初等函数的不动点，
与LC或CL的不动点是两个不同的场景，
初等函数方程是一种约束规则，
LC或CL的等式是一种推导规则。
结语
不动点问题，
一直是我的心结。
只可惜功力不够，总是想不明白。
本文只是对最近学习的总结，
肯定有不严谨的地方，
只当做以后继续学习的起点吧。
参考：《Lambda-Calculus and Combinators》