module plfa.Naturals where

夜空中有着难以计数的星星，但其实只有不多于五千颗是肉眼可见的。 可观测宇宙则包含了大约七百亿亿亿亿亿颗恒星。

星星的数量虽多却是有限的，而自然数的数量是无限的。就算用自然数把所有的星星都数尽了， 剩余的自然数也和刚开始时一样多。

自然数是一个归纳数据类型（Inductive Datatype）

大家都熟悉自然数，比如： 

0
1
2
3
...

等等。我们将自然数的类型（Type）记为 ℕ ，并称 0，1，2，3 等数字是类型 ℕ 的值（Value），表示为 0 : ℕ，1 : ℕ，2 : ℕ，3 : ℕ 等。

自然数集是无限的，然而其定义寥寥几行即可写出。如下是表示为一对推理规则（Inference Rules）的自然数定义。 

--------
zero : ℕ

m : ℕ
---------
suc m : ℕ

以及用 Agda 写出的自然数定义： 

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

这里 ℕ 是我们所定义的数据类型（Datatype）的名字，而 zero（零）和 suc （successor，即后继数，的缩写）是该数据类型的构造器（Constructors）。

以上的定义都告诉了我们相同的两件事情：

  • 起始步骤（Base Case）：zero 是一个自然数。
  • 归纳步骤（Inductive Case）：如果 m 是一个自然数，那么 suc m 也是。

进一步地，这两条规则给出的是仅有的产生自然数的方法。因此，可能的自然数包括： 

zero
suc zero
suc (suc zero)
suc (suc (suc zero))
...

我们将 zero 简写为 0；将 suc zero，零的后继数， 也就是排在零之后的自然数，简写为 1；将 suc (suc zero)，也就是 suc 1， 即一的后继数，简写为 2；将二的后继数简写为 3；以此类推。

练习 seven

完整写出 7 的定义。 

-- 在此处书写你的代码

推理规则分析

让我们来分析一下刚才的两条推理规则。每条推理规则包含写在一条水平直线上的零或更多条判断（Judgments），称之为假设（Hypotheses）；以及写在直线下的一条判断，称之为结论（Conclusion）。第一条规则是起始步骤：它没有任何假设，而结论断言 zero 是一个自然数。第二条规则是归纳步骤：它有一条假设，即 m 是自然数，而结论断言 suc m 也是一个自然数。

Agda 定义分析

现在我们来分析刚才的 Agda 定义。关键字 data 告诉我们这是一个归纳定义， 也就是我们正在用构造器定义一个新的数据类型。 

ℕ : Set

这告诉我们 ℕ 是新的数据类型的名字，并且它是一个 Set，也就是在 Agda 中对类型的称呼。 关键字 where 用于分离数据类型的声明和其构造器的声明。 每个构造器在单独的一行里声明，通过缩进来表示它属于对应的 data 声明。 

zero : ℕ
suc  : ℕ → ℕ

这两行给出的是指定了构造器 zero 和 suc 的类型的签名（Signature)， 告诉我们 zero 是一个自然数，suc 则取一个自然数作为参数并返回一个自然数。

读者可能已经注意到了 ℕ 和 → 在键盘上没有对应的按键。它们是 统一码（Unicode）中的符号。在每一章的结尾都会有本章节引入的 Unicode 符号的列表， 以及在 Emacs 编辑器中输入它们的方法。

创世故事

让我们再来看一遍定义了自然数的规则：

  • 起始步骤（Base Case）：zero 是一个自然数。
  • 归纳步骤（Inductive Case）：如果 m 是一个自然数，那么 suc m 也是。

等一下！第二行用自然数定义了自然数，这怎么能被允许呢？这个定义难道不会像“三角形就是三角形”一样无用吗？

实际上，无需利用循环性，我们的自然数定义也是可以被赋予意义的。为了做到这一点，我们甚至只需要处理有限集合，而不必涉及无限的自然数集。

我们可以将这个过程比作是一个创世故事。在最开始，我们对自然数一无所知： 

-- 起初，世上没有自然数。

现在，对我们已知的所有自然数应用之前的规则。起始步骤告诉我们 zero 是一个自然数，所以我们将其加入已知自然数的集合。归纳步骤告诉我们如果（在昨天） m 是一个自然数，那么（在今天）suc m 就也是一个自然数。我们在今天之前并不知道任何自然数，所以归纳步骤在此处不适用。 

-- 第一天，世上有了一个自然数。
zero : ℕ

然后我们重复这个过程。在今天我们知道来自前一天的所有自然数，以及任何通过规则添加的数。起始步骤依然告诉我们 zero 是一个自然数，当然，我们已经知道这件事了。而如今归纳步骤告诉我们，由于 zero 在昨天是自然数， suc zero 在今天也成为了自然数： 

-- 第二天，世上有了两个自然数。
zero : ℕ
suc zero : ℕ

我们再次重复这个过程。现在归纳步骤告诉我们因为 zero 和 suc zero 都是自然数，所以 suc zero 和 suc (suc zero) 也是自然数。我们已经知道前者是自然数了， 但 suc (suc zero) 是新加入的。 

-- 第三天，世上有了三个自然数。
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ

此时规律已经很明显了。 

-- 第四天，世上有了四个自然数。
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ
suc (suc (suc zero)) : ℕ

这个过程可以继续下去。在第 n 天会有 n 个不同的自然数。每个自然数都会在某一天出现。具体来说，自然数 n 在第 n+1 天首次出现。至此，我们并没有使用自然数集来定义其自身，而是根据第 n 天的数集定义了第 n+1 天的数集。

像这样的过程被称作是归纳的（Inductive）。我们从一无所有开始，通过应用将一个有限集合转换到另一个有限集合的规则，逐步生成可能是无限的集合。

定义了零的规则之所以被称作起始步骤，是因为它甚至在我们还不知道其它自然数时就引入了一个自然数。定义了后继数的规则之所以被称作归纳步骤，则是因为它在我们已知自然数的基础上引入更多自然数。其中，起始步骤的重要性不可小觑。如果我们只有归纳规则，我们将在第一天没有任何自然数，第二天，第三天，无论多久也依旧没有。 一个缺失了起始步骤的归纳定义是无用的，就像“三角形就是三角形”一样。

哲学和历史

哲学家可能会观察到，我们对“第一天”、“第二天”等说法的使用暗含了对自然数的理解。 在这个层面，我们的自然数定义也许一定程度上可以被视作循环的，但我们不必为此烦恼。 每个人对自然数都有良好的非形式化的理解，而我们可以将这作为自然数的形式化描述的基础。

尽管自然数从人类开始计数起就被认知，但是其归纳定义却是相对较近的事情。这可以追溯到理查德·戴德金于 1888 年发表的论文 “Was sind und was sollen die Zahlen?“（《数是什么，应该是什么？》）， 以及朱塞佩·皮亚诺于次年发表的著作 “Arithmetices principia, nova methodo exposita” （《算术原理：用一种新方法呈现》）。

编译程序指令

在 Agda 中，任何跟在 -- 之后或者被 {- 和 -} 包裹的文字都被视作一条注释（Comment）。一般的注释对代码没有任何作用，但有一种特殊的注释却是例外。 这种注释被称作编译程序指令（Pragma），被 {-# 和 #-} 包裹。 

{-# BUILTIN NATURAL ℕ #-}

这一行告诉 Agda 数据类型 ℕ 对应了自然数，然后编写者就可以将 zero 简写为 0，将 suc zero 简写为 1，将 suc (suc zero) 简写为 2，以此类推。 只有在给出的数据类型有且只有两个构造器，其中一个没有参数（对应零），另一个仅取一个和被定义的数据类型一样的参数（对应后继数）的时候，这条声明才是合乎规定的。

在启用上述简写的同时，这条编译程序指令也会使用 Haskell 的任意精度整数类型来提供更高效的自然数内部表示。用 zero 和 suc 表示自然数 n 要占用正比于 n 的空间，而将其表示为 Haskell 中的任意精度整数只会占用正比于 n 的对数的空间。

导入模块

我们很快就能够写一些包含自然数的等式了。在开始之前，我们需要从 Agda 标准库中导入相等性的定义和用于等式推理的记号： 

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

第一行代码将标准库中定义了相等性的模块导入当前作用域（Scope）并将其命名为 Eq。第二行打开了这个模块，也就是将所有在 using 从句中指定的名称添加到当前作用域。在这里被添加的名称有相等性操作符 _≡_ 和两个项相等的证据 refl。第三行选取了一个提供用于等价关系推理的操作符的模块，并将在 using 从句中指定的名称添加到当前作用域。在这里被添加的名称有 begin_， _≡⟨⟩_，以及 _∎。我们会在下文中看到这些操作符的使用方法。我们目前把这些名称都当作现成的工具来使用，不深究其细节，但我们会在 相等性 一章学习它们的具体定义。

Agda 用下划线来标注在中缀或多缀（Mixfix）操作符中项出现的位置。因此， _≡_ 和 _≡⟨⟩_ 是中缀的（操作符写在两个项之间），而 begin_ 是前缀的 （操作符写在项之前），_∎ 则是后缀的（操作符写在项之后）。

括号和分号属于少有的几个不能在名称中出现的的字符，所以我们在 using 列表中不需要额外的空白（以消除歧义）。

对自然数的操作是递归函数

既然我们有自然数了，我们可以用它们做什么呢？比如，我们能定义加法、乘法之类的算术操作吗？

我儿时曾花费了大量的时间来记忆加法和乘法表。最开始，运算规则看起来很复杂，我也经常犯错。在发现递归（Recursion）时，我如同醍醐灌顶。 通过这个简单的技巧，有无数种可能的加法和乘法运算，只用几行即可概括。

这是用 Agda 编写的加法的定义： 

_+_ : ℕ → ℕ → ℕ
zero  + n  =  n
suc m + n  =  suc (m + n)

我们来分析一下这个定义。加法是一个中缀操作符，被命名为 _+_，其中参数的位置在书写时被下划线占据。第一行是指定了操作符类型的签名。ℕ → ℕ → ℕ 这个类型说明加法接受两个自然数作为参数，并返回一个自然数。中缀记法只是函数应用的简写， m + n 和 _+_ m n 这两个项是等价的。

这个定义包含一个起始步骤和一个归纳步骤，与自然数的定义相对应。起始步骤说明了用零加一个数返回那个数，即 zero + n 得 n。归纳步骤说明了用一个数的后继数加上另一个数返回两数之和的后继数，即 (suc m) + n 得 suc (m + n)。在加法定义中，构造器出现在了等式左手侧，我们将这称为模式匹配（Pattern Matching）。

如果我们将 zero 写作 0，将 suc m 写作 1 + m，上面的定义就变成了两个熟悉的等式。 

 0       + n  ≡  n
 (1 + m) + n  ≡  1 + (m + n)

因为零是加法的单位元，所以第一个等式成立。又因为加法满足结合律，所以第二个等式也成立。加法结合律的一般形式如下，说明运算结果和括号的位置无关。 

 (m + n) + p  ≡  m + (n + p)

将上面第三个等式中的 m 换成 1，n 换成 m，p 换成 n，我们就得到了第二个等式。在定义中，我们将等于符号写作 =，而在断言两个已经定义了的事物等同时，我们将等于写作 ≡。

加法的定义是递归（Recursive）的，因为在最后一行我们用加法定义了加法。 类似于自然数的归纳定义的情况，这个表面上的循环性并不会造成问题，因为较大的数相加是用较小的数相加定义的。这样的定义被称作是良基的（Well founded）。

例如，我们来计算二加三： 

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩    -- 展开为
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- 归纳步骤
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- 归纳步骤
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- 起始步骤
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- 简写为
    5
  ∎

我们可以只展开需要用到的简写来把同样的推导过程写得更紧凑。 

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    suc (1 + 3)
  ≡⟨⟩
    suc (suc (0 + 3))
  ≡⟨⟩
    suc (suc 3)
  ≡⟨⟩
    5
  ∎

第一行通过取 m = 1 和 n = 3 匹配了归纳步骤，第二行也通过取 m = 0 和 n = 3 匹配了归纳步骤， 最后第三行通过取 n = 3 匹配了起始步骤。

以上两个推导过程都由一个类型签名（含冒号 : 的一行）和一个提供对应类型的项的绑定（Binding）（含等号 = 的一行及之后的部分）组成。在编写代码时我们用了虚拟名称 _。虚拟名称可以被重复使用，在举例时非常方便。除了 _ 之外的名称在一个模块里只能被定义一次。

这里的类型是 2 + 3 ≡ 5，而项，也就是这里写成表格形式的等式链，提供了作为类型的等式成立的证据（Evidence）。这个等式链由 begin 开始，以 ∎ 结束（∎ 可读作 “qed”/“证毕” 或 “tombstone”/“墓碑符号”，后者来自于其外观），并由一系列被 ≡⟨⟩ 分隔的项组成。

其实，上面的两种证明都比实际所需的要长，下面的证明就足以让 Agda 满意了。 

_ : 2 + 3 ≡ 5
_ = refl

Agda 知道如何计算 2 + 3 的值，也可以立刻确定这个值和 5 是一样的。如果一个二元关系（Binary Relation）中每个值都和自己相关，我们称这个二元关系是自反的（Reflexive）。 在 Agda 中，一个值等于其自身的证据写作 refl。

在等式链中，Agda 只检查是否每个项都可以化简到相同的值。如果我们打乱等式顺序， 省略或者加入一些额外的步骤，证明仍然会被接受。我们需要自己确保等式是按一定顺序书写的，以便读者理解。

在这里，2 + 3 ≡ 5 是一个类型，等式链（以及 refl）都是这个类型的项。 换言之，我们也可以把每个项都看作断言 2 + 3 ≡ 5 的证据。这种解释的对偶性————类型作为命题，而项作为证据————是我们在 Agda 中形式化各种概念的核心，也是本书贯穿始终的主题。

需要注意的是，当我们使用证据这个词时，不容一点含糊。这里的证据确凿不移，不像法庭上的证词一样必须被反复权衡以决定证人是否可信。 我们也会使用证明一词表达相同的意思，在本书中这两个词可以互换使用。

练习 +-example

计算 3 + 4，将你的推导过程写成等式链。 

-- 在此处书写你的代码

乘法

一旦我们定义了加法，我们就可以将乘法定义为重复的加法。 

_*_ : ℕ → ℕ → ℕ
zero  * n  =  zero
suc m * n  =  n + (m * n)

计算 m * n 返回的结果是 m 个 n 之和。

重写定义再一次给出了两个熟悉的等式： 

0       * n  ≡  0
(1 + m) * n  ≡  n + (m * n)

因为零乘任何数都是零，所以第一个等式成立。因为乘法对加法有分配律，所以第二个等式也成立。乘法对加法的分配律的一般形式如下： 

(m + n) * p  ≡  (m * p) + (n * p)

将上面第三个等式中的 m 换成 1，n 换成 m，p 换成 n，再根据一是乘法的单位元，也就是 1 * n ≡ n，我们就得到了第二个等式。

这个定义也是良基的，因为较大的数相乘是用较小的数相乘定义的

例如，我们来计算二乘三： 

_ =
  begin
    2 * 3
  ≡⟨⟩    -- 归纳步骤
    3 + (1 * 3)
  ≡⟨⟩    -- 归纳步骤
    3 + (3 + (0 * 3))
  ≡⟨⟩    -- 起始步骤
    3 + (3 + 0)
  ≡⟨⟩    -- 化简
    6
  ∎

第一行通过取 m = 1 和 n = 3 匹配了归纳步骤，第二行也通过取 m = 0 和 n = 3 匹配了归纳步骤，最后第三行通过取 n = 3 匹配了起始步骤。在这里我们省略了声明 _ : 2 * 3 ≡ 6 的签名，因为它很容易从对应的项推导出来。

练习 *-example

计算 3 * 4，将你的推导过程写成等式链。 

-- 在此处书写你的代码

练习 _^_（推荐）

根据如下等式写出乘方的定义。 

n ^ 0        =  1
n ^ (1 + m)  =  n * (n ^ m)

检查 3 ^ 4 是否等于 81。 

-- 在此处书写你的代码

饱和减法

我们也可以定义减法。由于没有负的自然数，如果被减数比减数小， 我们就将结果取零。这种针对自然数的减法变种称作饱和减法（Monus，由 minus 修改而来）。

饱和减法是我们第一次在定义中对两个参数都使用模式匹配： 

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

我们可以做一个简单的分析来说明所有的情况都被考虑了。

  • 考虑第二个参数。
    • 如果它是 zero，应用第一个等式。
    • 如果它是 suc n，考虑第一个参数。
      • 如果它是 zero，应用第二个等式。
      • 如果它是 suc m，应用第三个等式。

这个定义也是良基的，因为较大的数的饱和减法是用较小的数的饱和减法定义的。

例如，我们来计算三减二： 

_ =
  begin
     3 ∸ 2
  ≡⟨⟩
     2 ∸ 1
  ≡⟨⟩
     1 ∸ 0
  ≡⟨⟩
     1
  ∎

我们没有使用第二个等式，但是如果被减数比减数小，我们还是会需要它。 

_ =
  begin
     2 ∸ 3
  ≡⟨⟩
     1 ∸ 2
  ≡⟨⟩
     0 ∸ 1
  ≡⟨⟩
     0
  ∎

练习 ∸-examples（推荐） {#monus-examples}

计算 5 ∸ 3 和 3 ∸ 5，将你的推导过程写成等式链。 

-- 在此处书写你的代码

优先级

我们经常使用优先级（Precedence）来避免书写大量的括号。 函数应用比其它任何操作符都绑定更紧密（或有更高优先级），所以我们可以写 suc m + n 来表示 (suc m) + n。另一个例子是，我们说乘法比加法绑定更紧密，所以可以写 n + m * n 来表示 n + (m * n)。我们有时候也说加法是左结合的，所以可以写 m + n + p 来表示 (m + n) + p。

在 Agda 中中缀操作符的优先级和结合性需要被声明： 

infixl 6  _+_  _∸_
infixl 7  _*_

这声明了操作符 _+_ 和 _∸_ 的优先级为 6，操作符 _*_ 的优先级为 7。因为加法和饱和减法的优先级更低，所以它们绑定不如乘法紧密。 infixl 意味着三个操作符都是左结合的。编写者也可以用 infixr 来表示某个操作符是右结合的，或者用 infix 来表示总是需要括号来消除歧义。

柯里化

我们在之前曾将取两个参数的函数表示成取第一个参数并返回取第二个参数的函数的函数。这种技巧被称作柯里化（Currying）。

类似于别的函数式语言，如 Haskell 和 ML，Agda 在设计时就考虑了让柯里化更易用。函数箭头是右结合的，而函数应用是左结合的。

比如

ℕ → ℕ → ℕ 代表了 ℕ → (ℕ → ℕ)

以及

_+_ 2 3 代表了 (_+_ 2) 3。

_+_ 2 这个项本身代表了一个将参数加二的函数，所以将其应用到三得到了五。

柯里化是以哈斯凯尔·柯里（Haskell Curry）的名字命名的，编程语言 Haskell 也是。 柯里的工作可以追溯到 19 世纪 30 年代。当我第一次了解到柯里化时，有人告诉我柯里化的命名是个归因错误，因为在 20 年代同样的想法就已经被 Moses Schönfinkel 提出了。 我也听说过这样一个笑话：（柯里化）本来该命名成 Schönfinkel 化的，但是咖喱更好吃（curry 也可指调味料咖喱）。直到之后我才了解到，这个对于归因错误的解释本身也是个归因错误。柯里化的概念早在戈特洛布·弗雷格（Gottlob Frege）所著的发表于 1879 年的 “Begriffsschrift”（《概念文字》）中就出现了。

又一个创世故事

就像我们的归纳定义中用自然数定义了自然数一样，我们的递归定义也用加法定义了加法。

同理，无需利用循环性，我们的加法定义也是可以被赋予意义的。 为了办到这一点，我们将加法的定义规约到等价的用于判断相等性的推理规则。 

n : ℕ
--------------
zero + n  =  n

m + n  =  p
---------------------
(suc m) + n  =  suc p

这里我们假设我们已经定义了指定判断 n : ℕ 的意义的自然数的无限集合。 第一条推理规则是起始步骤。它断言如果 n 是一个自然数，那么零加上它得 n。 第二条推理规则是归纳步骤。它断言如果 m 加上 n 得 p，那么 suc m 加上 n 得 suc p。

我们又一次借助于创世故事来理解，只是这次我们关注的是关于加法的判断。 

-- 起初，我们对加法一无所知。

现在，对我们已知的所有判断应用之前的规则。起始步骤告诉我们对于每个自然数 n 都有 zero + n = n，所以我们添加所有的这类等式。 归纳步骤告诉我们如果（在昨天）有 m + n = p，那么（在今天） 有 suc m + n = suc p。我们在今天之前不知道任何关于加法的等式， 所以这条规则不会给我们任何新的等式。 

-- 第一天，我们知道了 0 为被加数的加法。
0 + 0 = 0     0 + 1 = 1    0 + 2 = 2     ...

然后我们重复这个过程。在今天我们知道来自前一天的所有等式，以及任何通过规则添加的等式。起始步骤没有告诉我们任何新东西，但是归纳步骤添加了更多的等式。 

-- 第二天，我们知道了 0，1 为被加数的加法。
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...

我们再次重复这个过程： 

-- 第三天，我们知道了 0，1，2 为被加数的加法。
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...
2 + 0 = 2     2 + 1 = 3     2 + 2 = 4     2 + 3 = 5     ...

此时规律已经很明显了： 

-- 第四天，我们知道了 0，1，2，3 为被加数的加法。
0 + 0 = 0     0 + 1 = 1     0 + 2 = 2     0 + 3 = 3     ...
1 + 0 = 1     1 + 1 = 2     1 + 2 = 3     1 + 3 = 4     ...
2 + 0 = 2     2 + 1 = 3     2 + 2 = 4     2 + 3 = 5     ...
3 + 0 = 3     3 + 1 = 4     3 + 2 = 5     3 + 3 = 6     ...

这个过程可以继续下去。在第 m 天我们将知道所有被加数小于 m 的等式。

正如我们所见，解释了归纳和递归定义的正确性的推导是很相似的。它们就像一枚硬币的两面。

有限的创世故事

上述的创世故事是用分层的方式讲述的。首先，我们创造了自然数的无限集合。 然后，我们构造加法的实例时把自然数集视为现成的，所以即使在第一天我们也有一个实例的无限集合。

然而，我们也可以选择同时构造自然数集和加法的实例。这样在任何一天都只会有一个实例的有限集合。 

-- 起初，我们一无所知。

现在，对我们已知的所有判断应用之前的规则。只有自然数的起始步骤适用： 

-- 第一天，我们知道了零。
0 : ℕ

我们再次应用所有的规则。这次我们有了一个新自然数，和加法的第一个等式。 

-- 第二天，我们知道了一和所有和为零的加法算式。
0 : ℕ
1 : ℕ    0 + 0 = 0

然后我们重复这个过程。我们通过加法的起始步骤得到了一个等式，也通过在前一天的等式上应用加法的归纳步骤得到了一个等式： 

-- 第三天，我们知道了二和所有和为一的加法算式。
0 : ℕ
1 : ℕ    0 + 0 = 0
2 : ℕ    0 + 1 = 1   1 + 0 = 1

此时规律已经很明显了： 

-- 第四天，我们知道了三和所有和为二的加法算式。
0 : ℕ
1 : ℕ    0 + 0 = 0
2 : ℕ    0 + 1 = 1   1 + 0 = 1
3 : ℕ    0 + 2 = 2   1 + 1 = 2    2 + 0 = 2

在第 n 天会有 n 个不同的自然数和 n × (n-1) / 2 个加法等式。 数字 n 和所有和小于 n 的加法等式在第 n+1 天首次出现。这提供了一个对数据和关联数据的等式的无限集合的有限主义视角。

交互式定义书写

Agda 被设计为使用 Emacs 作为文本编辑器，而这两者一起提供了很多能帮助用户交互式地创建定义和证明的功能。

我们从输入以下代码开始： 

_+_ : ℕ → ℕ → ℕ
m + n = ?

问号意味着你希望 Agda 帮助你填入这部分代码。如果按组合键 C-c C-l （按住 Control 键的同时先按 c 键再按 l 键），这个问号会被替换： 

_+_ : ℕ → ℕ → ℕ
m + n = { }0

这对花括号被称作一个洞，0 是这个洞的编号。洞将会被高亮显示为绿色（或蓝色）。Emacs 会同时创建一个窗口显示如下文字： 

?0 : ℕ

这表示 0 号洞需要填入一个类型为 ℕ 的项。按组合键 C-c C-f 会移动到下一个洞。

我们希望在第一个参数递归来定义加法。 将光标移至 0 号洞并按 C-c C-c，你将看见如下提示： 

pattern variables to case (empty for split on result):

即“用于分项的模式变量（留空以对结果分项）：”。 键入 m 会触发对名为 m 的变量的分项操作（即自动模式匹配），产生如下的代码更新： 

_+_ : ℕ → ℕ → ℕ
zero + n = { }0
suc m + n = { }1

现在有两个洞了。底部的窗口会告诉你每个洞所需的类型： 

?0 : ℕ
?1 : ℕ

移动至 0 号洞并按 C-c C-, 将会显示当前洞所需类型的具体信息，以及可用的自由变量： 

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ

这些信息强烈地提示了可以用 n 填入该洞。填入内容后，你可以按 C-c C-空格 来移除这个洞。 

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = { }1

同理，移动到 1 号洞并按 C-c C-, 将会显示当前洞所需类型的具体信息，以及可用的自由变量： 

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ

移动到一个洞并按 C-c C-r 会将一个构造器填入这个洞（如果有唯一的选择的话）， 或者告诉你有哪些可用的构造器以供选择。在我们目前的情况下，编辑器将显示如下内容： 

Don't know which constructor to introduce of zero or suc

即“不知道在 zero 和 suc 中该引入哪一个构造器”。我们将 suc ? 填入并按 C-c C-空格 产生如下的代码更新： 

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc { }1

移动到新的洞并按 C-c C-, 给出了和之前类似的信息： 

Goal: ℕ
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ

我们可以用 m + n 填入该洞并按 C-c C-空格 来完成程序： 

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

在如此简单的程序如此大量地使用交互操作可能帮助不大，但是同样的技巧能够帮助你构建更复杂的程序。 甚至对于加法定义这么简单的程序，使用 C-c C-c 来分项仍然是有用的。

更多编译程序指令

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

以上几行告诉 Agda 这几个操作符和数学中常规的运算符相对应， 并令其在计算时使用对应的处理任意精度整数类型的 Haskell 操作符。 计算 m 加 n 时，用 zero 和 suc 表示的自然数需要正比于 m 的时间， 而用 Haskell 整数表示的情况下只需要正比于 m 和 n 中较大者的对数的时间。 类似地，计算 m 乘 n 时，用 zero 和 suc 表示的自然数需要正比于 m 乘 n 的时间，而用 Haskell 整数表示的情况下只需要正比于 m 和 n 的对数之和的时间。

练习 Bin（拓展）

使用二进制系统能提供比一进制系统更高效的自然数表示。我们可以用一个比特串来表示一个数： 

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

比如，如下的比特串 

1011

代表数字十一被从右至左编码为了 

x1 x1 x0 x1 nil

由于前导零的存在，表示并不是唯一的。因此，十一同样可以表示成 001011，编码为： 

x1 x1 x0 x1 x0 x0 nil

定义这样一个函数 

inc : Bin → Bin

将一个比特串转换成下一个数的比特串。比如，1100 编码了十二，我们就应该有： 

inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil

实现这个函数并确定对于编码了零到四的比特串它都能给出正确结果。

使用以上的定义，再定义一对函数用于在两种表示间转换。 

to   : ℕ → Bin
from : Bin → ℕ

对于前者，用没有前导零的比特串来表示正数，并用 x0 nil 表示零。 确定这两个函数都能对零到四给出正确结果。 

-- 在此处书写你的代码

标准库

在每一章的结尾，我们将展示如何在标准库中找到相关的定义。 自然数，它们的构造器，以及用于自然数的基本操作符，都在标准库模块 Data.Nat 中定义： 

-- import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

正常情况下，我们会以可运行代码的形式展示一个导入语句， 这样如果我们尝试导入一个不可用的定义 Agda 就会报错。 但是这一次，我们只在注释里展示了这个导入语句。这一章和标准库都调用了 NATURAL 编译程序指令。我们是在 ℕ 上使用，而标准库是在等价的类型 Data.Nat.ℕ 上使用。这样的编译程序指令只能被调用一次，因为重复调用会导致类似于 2 到底是类型 ℕ 的值还是类型 Data.Nat.ℕ 的值这样的困惑。重复调用其它的编译程序指令也会导致同样的问题。基于这个原因， 我们在后续章节中通常会避免使用编译程序指令。更多关于编译程序指令的信息可以在 Agda 文档中找到。

Unicode

这一章使用了如下的 Unicode 符号： 

ℕ  U+2115  双线体大写 N (\bN)
→  U+2192  右箭头 (\to, \r, \->)
∸  U+2238  点减 (\.-)
≡  U+2261  等同于 (\==)
⟨  U+27E8  数学左尖括号 (\<)
⟩  U+27E9  数学右尖括号 (\>)
∎  U+220E  证毕 (\qed)

以上的每一行由 Unicode 符号（如 ℕ），对应的 Unicode 码点（如 U+2115）， 符号的名称（如 双线体大写 N），以及用于在 Emacs 中键入该符号的按键序列（如 \bN）。

通过 \r 命令可以访问多种右箭头符号。在输入 \r 后，使用者可以按左、右、上、下键来查看/选择可用的箭头符号。这个命令会记住你上一次选择的位置， 并在下一次使用时从该字符开始。 用于输入左箭头的 \l 命令的工作方式与此类似。

作为在输入箭头的命令中左、右、上、下键的替代，如下的控制字符也是可用的： 

C-b  左（后退一个字符）
C-f  右（前进一个字符）
C-p  上（到上一行）
C-n  下（到下一行）

C-b 表示按 Control + b，其余同理。使用者也可以直接输入显示的列表中的数字编号来选择。