类型`Set`的具体示例是什么？`Set`的含义是什么？

本文介绍了类型`Set`的具体示例是什么？`Set`的含义是什么？的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述

除了this great discussion in SO之外，我还在Adam Chlipala的书中遇到了Set，我一直在试图理解Set是什么。他的第一个示例使用Set定义二进制操作：

Inductive binop : Set := Plus | Times.

在那本书里他说：

Second, there is the : Set fragment, which declares that we are defining a datatype that should be thought of as a constituent of programs.

这让我很困惑。亚当在这里是什么意思？

此外，我认为其他一些具体的例子会有助于我的理解。我不是Coq方面的专家，所以我不确定哪种类型的示例会有帮助，但一些简单、非常具体/扎实的例子可能会有用。

注意，我已经看到Set是类型层次结构中的第一个&Quot；类型set"；，例如Set = Type(0) <= Type = Type(1) <= Type(2) <= ... 。我想这是有道理的，就像我假设nat in Type和所有常见的编程类型都在其中一样，但不确定Type中有什么不会在Set中。也许是递归类型？我不确定这是否是正确的例子，但我正在努力理解这个概念的含义以及它在概念上(和实践中)的用处。

推荐答案

虽然Set和Type在CoQ中有所不同，但这主要是由于历史原因。如今，大多数开发并不依赖于Set不同于Type。特别是，如果到处将Set替换为Type，那么Adam的评论也是有意义的。要点是，当您想要定义在执行期间可以用来计算的数据类型(例如数字)时，您希望将其放入Set或Type而不是Prop。这是因为当您从Coq中提取程序时，Prop中的内容将被擦除，因此Prop中定义的内容最终将不计算任何内容。

关于您的第二个问题：Set是Type中的内容，而不是Set中的内容，如以下代码片断所示。

Check Set : Type. (* This works *) Fail Check Set : Set. (* The command has indeed failed with message: *) (* The term "Set" has type "Type" while it is expected to have type *) (* "Set" (universe inconsistency: Cannot enforce Set+1 <= Set). *)

这一限制是为了防止理论中的悖论。默认情况下，这几乎是您在Set和Type之间看到的唯一区别。您还可以通过使用-impredicative-set选项调用CoQ：

来使它们更加不同 (* Needs -impredicative-set; otherwise, the first line will also fail.*) Check (forall A : Set, A -> A) : Set. Universe u. Fail Check (forall A : Type@{u}, A -> A) : Type@{u}. (* The command has indeed failed with message: *) (* The term "forall A : Type, A -> A" has type "Type@{u+1}" *) (* while it is expected to have type "Type@{u}" (universe inconsistency: Cannot enforce *) (* u < u because u = u). *)

请注意，我必须添加Universe u.声明，以强制Type的两次出现在同一级别。如果没有这个声明，Coq会默默地将这两个Type放在不同的宇宙级别，命令将被接受。(这并不意味着Type将与本例中的Set具有相同的行为，因为当u和v不同时，Type@{u}和Type@{v}是不同的东西！)

如果您想知道为什么这个特性很有用，这不是偶然的。绝大多数CoQ开发并不依赖于它。默认情况下，它被关闭，因为它与一些通常被认为在Coq开发中更有用的公理不兼容，例如排除中间的强大定律：

forall A : Prop, {A} + {~ A}

打开-impredicative-set时，此公理产生悖论，但默认情况下使用它是安全的。