1.3 自然数和计算机程序

现代计算机系统和在其上构建的程序已经非常复杂宏伟了。人们并非先建立了计算机程序的公理系统，然后演绎出这些成果；而是先取得了应用的巨大成功，然后才逐渐将计算机科学的基石数学化、形式化、严谨化。这种有趣的现象在人类历史上已经不是第一次了。牛顿和莱布尼茨在17世纪发展了微积分，然后被几代数学家应用到了各种领域，包括流体力学、天文学等。但是直到19世纪才由魏尔斯特拉斯、柯西等人将微积分的理论严格化[4]。

我们也模仿一下这样的过程，看看如何根据皮亚诺公理，用计算机程序定义自然数。在一个没有0、1、2、……这些数字的程序系统中，我们可以这样定义自然数[4]：

这一定义说：一个自然数或者为零，或者是另一自然数的后继。符号“|”表示互斥的关系。它自然蕴含了零不是任何自然数后继这一公理。在此基础上，我们可以进一步定义出自然数的加法：

加法定义包含两部分。首先任何自然数和零相加等于它本身；并且某个自然数和另一个数的后继相加，等于这两个数相加的后继。写成数学符号为

我们来验证一下2+3。自然数2为succ(succ zero)，而3为succ(succ(succ zero))。根据加法的定义2+3为

最终结果的确是零的五重后继，也就是5。从零开始一次一次地套用后继函数很麻烦。如果要表示100，这种记法要写很多行并且容易出错。为此，我们用下面的简单记法表示自然数n：

它表示从零开始，不断叠加使用succ函数n次。foldn函数可以具体实现如下：

foldn定义了在自然数上的一种操作，只要令z为zero，令f为succ就可以实现叠加后继若干次，从而获得某个特定的自然数。我们可以用前几个自然数验证一下：

定义好加法之后，我们再来定义自然数的乘法：

这里使用了刚定义好的加法。这一定义写成数学符号为

与通常的观念不同，加法和乘法的交换律、结合律既不是公理，也不是公设。它们都是定理，可以用皮亚诺公理和定义证明。以加法结合律为例，如图1.4所示。结合律是说(a+b)+c=a+(b+c)。我们先证明当c=0时它是对的。根据加法定义的第一条规则：

然后是递推步骤，假设(a+b)+c=a+(b+c)成立，我们要推出(a+b)+c′=a+(b+c′)。

这样就证明了加法的结合律。但加法交换律的证明却并不简单，如图1.5所示，本书附录给出了完整的证明。

练习1.1

1.定义0的后继为1，证明对于任何自然数都有a·1=a。

2.证明乘法分配律。

3.证明乘法结合律和交换律。

4.如何利用皮亚诺公理验证3+147=150？

5.试给出乘法分配律、乘法结合律和乘法交换律的几何解释。