什么是COQ中的集合 [英] What exactly is a Set in COQ

问题描述

我仍然对 Set 在COQ中的含义感到困惑.我什么时候使用 Set 和什么时候使用 Type ?

I'm still puzzled what the sort Set means in COQ. When do I use Set and when do I use Type?

在Hott中，将 Set 定义为一种类型，其中身份证明是唯一的. 但是我认为在Coq中它有不同的解释.

In Hott a Set is defined as a type, where identity proofs are unique. But I think in Coq it has a different interpretation.

推荐答案

Set在Coq和HoTT中的含义完全不同.

Set means rather different things in Coq and HoTT.

在Coq中，每个对象都有一个类型，包括类型本身.类型的类型通常称为 sorts ， kinds 或 universes .在Coq中，(与计算相关的)Universe是Set和Type_i，其中i的范围是自然数(0、1、2、3，...).我们包含以下内容:

In Coq, every object has a type, including types themselves. Types of types are usually referred to as sorts, kinds or universes. In Coq, the (computationally relevant) universes are Set, and Type_i, where i ranges over natural numbers (0, 1, 2, 3, ...). We have the following inclusions:

Set <= Type_0 <= Type_1 <= Type_2 <= ...

这些Universe的键入方式如下:

These universes are typed as follows:

 Set : Type_i     for any i

Type_i : Type_j  for any i < j

就像在Hott中一样，需要进行这种分层以确保逻辑上的一致性.正如Antal所指出的，Set的行为与最小的Type相似，但有一个例外:使用-impredicative-set选项调用coqtop时，可以使它成为 impredicative .具体来说，这意味着只要A为forall X : Set, A，其类型便为Set.相反，即使A的类型为Type_i，forall X : Type_i, A的类型也为Type_(i + 1).

Like in Hott, this stratification is needed to ensure logical consistency. As Antal pointed out, Set behaves mostly like the smallest Type, with one exception: it can be made impredicative when you invoke coqtop with the -impredicative-set option. Concretely, this means that forall X : Set, A is of type Set whenever A is. In contrast, forall X : Type_i, A is of type Type_(i + 1), even when A has type Type_i.

产生这种差异的原因是，由于逻辑上的悖论，只有这样的层次结构中的最低级别才是强制性的.然后，您可能想知道为什么默认情况下不将Set设置为强制性的.这是因为强制性Set与被排除的中点的公理的强形式不一致:

The reason for this difference is that, due to logical paradoxes, only the lowest level of such a hierarchy can be made impredicative. You may then wonder then why Set is not made impredicative by default. This is because an impredicative Set is inconsistent with a strong form of the axiom of the excluded middle:

forall P : Prop, {P} + {~ P}.

此公理允许您执行的工作是编写可以确定任意命题的函数.请注意，{P} + {~ P}类型位于Set中，而不位于Prop中.排除中间的通常形式forall P : Prop, P \/ ~ P不能以相同的方式使用，因为生活在Prop中的事物不能以计算相关的方式使用.

What this axiom allows you to do is to write functions that can decide arbitrary propositions. Note that the {P} + {~ P} type lives in Set, and not Prop. The usual form of the excluded middle, forall P : Prop, P \/ ~ P, cannot be used in the same way, because things that live in Prop cannot be used in a computationally relevant way.

这篇关于什么是COQ中的集合的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！