Coq中的构造函数是什么？

Question

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

例如,在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中一些非常聪明的背景魔法.

Answer 1

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

说以下事情:

1. Z 是一个类型的术语 naturals

2. 何时e是类型的术语naturals,N e是类型的术语naturals.

3. 应用Z或是N唯一两种创造自然的方法.当给予任意自然时,你知道它是由一个或另一个制成的.

4. 两个术语e1和e2类型的naturals相等当且仅当它们都是Z或者如果它们分别N t1和N t2与t1等于t2.

您可以看到这些规则如何推广到任意归纳类型定义.通常,在类型的任意归纳类型定义中t:

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

(旁注:当类型定义是针对形状为Z和的构造函数时N,这些属性或多或少完全对应于Peano的自然数公理.这就是为什么命名的类型nat在Coq中预定义,使用这些形状的构造函数代表自然数字.这种类型接受特殊处理,因为操作原始形式很快就会很累,但特殊处理只是为了方便.)