对自然数的理解，是随着自己的成长而不断深入的。在小学的时候觉得很自然就理解了，很自然就用起来了，加、减、乘和整除很自然就学会了，感觉没有什么障碍。到了初中的某一天，突然想到一个问题：1 + 1为什么就是等于2呢？没有理由的就指定了是2，没有推导和证明的过程，感觉很不自然。于是自己思考了好几个月，觉得似乎想通了，写了一篇文章，然后被一些同学嘲笑了。现在也想不起来当时写的是什么了，那篇文章也不知道遗失到哪里去了，不过应该还是没有写清楚究竟为什么1 + 1等于2，要不然我是不会忘记写的是什么的。于是这个令人疑惑的问题一直困扰着我，一直到参加工作，也依然时不时会惦记着这个问题。
直到我学习了Haskell，看到一篇关于自然数的表示文章，用Haskell清晰的定义了自然数，定义了自然数的加法和乘法。我终于明白了1 + 1为什么就是等于2，这个从自然数的定义和加法的定义很自然就可以推导得到了，证明起来很容易。在这之后，又看了皮亚诺公理的自然数定义，对自然数的定义更加清楚了。在这之前，我听说过皮亚诺公理，但是并不感兴趣，还感受不到自然数公理化的意义，所以并没有去看。
大概两个月前，我收到了刘新宇的新书《同构--编程中的数学》，看到了这本书中对自然数的论述，然后又重温了丘奇数的概念。觉得可以写点关于自然数的东西了。这是一个系列，有两篇文章：第一篇讲自然数和丘奇数的基础概念和构造，以及在其上的基本运算，第二篇讲自然数的变换，结合F-Alg来讲如何消除自然数的结构得到其他的类型的值。
好了，让我们从一无所知的状态来开始了解什么是自然数吧。我们最早了解自然数是从数数开始的，当我们不知道桌上一堆东西有多少个时，最简单的办法就是数一数有多少个。数一下手指头是1 个，数两下手指头是2 个，数三下手指头是3 个，这样一直数下去，直到数完了这堆东西。于是我们就得到了一系列的数：1, 2, 3, ...，这些数和数手指头的次数的对应关系如下。
1 ： 数一下手指头
当桌上没有东西的时候，我们就不用数手指头了，因为什么都没有，所以什么也不用做。这个时候我们用0 个来表示桌上东西的数量。于是有下面这个新的数和数手指头的次数的对应关系。
0 ： 什么也不做
因为我们一无所知，就像幼儿园的小朋友一样，还弄不明白两下、三下是怎么来的，是什么意思。我们再来看一遍我们数数的过程，一开始是什么也不做，然后将一个东西摆到桌子的另一边，做一次数手指头的动作，再将一个东西摆到桌子的另一边，再做一次数手指头的动作，这样每将一个东西摆到桌子的另一边，我们都接着做一次数手指头的动作，直到把桌子上的东西数完。于是我们就得到一个数手指头的动作的序列，这个数手指头动作的序列的次数就是东西的个数。因此有下面的数和数手指头的动作序列的对应关系。
0 ： 什么也不做
我们把上面的什么也不做用O 来表示，把数手指头这个动作用S 来表示，于是上面的数和数手指头的动作序列的对应关系就变成了下面这样。
0 ： O
我们可以这样认为，最开始存在一个自然数O，然后我们开始做一个数手指头的动作，就得到一个新的自然数S O，再做一个数手指头的动作，又得到一个新的自然数S (S O)。再继续下去，我们就得到了自然数的序列：O, S O, S (S O), S (S (S O), ...。我们用N 来表示所有自然数的集合，也就是自然数类型，这样每做一次数手指头的动作，我们就得到了一个自然数n ∈ N 的后继S n，这也是一个自然数。我们可以使用Haskell来定义自然数：
data 于是我们就得到了所有的自然数。我们可以通过皮亚诺公理来验证这一点，皮亚诺公理的表述如下：
1. 0 是自然数。
2. 每个自然数都有它的下一个自然数，称为它的后继。
3. 0 不是任何自然数的后继。
4. 不同的自然数有不同的后继数。
5. 如果自然数的某个子集包含 0，并且其中每个元素都有后继元素。那么这个子集就是全体自然数。
这里得到自然数的后继用动作S 来表示，也可把S 看成是自然数集合上的自函数。皮亚诺公理确保了0（也就是我们前面用O来表示的数）是第一个自然数，然后通过不停的获取自然数的后继，我们就得到了所有的自然数。其中皮亚诺公理的第4条确保了S 是一个单射，第5条确保了S 是一个满射，因此S 是一个自同构（这一点在下一篇中会用到）。
另外第5条公理还有如下的等价描述：
任意关于自然数的命题，如果证明了它对自然数 0 是对的，又假定它对自然数 n 为真时，可以证明它对 n的后继n′ 也真，那么命题对所有自然数都真。
这保证了数学归纳法的正确性，使得自然数上可以有归纳函数。因此也叫归纳公理。
我们有了严格定义的自然数，现在可以在这个定义的基础上定义加法、乘法和幂运算了。我们使用Haskell来定义这些运算：
-- | 先定义几个基本函数，用于给后面的运算定义使用
自然数上的归纳函数的定义是对于自然数n ，对其进行归纳的初始值是z ，每一个归纳步调用函数step 。自然数n 是由几个S 构造的，我们就以z 为参数递归调用几次step 函数。比如当自然数n 的值是S (S (S O)时，这是由3 个S 构造的，于是我们就递归调用3 次step 函数，于是结果是step (step (step z)) 。
对于加法，我们是这样定义的，给定一个自然数m，加上一个值为S (S O)的自然数n 时，其结果等于值为S (S m)的自然数。用归纳函数来定义就相当于初始值z 是m ，step 是S 也就是succN ，我们对加数n 做归纳法，也就是自然数n 中由几个S 构造的，我们就递归调用几步S 。于是有了结果的值是S (S m)。
当m 的值是S O 也就是1 ，n 的值也是S O 即1 时，我们有(S O) + (S O) = S (S O)，根据上面的数的对应关系，我们有1 + 1 = 2 。完成了证明，解决了我多年来的疑问。
对于乘法，两个自然数m 和n 相乘，就相当于把n 个m 加起来。用归纳函数来定义就相当于初始值是O，step 是(m +) 也就是plus m ，我们对乘数n 做归纳法。于是乘以一个值为S (S O)的自然数，我们就递归调用两步递归步plus m，于是得到结果值是plus m (plus m O)，就是m + m。
对于幂运算，则和乘法类似，自然数m 的n 次幂的值就等于把n 个m 乘起来。用归纳函数来定义就相当于初始值是S O，step 是(m *) 也就是mult m ，我们对幂数n 做归纳法。于是求m 的一个值为S (S O) 的n 次幂的自然数的值，我们就递归调用两步递归步plus m，于是得到结果值是mult m (mult m (S O))，就是m * m。
减法的定义比较复杂，因为自然数没有负数，因此需要比较两个数的大小来实现减法，这个放到后面一起来定义。
用皮亚诺公理来定义的自然数只是自然数表示的一种形式，我们可以用其他同构的形式来定义和表示自然数。接下来我们将使用列表和函数来表示自然数。
- 用列表表示自然数
列表是包含了同类型元素的一种数据类型，多个同类型的数据列在一起，就组成了列表。当列表内的元素的类型是 () 时，列表就只剩下长度信息了，我们可以用其来表示自然数。
Haskell中列表的定义如下：
data 列表的类型是[a]，当列表内的元素的类型也就是a 为() 时，我们有一个特殊的列表类型[()]。这个列表类型的元素是无具体信息的，其有用的信息就是列表的长度，因此我们可以使用列表类型[()]来表示自然数。比如用[(), (), ()] 来表示皮亚诺形式的自然数S (S (S O))。列表表示的自然数和数的关系如下：
0 我们使用Haskell来定义如下的用列表类型[()] 表示的自然数运算。
-- | 先定义几个基本函数，用于给后面的运算定义使用
列表上的归纳函数的定义是对于列表n，对其进行归纳的初始值是z ，每一个归纳步调用函数step 。列表n 是由元素组成的，我们就以z 为参数递归调用几次step 函数。比如当列表n 的值是[(), (), ()] 时，这是由3 个元素组成的，于是我们就递归调用3 次step 函数，于是结果是step (step (step z)) 。
对于加法，直接用两个列表的连接运算来定义。即将两个列表m 和n 连接起来就实现了列表的加法。
对于乘法，两个列表m 和n 相乘，就相当于把n 个m 加起来。用归纳函数来定义就相当于初始值是[]，step 是(m +) 也就是plus m ，我们对列表n 做归纳法。于是乘以一个值为[(), ()] 的列表，我们就递归调用两步递归步plus m，于是得到结果值是plus m (plus m [])，就是将两个列表m 连接起来。
对于幂运算，则和乘法类似，列表m 的n 次幂的值就等于把n 个m 乘起来。用归纳函数来定义就相当于初始值是[()]，step 是(m *) 也就是mult m ，我们对幂数n 做归纳法。于是求m 的一个值为[(), ()] 的n 次幂的自然数的值，我们就递归调用两步递归步plus m，于是得到结果值是mult m (mult m (S O))，就是m * m。
- 用函数表示自然数（丘奇数）
在纯函数编程语言中（比如Haskell），函数也是一个值，因此我们也可以用函数来表示自然数。这种表述方式时阿隆佐.丘奇发明的，因此也叫丘奇数。
我们知道，函数是可以组合起来，即我们可以把函数f 和g 组合起来得到g . f ，这里运算符 . 就是组合运算（按普遍的定义，是反序的）。那我们把相同的两个函数f 组合起来就得到了f . f，把三个函数f 组合起来就得到了f . f . f，以此类推，我们就可以得到n 个函数f 的组合f . f . f . f ...。我们可以用函数f 的组合来表示自然数，由几个函数f 组合的函数就表示自然数几，比如用f 表示S O ，用f . f 表示S (S O) ，用f . f . f 表示S (S (S O))。至于自然数O ，则用函数id 来表示。丘奇数和数的对应关系如下：
0 于是就有了如下使用Haskell来实现的自然数的函数表示的定义和基本运算。
-- | 用函数来表示自然数的数据类型，就是给定一个函数f得到多个函数f的组合函数。
我们用一个新的数据类型Church来定义丘奇数，这实际上就是以函数f 为参数得到多个函数f 组合的函数的lambda函数的封装类型，其本质就是一个lambda函数，这个lambda函数的返回结果是多个函数f的组合。
当类型Church的lambda的函数参数是(+1) 时，如果这个丘奇数表示的是自然数S (S (S O))，那lambda函数返回的结果是(+1) . (+1) . (+1)，也是一个函数，将这个函数应用到参数0，我们得到了3。可以看到类型Church（丘奇数）本身的定义就是归纳的，因此其归纳函数iter 的实现就是将归纳步step 直接作为参数传递给类型Church的lambda函数，然后将结果函数应用到初始值z ，就得到了归纳函数iter 的结果。
因为丘奇数本身的定义就是归纳的，所以我们就不需要用归纳法来实现加法了，直接用Church本身的定义来实现加法就可以了。比如当丘奇数m 的值为Church (f -> f . f . f)，丘奇数n 的值为Church (f -> f . f) 时，m 加上n 的丘奇数的lambda函数返回的结果是(f . f . f . f . f)，也就是Church (f -> (f . f) . (f . f . f))，因此加法就是由函数的组合运算来实现。
类似的，丘奇数的乘法也使用其本身的定义来实现。当丘奇数m 的值为Church (f -> f . f . f)，丘奇数n 的值为Church (f -> f . f) 时，m 乘以n 的丘奇数的lambda函数返回的结果是(g -> g . g) (f . f . f)，得到Church ((g -> g . g) . (f -> f . f . f))，结果是Church (f -> (f . f . f) . (f . f . f))，因此乘法就是由丘奇数的lambda函数的组合来实现的。
最后，丘奇数的幂运算也可以使用其本身的定义来实现。当丘奇数m 的值为Church (f -> f . f . f)，丘奇数n 的值为Church (f -> f . f) 时，m 的n 次幂的丘奇数的lambda函数返回的结果是(g -> g . g) (h -> h . h . h)，得到Church (f -> ((g -> g . g) (h -> h . h . h)) f)，将g 替换为(h -> h . h . h) 有Church (f -> ((h -> h . h . h) . (h -> h . h . h)) f)，结果是Church (f -> (f . f . f) . (f . f . f) . (f . f . f))，因此幂运算就是将一个丘奇数的lambda函数应用到另一丘奇数的lambda函数的方式来实现的。
丘奇数和前面两个自然数表示形式所不同的是丘奇数的前驱的实现比较难，不像皮亚诺形式的和列表形式的那么简单直观。
我们在前面已经说过，丘奇数的前驱就是从由n 个函数f 组合成的函数中去除一个函数f ，变为由n-1 个函数f 组合成的函数。比如丘奇数的lambda 返回结果是f . f . f，这个丘奇数的前驱的lambda 返回的结果是f . f。最简单的实现就是找到函数f 的反函数
-- 前驱函数，从n个函数f的组合得到n-1个函数f的组合
predChurch n = Church $ f x -> runChurch n (g h -> h (g f)) (const x) id具体的证明就留给聪明的读者吧。
- 自然数的减法和整除的实现
有了自然数的前驱函数，我们就可以实现减法了。前面说过，自然数没有负数，所以我们需要可以比较两个自然数，当自然数m 小于自然数n 时，m - n 的结果是0 。
我们可以将自然数实现为Eq 和Ord 类型类的实例，就可以比较两个自然数了。Haskell的实现如下：
instance 我们通过自然数的前驱来实现减法，皮亚诺形式的自然数减法实现如下所示：
minus 列表形式的自然数减法实现如下所示：
minus 丘奇数的减法实现如下所示：
minus 自然数的整除就是通过减法来实现的，具体如下所示：
divide 列表形式的自然数和丘奇数使用类似的方式，具体实现就留给读者了。
至此，我们从最开始的一无所知的状态一步一步的定义了什么是自然数，然后定义了其上的加、减、乘、整除和幂运算这些基本操作，证明了1 + 1 = 2 这个命题。我们还介绍了自然数的其他两种同构形式的自然数定义，即列表表示的自然数和丘奇数。
有兴趣的读者可以等待下一篇：Haskell和自然数之代数篇。
参考链接：
- 《同构--编程中的数学》https://github.com/liuxinyu95/unplugged
)
