Haskell和自然数之基础篇（一） (5-2)

我们可以这样认为，最开始存在一个自然数O，然后我们开始做一个数手指头的动作，就得到一个新的自然数S O，再做一个数手指头的动作，又得到一个新的自然数S (S O)。再继续下去，我们就得到了自然数的序列：O, S O, S (S O), S (S (S O), ...。我们用N 来表示所有自然数的集合，也就是自然数类型，这样每做一次数手指头的动作，我们就得到了一个自然数n ∈ N 的后继S n，这也是一个自然数。我们可以使用Haskell来定义自然数：

data N = O

| S N

deriving (Show)

于是我们就得到了所有的自然数。我们可以通过皮亚诺公理来验证这一点，皮亚诺公理的表述如下：

1. 0 是自然数。

2. 每个自然数都有它的下一个自然数，称为它的后继。

3. 0 不是任何自然数的后继。

4. 不同的自然数有不同的后继数。

5. 如果自然数的某个子集包含 0，并且其中每个元素都有后继元素。那么这个子集就是全体自然数。

这里得到自然数的后继用动作S 来表示，也可把S 看成是自然数集合上的自函数。皮亚诺公理确保了0（也就是我们前面用O来表示的数）是第一个自然数，然后通过不停的获取自然数的后继，我们就得到了所有的自然数。其中皮亚诺公理的第4条确保了S 是一个单射，第5条确保了S 是一个满射，因此S 是一个自同构（这一点在下一篇中会用到）。

另外第5条公理还有如下的等价描述：

任意关于自然数的命题，如果证明了它对自然数 0 是对的，又假定它对自然数 n 为真时，可以证明它对 n的后继n′ 也真，那么命题对所有自然数都真。

这保证了数学归纳法的正确性，使得自然数上可以有归纳函数。因此也叫归纳公理。

我们有了严格定义的自然数，现在可以在这个定义的基础上定义加法、乘法和幂运算了。我们使用Haskell来定义这些运算：

-- | 先定义几个基本函数，用于给后面的运算定义使用

-- 0函数

zero = O

-- 后继函数

succN = S

-- 前驱函数

predN O = error "zero hasn't predecessor"

predN (S n) = n

-- | 这是自然数上的归纳函数

iter :: a -＞ (a -＞ a) -＞ N -＞ a

iter z step O = z

iter z step (S n) = step $ iter z step n

-- | 这是加法的定义，使用了归纳法

plus :: N -＞ N -＞ N

plus m n = iter m succN n

-- | 这是乘法的定义，使用了归纳法

mult :: N -＞ N -＞ N

mult m n = iter O (plus m) n

-- | 这是幂运算的定义，使用了归纳法

pow :: N -＞ N -＞ N

pow m n = iter （S O) (mult m) n

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。