一個(gè)前人寫的有關(guān)Lambda演算的項(xiàng)目，里面包含了一個(gè)完整的關(guān)于Lambda演算的起源和講解的pdf文件窑睁，還有能在不同平臺(tái)下運(yùn)行的解釋器昂拂。
Lambda演算是一套用于研究函數(shù)定義、函數(shù)應(yīng)用和遞歸的形式系統(tǒng)溉奕。它由 Alonzo Church 和 Stephen Cole Kleene 在 20 世紀(jì)三十年代引入压语，Church 運(yùn)用 lambda 演算在 1936 年給出 判定性問題 (Entscheidungsproblem) 的一個(gè)否定的答案啸罢。這種演算可以用來清晰地定義什么是一個(gè)可計(jì)算函數(shù)。關(guān)于兩個(gè) lambda 演算表達(dá)式是否等價(jià)的命題無法通過一個(gè)通用的算法來解決胎食，這是不可判定性能夠證明的頭一個(gè)問題扰才，甚至還在停機(jī)問題之先。
這篇文章寫于軟工與計(jì)算一剛剛上完Lambda演算之后厕怜，因?yàn)槔碚摵蛻?yīng)用之間存在很大的距離衩匣，很多人覺得Lambda演算沒有什么作用，這篇文章注在以更簡單直白的語言為大家講解Lambda演算并且告訴大家這個(gè)東西究竟有什么用粥航。
首先先講一講Lambda演算里面得幾個(gè)定義和幾個(gè)操作：
定義
定義1. ?? 項(xiàng)
假設(shè)我們有一個(gè)無窮的字符串集合琅捏，里面的元素被稱為變量（和程序語言中變量概念
不同，這里就是指字符串本身）递雀。那么 ?? 項(xiàng)定義如下：
- 所有的變量都是 ?? 項(xiàng)（名為原子）
- 若 ?? 和 ?? 是 ?? 項(xiàng)柄延，那么 (?? ?? ) 也是 ?? 項(xiàng)（名為應(yīng)用）
- 若 ?? 是 ?? 項(xiàng)而 ?? 是一個(gè)變量，那么 (????.??) 也是 ??項(xiàng)（名為抽象）缀程。
解釋
1.函數(shù)包括因變量和自變量搜吧，自變量作為變量可以看成 ?? 項(xiàng)市俊，因變量本質(zhì)上也是一個(gè)變量（廢話），所以因變量也是變量滤奈，可以簡單的認(rèn)為幾乎所有的東西都是 ?? 項(xiàng)
2.簡單來說秕衙，就是可以將括號(hào)內(nèi)部的東西看成一個(gè)整體。
3.即一種函數(shù)的表達(dá)方式僵刮，??表示這是一個(gè)函數(shù)据忘，??是函數(shù)里的一個(gè)變量，??是表達(dá)式
（下面為了方便起見搞糕，所有的??都用\代替勇吊，這也是解釋器中的寫法）
這些都是??項(xiàng)
(????.(?? ??))
(??(????.(????.??)))
((((?? ??) ??) ??) ??)
(((????.(????.(?? ??))) ??) ??)
((????.??) (????.(?? ??)))
(????.(?? ??))
在lambda演算里面，括號(hào)是非常重要的（在一般的數(shù)學(xué)里也很重要）窍仰，它涉及到了運(yùn)算的順序和后面β規(guī)約的時(shí)候能不能正確規(guī)約
下面介紹三個(gè)括號(hào)省略的規(guī)則：
1.最外層的括號(hào)可以省略汉规，(\x.x)可以寫成\x.x
2.左結(jié)合的應(yīng)用型的lambda項(xiàng)，如(((MN)P)Q)驹吮，括號(hào)可以省略针史，表示為M N P Q（這個(gè)規(guī)則十分重要）
3.抽象型的lambda項(xiàng)，(????.??)的M里最外層的括號(hào)可以省略碟狞，如\x.(xy)可以寫成\x.xy
省略表示
????.????.?? ?? ?? ??
(????.????.?? ??) ?? ??
????.(????.?? (?? ??)) ????.?? (?? ??)
????.????.?? ?? ????.??
完整的lambda項(xiàng)
(????.(????.(((?? ??) ??) ??)))
(((????.(????.(?? ??))) ??) ??)
(????.((????.(?? (?? ??))) (????.(?? (?? ??)))))
(????.(????.((?? ??) (????.??))))
在后面演算的時(shí)候啄枕，將括號(hào)復(fù)原是非常重要的事情
定義2：語法全等
我們用恒等號(hào)來表示兩個(gè)lambda項(xiàng)完全相同，即他們具有完全相同的結(jié)構(gòu)族沃，對(duì)應(yīng)位置上的變量也完全相同频祝，就像矩陣全等一樣
定義3：自由變量
對(duì)一個(gè) ?? 項(xiàng) ??，我們可以定義 ?? 中自由變量的集合 FV(??) 如下：
- FV(??) = {??}
- FV(????.??) = FV(??) \ {??}
- FV(?? ?? ) = FV(??) ∪ FV(?? )
從第 2 可以看出抽象 ????.?? 中的變量 ?? 是要從 ?? 中被排除出自由變量這個(gè)集合的脆淹。若 ?? 中有??常空，我們可以說它是被約束的。據(jù)此可以進(jìn)一步定義約束變量集合盖溺。值得注意的是漓糙，對(duì)同一個(gè) ?? 項(xiàng)來說，這兩個(gè)集合的交集未必為空烘嘱。
幾個(gè)簡單的例子：
?? 項(xiàng) ??的 自由變量集合 FV(??)
????.????.?? ?? ?? ??的自由變量集合 {??, ??}
?? ?? ?? ?? 的自由變量集合{??, ??, ??, ??}
?? ?? ????.????.?? 的自由變量集合{??, ??}
（注意昆禽，在第四個(gè)例子中，\y.\x.x中被約束的變量確實(shí)是x y拙友，但是這和開頭的x y不同为狸，因?yàn)閈y.\x.x同樣可以寫成\a.\b.b，這就像f(x)可以寫成f(a)一樣遗契，抽象中的??只是一個(gè)符號(hào)而已，但是符號(hào)的重復(fù)會(huì)給計(jì)算帶來很大的困難病曾，建議還是使用不同的??牍蜂。另一方面漾根，如果對(duì)于lambda項(xiàng)P來說，F(xiàn)V(P) = ?鲫竞，則稱 P 是 封閉的辐怕，這樣的 P 又稱為組合子。）
定義4：出現(xiàn)
對(duì)于 ?? 項(xiàng) ?? 和 ??从绘，可以定義一個(gè)二元關(guān)系出現(xiàn)寄疏。我們說 ?? 出現(xiàn)在 ?? 中，是這樣定義的：
- ?? 出現(xiàn)在 ?? 中僵井；
- 若 ?? 出現(xiàn)在 ?? 中或 ?? 中陕截，則 ?? 出現(xiàn)在 (?? ?? ) 中；
- 若 ?? 出現(xiàn)在 ?? 中或 ?? ≡ ??批什，則 ?? 出現(xiàn)在 (????.??) 中农曲。
定義5：替換
對(duì)任意 ??, ??, ??，定義 [??/??] ?? 是把 ?? 中出現(xiàn)的自由變量 ?? 替換成 ?? 后得到的結(jié)果驻债，這個(gè)替換有可能改變部分約束變量名稱以避免沖突乳规。
其實(shí)在原文本中給出了7個(gè)非常抽象的例子，在這里筆者用簡單的語言來描述一下這里發(fā)生了什么事情
對(duì)于\f.\x. f (\f.\x.x) f x這個(gè)lambda項(xiàng)來說合呐，有些人會(huì)把f或者（f x）當(dāng)成一個(gè)lambda項(xiàng)替換開頭的\f.\x暮的，這是不可以的（但可以替換它前一個(gè)括號(hào)里的抽象），因?yàn)樵谶@個(gè)lambda項(xiàng)的真實(shí)表達(dá)式（即補(bǔ)滿了括號(hào)）中淌实，f x均是約束變量青扔，不能替換自己，另一方面翩伪，lambda項(xiàng)中的變量都是假變量微猖，即都是無意義的符號(hào)變量，就像定積分中的
一樣缘屹，你把x換成t或者別的不影響任何事情凛剥。
說到底，lambda演算還是一種解釋性的語言轻姿，它并不要求計(jì)算出任何具體的數(shù)值犁珠，而是去解釋這個(gè)函數(shù)/抽象，并且可以隨意替換互亮。
定義 6：?? 變換和 ?? 等價(jià)
設(shè) ????.?? 出現(xiàn)在一個(gè) ?? 項(xiàng) ?? 中犁享，且設(shè) ?? ? FV(??)，那么把 ????.?? 替換成????.[??/??] ??
的操作被稱為 ?? 的 ?? 變換豹休。當(dāng)且僅當(dāng)若 ?? 經(jīng)過有限步（包括零步）?? 變換后炊昆，得到新的 ?? 項(xiàng) ??，則我們可以稱 ?? 與 ?? 是 ?? 等價(jià)的。
這個(gè)就是上面說的假變量
定義 7：?? 規(guī)約
形如(????.??) ??的 ?? 項(xiàng)被稱為 ?? 可約式凤巨，對(duì)應(yīng)的項(xiàng)[??/??] ??則稱為 ?? 縮減項(xiàng)视乐。當(dāng) ?? 中含有 (????.??) ?? 時(shí)，我們可以把 ?? 中的 (????.??) ?? 整體替換成 [??/??] ??敢茁，用 ??指稱替換后的得到的項(xiàng)佑淀，那么我們說 ?? 被 ?? 縮減為 ??，當(dāng) ?? 經(jīng)過有限步（包括零步）的 ?? 縮減后得到 ??彰檬，則稱 ?? 被 ?? 規(guī)約到 ??
這個(gè)就是剛剛說的替換的事情
到這里伸刃，整個(gè)lambda演算的體系已經(jīng)基本建立起來了，只需要再定義一些ZERO逢倍，ADD捧颅，POW，TRUE瓶堕，F(xiàn)ALSE等的lambda項(xiàng)即可隘道，也即程序設(shè)計(jì)語言。
ZERO = \f.\x.x
SUCC =\n.\f.\x.f(n f x)
PLUS = \m.\n.m SUCC n
MULT = \m.\n.\f.m(n f)
POW = \b.\e.e b
PRED = \n.\f.\x.n(\g.\h.h(g f))(\u.x)(\u.u)
SUB = \m.\n.n PRED m
一個(gè)簡單的例子
SUCC ZERO
? \n.\f.\x.f (n f x) \f.\x.x
? \f.\x.f (\f.\x.x) f x
? \f.\x.f x
TREU = \x.\y.x
FALSe = \x.\y.y
AND = \p.\q.p q p
OR = \p.\q.p p q
NOT = \p.\a.\b.p b a
IF = \p.\a.\b.p a b
ISZERO = \n.n(\x.FALSE)TRUE
LEQ = \m.\n.ISZERO(SUB m n)[如果GEQ將m n 交換了位置]
EQ = \m.\n. AND(LEQ m n)(LEQ n m)
到這里郎笆，Lambda里面的基本定義和易錯(cuò)易混的地方筆者已經(jīng)全部解釋清楚了谭梗。接下來還有一個(gè)叫不動(dòng)點(diǎn)的概念，主要是用來處理遞歸/迭代的Lambda表達(dá)式的雙重應(yīng)用宛蚓。
Y = \g.(\x.g (x x))\x.g(x x)
YF = (\g.(\x.g (x x))\x.g(x x)) F
= (\x.F (x x))\x.F(x x)
= F(\x.F(x x))(\x.F(x x))
= F(YF)
最后把軟工一的十道題放上來激捏，供大家練習(xí)和參考。
1.I = \x.x
S = \x.\y.\z.x z(y z)
I =S I = \x.\y.\z.x z(y z) \x.x
=\y.\z. (\x.x)z(y z)
=\y.\z. z(y z)
I m n = \y.\z.z(y z) m n
= n (m n)
2.ZERO = \f.\x.x
SUCC = \n.\f.\x.f(n f x)
SUCC(SUCC ZERO)=SUCC(\n.\f.\x.f(n f x) \f.\x.x)
=SUCC(\f.\x.f(\f.\x.x)f x)
=SUCC(\f.\x.f x)
=\n.\f.\x.f(n f x) (\f.\x.f x)
=\f.\x.f (\f.\x.f x)f x
=\f.\x.f f x
3.POW = \b.\e.e b(TWO = \f.\x.f f x THREE = \f.\x.f f f x)
POW TWO THREE=\b.\e.e b TWO THREE
=THREE TWO
=\f.\x. f(f(f(x))) TWO
=\x. TWO(TWO(TWO(x)))
=\x. TWO(TWO(\a.\b. a(a(b)) (x))
=\x. TWO(TWO \b. x(x(b))
=\x. TWO((\c.\d. c(c(d))(\b. x(x(b)) ))
=\x. TWO(\d. (\b. x(x(b)) ( \b. x(x(b)) d ) ) )
=\x. TWO(\d. (\b. x(x(b)) ( \b. x(x(b)) d ) ) )
=\x. TWO(\d. (\b. x(x(b)) ( x(x(d)) ) ) )
=\x. TWO(\d. (x(x(x(x(d))))) )
=\x. \e.\f. e(e(f)) (\d. (x(x(x(x(d))))) )
=\x. \f. (\d. (x(x(x(x(d))))) ) ( ( \d. (x(x(x(x(d))))) ) f))
=\x. \f. (\d. (x(x(x(x(d))))) ) (x(x(x(x(f)))))
=\x. \f. (x(x(x(x(x(x(x(x(f)))))))))
=\f. \x. (f(f(f(f(f(f(f(f(x)))))))))
NOT(NOT TRUE)=(\p.\a.\b.p b a)((\p.\a.\b.p b a)(\x.\y.x))
=(\p.\a.\b.p b a)((\a.\b.(\x.\y.x) b a))
=(\p.\a.\b.p b a)(\a.\b.b)
=(\a.\b.(\a.\b.b) b a)
=(\a.\b.a)= TRUE
IF(OR FALSE FALSE)a b=IF((\p.\q.p p q)(\x.\y.y)(\x.\y.y))a b
=(\p.\a.\b.p a b)((\p.\q.p p q)(\x.\y.y)(\x.\y.y))a b
=(\p.\a.\b.p a b)((\x.\y.y)(\x.\y.y)(\x.\y.y))a b
=(\p.\a.\b.p a b)(\x.\y.y)a b
=\x.\y.y a b
=bLEQ=\m.\n.ISZERO(SUB m n)
GEQ =NOT LEQ
=(\p.\a.\b.p b a) LEQ
=\a.\b (\m.\n ISZERO(SUB m n)) b a
=\a.\b(ISZERO(SUB b a))FACT1 =\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n)))
FACT = FACT1 FACT1
FACT THREE = FACT1 FACT1 THREE
=\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) \f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) THREE
=IF(ISZERO THREE)ONE(MULT THREE (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) \f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) (PRED THREE)))
=(MULT THREE (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) \f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) (PRED THREE)))
=(MULT THREE (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) \f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) TWO))
=(MULT THREE (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) \f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) TWO))
=(MULT THREE (IF(ISZERO TWO)ONE(MULT TWO ((\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) (PRED TWO))))
=(MULT THREE TWO ((\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) (PRED TWO))))
=(MULT THREE TWO ((\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))) (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n)))ONE)))
=(MULT THREE TWO ((IF(ISZERO ONE)ONE(MULT ONE ((\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n)))ONE) (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))))(PRED ONE))) ))
=(MULT THREE TWO (MULT ONE ((\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n)))ONE) (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))))(PRED ONE))) ))
=(MULT THREE TWO (MULT ONE ((\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n)))ONE) (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n))))ZERO))))
=(MULT THREE TWO (MULT ONE ((IF(ISZERO ZERO)ONE(MULT ZERO ((\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n)))) (\f.\n.IF(ISZERO n)ONE(MULT n (f f (PRED n)))) (PRED n)))ONE) ))))
=(MULT THREE TWO (MULT ONE ONE))
=\f.\x f f f f f f x
7.ADD = W(\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))
ADD TWO FOUR = W(\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) TWO FOUR
= \x.x (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) TWO FOUR
= (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) TWO FOUR
=(IF(ISZERO FOUR)TWO((\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))(SUCC TWO)(PRED FOUR)))
=IF(ISZERO FOUR)TWO((\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))(THREE)(THREE))
=(\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))(\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) THREE THREE
=IF(ISZERO THREE)THREE((\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))(SUCC THREE)(PRED THREE))
=(\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))FOUR TWO
=IF(ISZERO TWO)FOUR((\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))(SUCC FOUR)(PRED TWO))
=(\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))FIVE ONE
=IF(ISZERO ONE)FIVE((\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))(SUCC FIVE)(PRED ONE))
=(\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))SIX ZERO
=IF(ISZERO ZERO)SIX((\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m))) (\f.\n.\m.IF(ISZERO m)n(f f(SUCC n)(PRED m)))(SUCC SIX)(PRED ZERO))
=SIX = \f.\x f f f f f f x
8.FACT2 =\f.\n. IF(ISZERO n)ONE(MULT n(f (PRED n)))
FACTY = Y FACT2
FACTY THREE = Y FACT2 THREE
=FACT2(Y FACT2) THREE
=\f.\n. IF(ISZERO n)ONE(MULT n(f (PRED n)))(Y FACT2)THREE
=IF(ISZERO THREE)ONE(MULT THREE (Y FACT2 (PRED THREE)))
=IF(ISZERO THREE)ONE(MULT THREE (FACT2(Y FACT2)(TWO)))
=MULT THREE (FACT2(Y FACT2) TWO)
=MULT THREE (IF(ISZERO TWO)ONE(MULT TWO (Y FACT2 (PRED TWO))))
=MULT THREE (MULT TWO (Y FACT2 (ONE)))
=MULT THREE (MULT TWO (MULT ONE (Y FACT2 ZERO)))
=MULT THREE (MULT TWO (MULT ONE ONE))
=MULT THREE (MULT TWO ONE)
=MULT THREE TWO
=\f.\x. f f f f f f x
CAR = \p.p TRUE
CDR =\p.p FALSE
TRUE = \x.\y.x
FALSE =\x.\y.y
CAR(CDR(CONS a(CONS b(CONS c NIL))))=\p.p TRUE (\t.t FALSE(CONS a(CONS b(CONS c NIL))))
=\p.p TRUE(\t.t (\x.\y.y)(CONS a(CONS b(CONS c NIL))))
=\p.p TRUE(\x.\y.y CONS a(CONS b(CONS c NIL)))
=\p.p TRUE(CONS b(CONS c NIL))
=\x.\y.x (CONS b (CONS c NIL))
= bLENGTH NIL =LENGTH \x.TRUE
=Y (\g.\c.\x. NULL x c (g (SUCC c) (CDR x))) ZERO NIL
=Y F ZERO \x.TRUE
=(\g.\c.\x. NULL x c (g (SUCC c) (CDR x)))(Y F )ZERO NIL
=NULL NIL ZERO (Y F(SUCC ZERO)(CDR NIL))
=(\p.p(\x.\y.FALSE)) NIL ZERO(Y F(SUCC ZERO)(CDR NIL))
=(\x.TRUE(\x.\y.FALSE))ZERO(Y F(SUCC ZERO)(CDR NIL))
=\x.\y.x ZERO (Y F(SUCC ZERO)(CDR NIL))
=ZERO
