标签：
lambda算子是一切函数式语言的基础，明白lambda算子对于掌握函数式语言有着许多好处。最近学习相关知识略有所得，故在此写出以备忘：
λ 算子是函数式编程的理论基础，是图灵机外的另一种计算模型。 它十分简洁，只有三条产生规则，却可以表达一切可计算的函数。
λ 算子的核心概念是表达式expression。λ 算子的产生规则如下：
<expression> ::= <name>|<function>|<application>
<function> ::= λ <name>.<expression>
<application> ::= <expression><expression>
需注意：
function表示函数的定义，采用
λ <name>.<expression>
的形式。 <name>代表函数的参数，expression则是该函数的返回值。
λ 中的function都是单参数函数，如下例：
λ a.a+1
本例中假设已定义+操作
那么如何定义多参数函数呢？可以使用嵌套结构：
λ a.λ b.a+b
这个例子也可以简写为
λ a b.a+b
application表示函数的应用。应用中，参数的使用采用替换的方式来完成， 因此函数中参数的名字实际是无关紧要的，所以
λ x.x ≡ λ y.y ≡ λ z.z
用以下符号来表示替换：
(λ x.x)y = [y/x]x = y
[y/x]表示把x替换成y， 一个简单的记法是把x想成分母，乘了后面的x以后就只剩下y了，这样就完成了替换
λ 算子中，我们把出现在λ 后参数中的变量称为约束变量， 把不出现的λ 后的变量称为自由变量，比如：
λ x.xy
x为约束变量，y为自由变量。
自由变量的判断规则有下列三条：
约束变量的判断规则有下列两条
需要注意的是，一个变量在表达式中可能既自由又约束，考虑下面的这个例子：
(λ x.xy)(λ y.y)
在λ x.xy中，y是自由的，但在λ y.y中y却是约束的。
在λ 算子中，函数都是没名字的， 这样用起来是很麻烦的事情，每次用函数都需要把它的定义写一遍。 因此，为了简便，我们可以给函数定义起个别名：
f ≡ λ x.x
ff = (λ x.x)(λ z.z)
= [λ z.z/x]x
= λ x.x
= f
当函数中存在自由变量时需要小心变量名的冲突：
(λ x.(λ y.xy))y = λ y.[x/y]y = λ y.yy
注意，在表达式λ y.xy中x为自由变量，这一点很重要。 此时两个y发生了冲突。把函数中的约束变量y改名为t：
(λ x.(λ t.xt))y = λ t.[x/y]t = λ y.yt
最后，总结一下替换规则。 在函数λ x.<exp>应用到表达式E时，把exp中所有的自由的x替换成E。 如果替换会使得自由变量变为约束变量， 那么在替换前应该把冲突的约束变量重命名。
再看一个例子：
(λ x.(λ y.(x (λ x.xy))))y
在(λ y.(x (λ x.xy)))中只有第一个x是自由的，因此只需要替换第一个x即可。 可是替换x为y后x就会变成约束变量，因此需要对约束变量y进行重命名：
[y/x](λ t.(x (λ x.xt))) = (λ t.([y/x]x (λ x.xt))) = (λ t.(y (λ x.xt)))
需要注意，在对λ x.<exp>的替换中，替换的是<exp>中的自由变量x，而不是λ x.<exp>中的变量x， 在λ x.<exp>中不存在自由的x。
另外，在使用函数时，如果给出的参数不足函数定义的参数，那么会产生一个新的函数， 若参数数量足够，则消去对应的λ 部分
example ≡ λ xy.x(y)
example a ≡ (λ xy.x(y))a
≡ (lambda y.a(y))
example a b ≡ (λ xy.x(y))a b
≡ a(b)
有了λ 算子，就可以从全新的角度重新定义许多基础的概念了。
通过如下定义可以定义所有的自然数：
0 ≡ λ sz.z
1 ≡ λ sz.s(z)
2 ≡ λ sz.s(s(z))
这样定义的数被称为丘奇数。
有了丘奇数，还可以对其进行运算：
S ≡ λ wyx.y(wyx)
S0 ≡ (λ wyx.y(wyx))(λ sz.z)
≡ λ yx.y((λ sz.z)yx)
≡ λ yx.y(x)
≡ 1
S1 ≡ (λ wyx.y(wyx))(λ sz.s(z))
≡ λ yx.y((λ sz.s(z))yx)
≡ λ yx.y(y(x))
≡ 2
S可以对数进行加一操作。那么如何实现加法呢？
2S1 ≡ (λ sz.s(s(z)))(λ wyx.y(wyx))(λ uv.u(v))
≡ λ wyx.y(wyx)(λ wyx.y(wyx)(λ uv.u(v)))
≡ SS1
≡ λ wyx.y(wyx)(λ yx.y(y(x)))
≡ S2
≡ 3
在这个例子中，数2把加一操作嵌套了两次，依次作用在1上，得到了3； 同理，当计算m+n是，m会把加一操作嵌套m次并作用在n上，得到的结果就是m+n。
乘法的定义如下：
x ≡ (λ xyz.x(yz))
x 2 2 ≡ (λ xyz.x(yz))2 2
≡ λ z.2(2z)
≡ λ z.2((λ uv.u(u(v)))z)
≡ λ z.2(λ v.z(z(v)))
≡ λ z.((λ ab.a(a(b)))(λ v.z(z(v))))
≡ λ z.(λ b.(λ v.z(z(v))((λ v.z(z(v)))b)))
≡ λ zb.(λ v.z(z(v)) (z(z(b))))
≡ λ zb.z(z(z(z(b))))
≡ 4
用λ 算子还可以定义逻辑值true和false，并在其上进行操作：
T ≡ λ xy.x
F ≡ λ xy.y
正误的定义很简单，逻辑运算的定义也不复杂：
∧ ≡ λ xy.xyF
∨ ≡ λ xy.xTy
¬ ≡ λ x.xFT
有了逻辑值，就可以定义带条件分支的函数。 现在我们来定义一个函数，使得输入0返回T，输入正数返回F：
Z ≡ λ x.xF¬F
若作用在0上，那么会展开成如下：
Z0 ≡ 0F ¬ F ≡ (λ sz.z)(F ¬)F ≡ ¬ F ≡ T
若作用在正整数N上，则会展开成如下（以2为例子）：
Z2 ≡ 2F ¬ F ≡ (λ sz.s(s(z)))(F ¬)F
≡ F(F(¬))F ≡ FAF ≡ F
A ≡ F(¬)
如例子所示，无论内部嵌套多少F(F(F(¬)))，由于都是FAF的形式，返回结果都是F。
之后，就可以定义比较函数。 在此之前，需要先定义减一函数。
对于任意一个二元组(x, y)，可以用如下表达式定义：
λ zxy.xy
z为T时，可以得到该二元组的第一个数，为F时可得第二个数。
现在定义一个函数G，给出二元组(m, n)，返回(m+1, m)：
G ≡ λ pz.z(S(pT))(pT)
其中p为二元组
那么对数m的减1运算就是对z00二元组进行m次G操作，然后取其第二个元素， 因此减一定义为：
P ≡ λ n.nG(λ p.p00)F
注意，当输入为0时，返回的结果仍为0
此时，x ≥ y可以定义为对y进行x次减一操作得到的结果为0:
GT ≡ λ xy.Z(xPy)
这样，等取操作就是x ≥ y且y ≥ x：
EQ ≡ λ xy.∧ (GT xy)(GT yx)
由大等、等于以及逻辑操作，可以定义小于、小等、不等等一系列比较操作，在此就略过了。
待续
标签：
原文地址：http://www.cnblogs.com/w0mTea/p/4244875.html
