Coq中的构造函数是什么？

我无法理解构造函数的原理以及它的工作原理。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中一些非常聪明的背景魔法。

来源

2011-02-23 Jerome

的漂亮打印'（S（S（S（SO））））''作为4'仅仅是一个方便你不应该让你分心。如果你想知道构造函数是什么，那么用构造函数'Z'（零）和'N'（下一个）定义你自己的类型'naturals'。那么没有什么魔法会发生。 – 2011-02-23 12:05:53

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

说以下几点：

Z的类型是naturals
的一个术语时e是naturals类型的一个术语，N e是naturals类型的术语。
应用Z或N是创建自然的唯一两种方式。当给予任意自然的时候，你知道它是由一个或者从另一个构成的。
两个术语e1和naturals类型的e2是如果相等且仅当它们都是Z或者如果它们是分别N t1N t2和与t1等于t2。

您可以看到这些规则如何推广到任意归纳类型定义。但是，事实证明，当类型定义适用于形状为Z和N形状的构造函数时，这些属性几乎完全对应自然数对应的Peano's axioms。这就是为什么一个名为nat的类型是在Coq中用这些形状的构造函数预定义的，用于表示自然数。这种类型接受特殊治疗是因为它操纵原始形式非常快而累，但特殊治疗只是为了方便。

来源

2011-02-23 12:18:50

在第2项中，你的意思是说N e是一个自然类型的术语吗？ – mushroom 2012-11-21 00:42:15

@mushroom是的，我做到了。 – 2013-08-02 05:53:37

-1

在类型理论中，（类型）构造函数只是一种从现有类型构造新类型的方法（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-23 18:18:48 GClaramunt

这个答案有点令人误解：'S'是一个构造函数的事实不是由它的类型决定的。例如'plus 1'不是一个构造函数（尽管它与'S'具有相同的类型，甚至eta也减少了它）。 'S'是一个构造函数，因为它是构建'nat'的“规范”方法之一。一个类型的构造函数是构建该类型对象的唯一方法是很重要的。 – Gilles 2011-03-04 22:34:24

是的，值得澄清的是我正在讨论（归纳）类型定义。即使共享相同的类型签名，普通函数也不是类型构造函数。（如果这就是你所说的） – GClaramunt 2011-03-05 03:31:34

我可能混合了这些名称，我认为它们被称为值构造函数 – GClaramunt 2011-05-31 20:06:47

Coq中的构造函数是什么？

回答

相关问题