上一篇我们已经建好了lambda演算大厦的地基，接下来需要了解的就是如何在此基础上构造用于计算的一些通用工具了，比如自然数、布尔值、基本运算和布尔运算等等。

丘奇数(Church Numerals)

在介绍丘奇数之前，需要通过定义自然数的皮亚诺公理(Peano Axioms)来说明自然数的本质特征：

1. 皮亚诺公理

皮亚诺公理系统由五条基于自然数集N和后继函数S的公理组成：

1. 0∈N
2. x∈N→S(x)∈N
3. x∈N→S(x)≠0
4. x∈N∧y∈N∧S(x)=S(y)→x=y
5. 0∈M∧∀x(x∈M→S(x)∈M)→N⊆M for any property M (axiom of induction).

皮亚诺公理规定了自然数集就是从0开始通过后继函数S构成的集合（注：最初的皮亚诺公理中规定自然数从1开始），其中单射S(n)对应到我们的日常生活就是n+1，S(0)就是1，S(S(0))就是2，以此类推。
并且，很明显的，皮亚诺公理系统描述的是自然数的本质性质而与表示方式关系不大，用阿拉伯数字表示就是{0,1,2,...}，用汉字表示就是{〇,一,二,...}，用英文表示就是{zero,one,two,...}，按皮亚诺公理表示就是{0,S(0),S(S(0)),...}，在lambda演算中表示就是丘奇数(Church Numerals)。

2. 丘奇数

根据皮亚诺公理我们可以知道，只要确定了自然数0和后继函数S，就可以根据公理获得所有的自然数。由于lambda演算中只有函数，因此自然数0也需要用函数来表示，这个函数具有自然数0的性质，表示为：

0 ≡ λf.λx.x

而后继函数S在lambda演算中则表示为：

S ≡ λn.λf.λx.f (n f x)

于是这些丘奇数依次表示为：

0 ≡ λf.λx.x
1 ≡ λf.λx.f x
2 ≡ λf.λx.f (f x)
3 ≡ λf.λx.f (f (f x))
...

对后继函数S和丘奇数的简单验证如下：

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演算中，由于其函数本位的指导思想，丘奇数表示为：
n ≡ λf.λx.fnx
每个丘奇数都是一个高阶函数(higher-order function)，即输入和输出也包含函数的函数，其中fnx表示把输入函数f应用于参数x上n次，即

• 丘奇数代表的自然数意为将函数应用于参数的次数，它满足皮亚诺公理，具备自然数的性质；
• 后继函数S意为将函数多应用一次，是从自然数映射到丘奇数的加一操作。

3. 相关运算

下面我们可以进行lambda演算中一些相关运算的学习了，其间需要多与与丘奇数相互交叉理解并参照自然数运算的原理、过程和结果，这样能更好的解决诸如“为什么这个运算要这样表示？”此类疑问。

3.1 加法(addition)

我们已经知道丘奇数n ≡ λf.λx.fnx意为将f应用于x上n次，那么根据加法的性质，要计算丘奇数m和n的和，就可以将函数应用于n上m次(m f n -> m f (n f x))，即

PLUS ≡ λm.λn.λf.λx.m f (n f x)

事实上后继函数S作为+1在lambda演算中的映射，也就是经过归约后的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应用于n上m次，即

PLUS
≡ λm.λn.λf.λx.m f (n f x) 
≡ λm.λn.m S n

试着验证一下吧~

3.2 乘法(multiplication)

接下来要介绍的是丘奇乘法，通过自然数乘法的性质，可以进行类比，两个丘奇数m和n的乘法结果应当表示这样一个丘奇数p ≡ λf.λx.fpx：将f应用于x上p = m * n次。
显然，要计算这样的结果p，可以

1. 将n先应用于f上，得到将f应用于参数x上n次的中间函数TMP；
2. 然后将m应用于TMP上，即再把TMP应用于参数x上m次，这样就可以得到将f应用于x上m * n次的结果p。

是不是也很简单？这样我们就重新“发明”了丘奇乘法：

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归约来互相转换。

To be continued...