1

我正在阅读软件基础这本书来学习Coq，但我被困在了Numbers上。在这个类型定义中

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

当我们在定义中使用它时会O变成怎样0

Definition pred (n : nat) : nat :=
  match n with
    | O => O
    | S n' => n'
  end.

我只知道O表示自然数并S取一个自然数并返回另一个自然数。我没有得到的是，当我们定义的nat数据类型在pred定义中使用时如何O表示0？而S n'pattern match给我们的前身是怎样的n。

4

1 回答 1

2

皮亚诺数

nat通过一元数字系统表示自然数。该nat类型的居民（值）是O, S O, S (S O), S (S (S O)), ..., S (S (S (S ... O)...)。

我们将符号解释O为自然数零。并S以一元表示形式表示单个“滴答”，即我们将其解释S为构造函数（它与面向对象编程无关），它接受一个自然数并产生下一个自然数。

前置函数

pred在某种意义上实际上并不是一个非常乖巧的函数。

首先，当我们谈论自然数时，没有零的前身。但是 Coq 中的所有函数都必须返回一个值，所以如果我们想保留pred（即nat -> nat）的类型，我们必须对pred O. 回来O并结束它感觉很自然。这给了我们模式数学表达式 ( O => O) 的第一个分支。

pred接下来，当我们调用代表 1 的数字时，我们返回了什么？让我们回想一下，我们在 Coq 中将 1 写为S O。这很容易——pred (S O)应该返回O。现在让我们尝试 2：pred (S (S O))应该返回S O. 你看到这里的模式了吗？S如果我们在一个' 前面有一堆' O，我们就去掉一个S——就这么简单。模式匹配表达式的第二个分支 ( S n' => n') 正是这样做的：它采用一个（非零）形式的数字S n'并将其转换为n'（当然不改变原始形式）。

让我举个例子。让我们一步一步计算数字3的前身：

pred (S (S (S O)))

展开 的定义，pred代替S (S (S O))：n

match S (S (S O)) with
| O => O
| S n' => n'
end

S (S (S O))有形式S n'（以 开头S），所以我们采用第二个分支，绑定 n'到S (S O). 我们如何检查我们没有在这里犯错？如果我们替换n'into的定义，S n'我们应该得到原来的n: S n'= S (S (S O))= n。

现在，我们只需返回n'：

S (S O)

正如预期的那样，我们得到了 2 作为结果！

符号

00、和之间有区别O。第一个零 (0) 是自然数零的元级数字（这是我们在元语言中指定零的方式，例如本例中的英语）。0是 的符号O，换句话说，0是 的语法糖O。正如 Coq 参考手册所说（§1.2.4）：

数词在微积分中没有明确的语义。它们只是可以通过符号机制绑定到对象的符号（详见第 12 章）。最初，数字被绑定到 Peano 对自然数的表示（见 3.1.3）。

很容易说明：

Check 0.                     (* 0 : nat *)
Check 5.                     (* 5 : nat *)
Unset Printing Notations.    (* Print terms as is, no syntactic sugar *)
Check 0.                     (* O : nat *)
Check 5.                     (* S (S (S (S (S O)))) : nat *)

您可以重载数字，这是一个整数示例：

Set Printing Notations.
Require Import Coq.ZArith.ZArith.
Open Scope Z.
Check 0.                            (* 0 : Z *)
Check 5.                            (* 5 : Z *) 
Unset Printing Notations.
Check 0.                            (* Z0 : Z *)
Check 5.                            (* Zpos (xI (xO xH)) : Z *)

结果：相同的符号可以绑定到不同的术语。Coq 定义了一些默认符号，例如数字等无处不在的事物。

如果你想定义你自己的类型来表示自然数 ( my_nat) 可能与O和S(like stopand tick) 的名称不同，你必须编写一个插件来将 Coq 数字映射到my_nat(see here ) 的术语上。

于 2017-05-24T07:59:14.397 回答