上一篇我們已經(jīng)建好了lambda演算大廈的地基杰刽，接下來需要了解的就是如何在此基礎(chǔ)上構(gòu)造用于計算的一些通用工具了菠发，比如自然數(shù)贺嫂、布爾值、基本運算和布爾運算等等第喳。
丘奇數(shù)(Church Numerals)
在介紹丘奇數(shù)之前糜俗，需要通過定義自然數(shù)的皮亞諾公理(Peano Axioms)來說明自然數(shù)的本質(zhì)特征：
1. 皮亞諾公理
皮亞諾公理系統(tǒng)由五條基于自然數(shù)集N和后繼函數(shù)S的公理組成：
- 0∈N
- x∈N→S(x)∈N
- x∈N→S(x)≠0
- x∈N∧y∈N∧S(x)=S(y)→x=y
- 0∈M∧?x(x∈M→S(x)∈M)→N?M for any property M (axiom of induction).
皮亞諾公理規(guī)定了自然數(shù)集就是從0開始通過后繼函數(shù)S構(gòu)成的集合（注：最初的皮亞諾公理中規(guī)定自然數(shù)從1開始），其中單射S(n)對應(yīng)到我們的日常生活就是n+1悠抹，S(0)就是1锌钮，S(S(0))就是2梁丘，以此類推氛谜。
并且值漫，很明顯的，皮亞諾公理系統(tǒng)描述的是自然數(shù)的本質(zhì)性質(zhì)而與表示方式關(guān)系不大杨何，用阿拉伯數(shù)字表示就是{0,1,2,...}酱塔，用漢字表示就是{〇,一,二,...}，用英文表示就是{zero,one,two,...}危虱，按皮亞諾公理表示就是{0,S(0),S(S(0)),...}羊娃，在lambda演算中表示就是丘奇數(shù)(Church Numerals)。
2. 丘奇數(shù)
根據(jù)皮亞諾公理我們可以知道埃跷，只要確定了自然數(shù)0和后繼函數(shù)S蕊玷，就可以根據(jù)公理獲得所有的自然數(shù)。由于lambda演算中只有函數(shù)弥雹，因此自然數(shù)0也需要用函數(shù)來表示垃帅，這個函數(shù)具有自然數(shù)0的性質(zhì)，表示為：
0 ≡ λf.λx.x
而后繼函數(shù)S在lambda演算中則表示為：
S ≡ λn.λf.λx.f (n f x)
于是這些丘奇數(shù)依次表示為：
0 ≡ λf.λx.x
1 ≡ λf.λx.f x
2 ≡ λf.λx.f (f x)
3 ≡ λf.λx.f (f (f x))
...
對后繼函數(shù)S和丘奇數(shù)的簡單驗證如下：
S 0
≡ (λn.λf.λx.f (n f x)) λf.λx.x
= (λf.λx.f (n f x))[n := λf.λx.x] //beta
= (λg.λy.g (n g y))[n := λf.λx.x] //alpha
= λg.λy.g ((λf.λx.x) g y) //substitute
= λg.λy.g (x[f := g, x := y]) //beta
= λg.λy.g y //substitute
≡ 1
那么為什么要這么表示呢剪勿？
就個人理解來講贸诚，在lambda演算中，由于其函數(shù)本位的指導(dǎo)思想窗宦，丘奇數(shù)表示為：
n ≡ λf.λx.fnx
每個丘奇數(shù)都是一個高階函數(shù)(higher-order function)赦颇，即輸入和輸出也包含函數(shù)的函數(shù)，其中fnx表示把輸入函數(shù)f應(yīng)用于參數(shù)x上n次赴涵，即
- 丘奇數(shù)代表的自然數(shù)意為將函數(shù)應(yīng)用于參數(shù)的次數(shù)，它滿足皮亞諾公理订讼，具備自然數(shù)的性質(zhì)髓窜；
- 后繼函數(shù)S意為將函數(shù)多應(yīng)用一次，是從自然數(shù)映射到丘奇數(shù)的加一操作。
3. 相關(guān)運算
下面我們可以進行l(wèi)ambda演算中一些相關(guān)運算的學習了寄纵，其間需要多與與丘奇數(shù)相互交叉理解并參照自然數(shù)運算的原理鳖敷、過程和結(jié)果，這樣能更好的解決諸如“為什么這個運算要這樣表示程拭？”此類疑問定踱。
3.1 加法(addition)
我們已經(jīng)知道丘奇數(shù)n ≡ λf.λx.fnx意為將f應(yīng)用于x上n次，那么根據(jù)加法的性質(zhì)恃鞋，要計算丘奇數(shù)m和n的和崖媚，就可以將函數(shù)應(yīng)用于n上m次(m f n -> m f (n f x))，即
PLUS ≡ λm.λn.λf.λx.m f (n f x)
事實上后繼函數(shù)S作為+1在lambda演算中的映射恤浪，也就是經(jīng)過歸約后的PLUS 1：
PLUS 1
≡ (λm.λn.λf.λx.m f (n f x)) (λf.λx.f x)
= (λn.λf.λx.m f (n f x))[m := λf.λx.f x] //beta
= (λn.λg.λy.m g (n g y))[m := λf.λx.f x] //alpha
= λn.λg.λy.(λf.λx.f x) g (n g y) //substitute
= λn.λg.λy.g (n g y) //beta & substitute
= λn.λf.λx.f (n f x) // alpha
≡ S
那么換一個角度考慮畅哑，PLUS m n其實也可以理解為將S應(yīng)用于n上m次，即
PLUS
≡ λm.λn.λf.λx.m f (n f x)
≡ λm.λn.m S n
試著驗證一下吧~
3.2 乘法(multiplication)
接下來要介紹的是丘奇乘法水由，通過自然數(shù)乘法的性質(zhì)荠呐，可以進行類比，兩個丘奇數(shù)m和n的乘法結(jié)果應(yīng)當表示這樣一個丘奇數(shù)p ≡ λf.λx.fpx：將f應(yīng)用于x上p = m * n次砂客。
顯然泥张，要計算這樣的結(jié)果p，可以
- 將
n先應(yīng)用于f上鞠值，得到將f應(yīng)用于參數(shù)x上n次的中間函數(shù)TMP媚创； - 然后將
m應(yīng)用于TMP上，即再把TMP應(yīng)用于參數(shù)x上m次齿诉，這樣就可以得到將f應(yīng)用于x上m * n次的結(jié)果p筝野。
是不是也很簡單？這樣我們就重新“發(fā)明”了丘奇乘法：
multiply m n f = m (n f)
于是它的lambda表達式便可以得到了：
MULT ≡ λm.λn.λf.m (n f)
MULT ≡ λm.λn.λf.λx.m (n f) x
注意這是丘奇乘法的兩種等價表示方式粤剧，可以通過eta歸約來互相轉(zhuǎn)換歇竟。
