9

我无法理解构造函数的原理及其工作原理。

例如，在 Coq 中，我们被教导这样定义自然数：

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

并且被告知这S是一个构造函数，但这究竟是什么意思？

如果我这样做：

Check (S (S (S (S O)))).

我知道它是4和类型nat。

这是如何工作的，Coq 是如何知道它(S (S (S (S O))))代表的4？

我想这个问题的答案是 Coq 中一些非常聪明的背景魔法。

4

2 回答 2

7 
Inductive naturals : Type :=
   | Z : naturals
   | N : naturals -> naturals.

说了以下几点：

  1. Z是类型的术语naturals

  2. whene是一个类型的项naturals，N e是一个类型的项naturals。

  3. 应用Z或是N创造自然的仅有的两种方法。当给定一个任意的自然时，您知道它是由一个或另一个制成的。

  4. 两个项e1和e2的类型naturals相等当且仅当它们都是Z或者它们分别是N t1并且等于。N t2t1t2

您可以看到这些规则如何推广到任意归纳类型定义。通常，在 type 的任意归纳类型定义中t：

  • 将构造函数应用于正确类型的参数会产生一个类型的术语t；
  • 任何类型的术语t都是应用与定义该类型相关联的构造函数之一的结果t；换句话说，给定一个类型的术语t，可以假设它是应用 ; 的构造函数之一的结果t。
  • t只有当它们将相同的构造函数应用于相同的参数时，两个类型项才相等。

（旁注：当类型定义用于 和 的构造函数时，这些属性或多或少完全对应于自然数的皮亚诺公理。这就是为什么在 Coq 中预先定义了一个名为的类型，并使用了这些形状的构造Z函数表示自然数。这种类型受到特殊处理，因为它很快就会很累地处理原始形式，但特殊处理只是为了方便。）Nnat

于 2011-02-23T12:18:50.910 回答
0

在类型理论中，（类型）构造函数只是一种从现有类型（http://en.wikipedia.org/wiki/Type_constructor）构造新类型的方法。

在您对 nat 的归纳定义中，S 是一个构造函数，因为（如果您查看签名）它需要一个 nat 并产生另一个 nat。

例如，一对 nat 的类型构造函数将是：

Inductive pair : Type := P: nat->nat->pair.

Check P (S (O)) (S(S(O))).
于 2011-02-23T18:18:48.100 回答