Haskell和自然数之基础篇（二）

我们用一个新的数据类型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 的反函数f⁻¹，于是有f⁻¹ . f . f .f 等于f . f。但是我们没有办法在Haskell中找到任意一个函数的反函数，看来这个实现方式是行不通的。那既然我们做不到逆转世界，那停止世界是可以的，我们可以使用const x 函数来停止世界，将\x -＞ \f -＞ f x 用为\x -＞ \f -＞ x 即\x -＞ const x 来替换，就去除了一次函数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 Eq N where

O == O = True

S _ == O = False

O == S _ = False

S n1 == S n2 = n1 == n2

instance Ord N where

O `compare` O = EQ

S _ `compare` O = GT

O `compare` S _ = LT

S n1 `compare` S n2 = n1 `compare` n2

listToN :: [()] -＞ N

listToN [] = O

listToN (_:xs) = S $ listToN xs

-- 因为有instance Eq ()，所以有下面的

-- instance Eq [()]

-- 因为有instance Ord ()，所以有下面的

-- instance Ord [()]

churchToN :: Church -＞ N

churchToN c = runChurch c S O

instance Eq Church where

c1 == c2 = churchToN c1 == churchToN c2

instance Ord Church where

c1 `compare` c2 = churchToN c1 `compare` churchToN c2

我们通过自然数的前驱来实现减法，皮亚诺形式的自然数减法实现如下所示：

minus :: N -＞ N -＞ N

minus m n

| m＞n = iter m predN n

| otherwise = O

列表形式的自然数减法实现如下所示：

minus :: [()] -＞ [()] -＞ [()]

minus m n

| m＞n = iter m predList n

| otherwise = [()]

丘奇数的减法实现如下所示：

minus :: Church -＞ Church -＞ Church

minus m n

| m＞n = runChurch n predChurch m

| otherwise = Church $ const id

自然数的整除就是通过减法来实现的，具体如下所示：

divide :: N -＞ N -＞ N

m `divide` n | m == 0 && n == 0 = undefined

m `divide` n | m < n = 0

m `divide` n | otherwise = S ((m `minus` n) `divide` n)

至此，我们从最开始的一无所知的状态一步一步的定义了什么是自然数，然后定义了其上的加、减、乘、整除和幂运算这些基本操作，证明了1 + 1 = 2 这个命题。我们还介绍了自然数的其他两种同构形式的自然数定义，即列表表示的自然数和丘奇数。

参考链接：

1.《同构--编程中的数学》 github.com/liuxinyu95/u...

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。