因为发现简书支持Markdown所以决定把我的新浪博客搬到简书。
说明
lambda calculus是图灵完备的语言，可以定义自然数，布尔值等等，这种方法称之为Church encoding
例如对自然数的定义如下：
\f.\x. x =>0
\f.\x. f x =>1
\f.\x. f f x =>2
这里的返回值是右结合的，即
\f.\x. f f f f x =>\f.\x.(f(f(f(f x))))
以此类推，这个定义可以这么解释，我们输入两个参数f和x，返回将f作用在x上n次的结果。
接下来可以定义加减乘除运算。
加法再简单不过了，m+n就是将已经作用n次f的x再作用m次f即可。
plus: \m.\n.\f.\x. m f (n f x)
(plus m n)=> \f.\x. f f f...f x （一共 m+n 个f）
乘法同样简单，把作用n次f当作一个过程，这个过程再进行m次，就得到了m*n。
multi: \m.\n.\f.\x. m (n f)
再往下，乘法带入乘法就得到了乘方。
exp: \m.\n. n m
关于减法
一步得到似乎有难度，所以可以先得到一个减1函数pred，即前驱，将pred作用输入的次数即得到减法。
所以我们要找到f和x的具体形式，使得
f f...f x => g ...g y（n个f和n-1个g）
一个很自然的想法
f x => y
f exp => g exp ;;(exp !=x)
看起来很简单，不过这里有个像if语句一样的条件跳转。
之前说过lambda calculus可以定义bool值。
true ： \x.\y x
false : \x.\y y
true可以理解为两个输入参数中选择第一个，false则是选择第二个。
这样if的定义如下
\f.\x.\y. f x y
if b x y 的语句得到如下结果。
b=true => x
b=false => y
即true跳转到第一条语句，false跳转到第二条。
其他操作也可以定义：
and 函数，形如and b1 b2，若b1=true => b2， b1=false => false。
所以有
and : \x.\y. x y false
同理
or : \x.\y. x true y
not : \x. x false true
从上可以发现，如果需要对x的值进行判断，则让x作用在返回值上。
可以想到
(f x) = (x exp) = y
(f y)=(y exp)
f...f fy=(...((y exp)exp)...exp)=g...g g z ;;（不妨记为*式）
简单起见，令
x=\x.y f=\x.x exp
现在我们得到了n-1个exp，接下来想办法把上面的式子翻转过来。
下求解exp
可以得到
(y exp)=(g z)
((g z) exp)=(g(g z))
显然上面的等式是有问题的，每次计算都应该应返回一个函数调用下一个exp，所以相应的做些修改。
即
(y exp)=\f. f (g z)
((y exp) exp)=exp (g z)=\f. f (g(g z))
得到
exp=\x.\f.f (g x), y=\x. x z
所以*式应为
(...((yexp)exp)...exp)=\f.f g...g g z
多出来的\f.f的部分再简单不过，令f=\x.x即可。
大功告成！整理一下上面得到的结果。
x=\x. y
f=\x. x exp
exp=\x.\f.f (g x)
y=\x. x z
最后再化简一下。
x=\x.\y. y z
f=\x.x (\a.\f. f (g a))
有
(n (\x.\y. y z) (\x.x (\a.\f.f (g a))))=\f. f (g...g z)
所以得到pred函数
\n.\g.\z. (n (\x.x (\a.\f.f (g a))) (\x.\y. y z)) (\x.x)
重新命名一下各变量得到
pred: \n.\f.\x. (n (\x.x (\y.\f.f (g y))) (\x.\y. y z)) (\x. x)
最后
解法并不唯一，可以参考维基百科。
