因?yàn)榘l(fā)現(xiàn)簡書支持Markdown所以決定把我的新浪博客搬到簡書。
說明
lambda calculus是圖靈完備的語言，可以定義自然數(shù)，布爾值等等，這種方法稱之為Church encoding
例如對自然數(shù)的定義如下：
\f.\x. x =>0
\f.\x. f x =>1
\f.\x. f f x =>2
這里的返回值是右結(jié)合的，即
\f.\x. f f f f x =>\f.\x.(f(f(f(f x))))
以此類推，這個(gè)定義可以這么解釋，我們輸入兩個(gè)參數(shù)f和x，返回將f作用在x上n次的結(jié)果。
接下來可以定義加減乘除運(yùn)算。
加法再簡單不過了，m+n就是將已經(jīng)作用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 個(gè)f）
乘法同樣簡單，把作用n次f當(dāng)作一個(gè)過程，這個(gè)過程再進(jìn)行m次，就得到了m*n。
multi: \m.\n.\f.\x. m (n f)
再往下，乘法帶入乘法就得到了乘方。
exp: \m.\n. n m
關(guān)于減法
一步得到似乎有難度，所以可以先得到一個(gè)減1函數(shù)pred，即前驅(qū)，將pred作用輸入的次數(shù)即得到減法。
所以我們要找到f和x的具體形式，使得
f f...f x => g ...g y（n個(gè)f和n-1個(gè)g）
一個(gè)很自然的想法
f x => y
f exp => g exp ;;(exp !=x)
看起來很簡單，不過這里有個(gè)像if語句一樣的條件跳轉(zhuǎn)。
之前說過lambda calculus可以定義bool值。
true ： \x.\y x
false : \x.\y y
true可以理解為兩個(gè)輸入?yún)?shù)中選擇第一個(gè)，false則是選擇第二個(gè)。
這樣if的定義如下
\f.\x.\y. f x y
if b x y 的語句得到如下結(jié)果。
b=true => x
b=false => y
即true跳轉(zhuǎn)到第一條語句，false跳轉(zhuǎn)到第二條。
其他操作也可以定義：
and 函數(shù)，形如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
從上可以發(fā)現(xiàn)，如果需要對x的值進(jìn)行判斷，則讓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
現(xiàn)在我們得到了n-1個(gè)exp，接下來想辦法把上面的式子翻轉(zhuǎn)過來。
下求解exp
可以得到
(y exp)=(g z)
((g z) exp)=(g(g z))
顯然上面的等式是有問題的，每次計(jì)算都應(yīng)該應(yīng)返回一個(gè)函數(shù)調(diào)用下一個(gè)exp，所以相應(yīng)的做些修改。
即
(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
所以*式應(yīng)為
(...((yexp)exp)...exp)=\f.f g...g g z
多出來的\f.f的部分再簡單不過，令f=\x.x即可。
大功告成！整理一下上面得到的結(jié)果。
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函數(shù)
\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)
最后
解法并不唯一，可以參考維基百科。
