目前的数字，只能通过这样的方式来定义。

z = zero()

one = next(z)

two = next(one)

three = next(two)

four = next(three)

而且除了定义之外，我们对这些数字还不能做什么。

让我们首先建立自然数的

加法运算

。

我们利用归纳公理，这样定义加法的规则：

①任何数N加上0都不变(N+0 => N)

②任何数N加上“M的后继”，等于(N+M)的后继(N+ next(M) => next(N+M))

根据规则②，我们可以看到

N+one(N+“zero的后继”)=> N+ next(z) => next(N+z) => next(N)

N+two(等于N+“one的后继”)=> N+ next(one) => next(N+one) => next(next(N))

...

以此类推

然后我们用python的代码来实现这个规则(自然数加法nAdd)。

def nAdd(a1, a2):

if isZero(a2):

return a1

return nNext(nAdd(a1, nPre(a2)))

代码说明几乎可以省略了，归纳公理，非常恰当地用递归来实现。

为了验证加法的正确性，我们再根据自然公理定义一下什么叫做两个自然数相等。

公理④说明：不同元素有不同的后继。那么显然根据逆否命题，如果两个自然数的前驱相同，就代表这两个自然数相同。

我们这样定义

相等

的规则：

①0与0相等

②0与其他任何自然数都不相等

③任何两个自然数是否相等，取决于它们的前驱数是否相等

自然数相等(nEq)的代码实现如下：

def nEq(a1, a2):

if isZero(a1) and isZero(a2):

return True

elif isZero(a1) or isZero(a2):

return False

else:

return nEq(nPre(a1), nPre(a2))

代码说明也相当直接：如果a1和a2同时为None，肯定是相同；否则，两者任何单一为None都说明不相同。两个数字都不为None时，则取决于他们的前驱是否相同。这时，我们可以做一些测试。

from nature import *

import pytest

def test_basic():

z = zero()

one = nNext(z)

two = nNext(one)

three = nNext(two)

four = nNext(three)

five = nNext(four)

a= nNext(zero())

b= nAdd(z, one)

c= nPre(a)

d= nAdd(two, three)

e= nAdd(two, four)

# 这个时候还没有-1的定义，应当报错

with pytest.raises(TypeError):

minusOne= nPre(z)

# 不相同判断

assert not nEq(two, one)

assert not nEq(b, three)

assert not nEq(four, nNext(five))

# 相同判断

assert nEq(z, nPre(one))

assert nEq(d, five)

assert nEq(e, nNext(five))

# 加法交换律

assert nEq(nAdd(three, four), nAdd(four, three))

# 加法结合律

assert nEq(nAdd(five, nAdd(three, four)), nAdd(nAdd(five, three), four))

测试用了pytest，用法相当简洁的一个测试框架。