什么是“错误:宇宙不一致"?在Coq中意味着什么? [英] What does "Error: Universe inconsistency" mean in Coq?

问题描述

我正在通过软件基础进行工作，目前正在练习中在教堂的数字上.这是自然数的类型签名:

I am working through Software Foundations and am currently doing the exercises on Church numerals. Here is the type signature of a natural number:

Definition nat := forall X : Type, (X -> X) -> X -> X.

我已经定义了类型为nat -> nat的函数succ.我现在想定义一个类似的加法函数:

I have defined a function succ of type nat -> nat. I would now like to define an addition function like so:

Definition plus (n m : nat) : nat := n nat succ m.

但是，我收到以下错误消息:

However, I get the following error message:

Error: Universe inconsistency.

此错误消息的实际含义是什么?

What does this error message actually mean?

推荐答案

在Coq中，所有内容都有一个类型. Type也不例外:如果您使用Check命令询问Coq，它将告诉您其类型是... Type！

In Coq, everything has a type. Type is no exception: if you ask Coq with the Check command, it will tell you that its type is... Type!

实际上，这有点说谎.如果您通过发出指令Set Printing Universes.要求更多详细信息，Coq会告诉您Type与第一个不同，而是一个更大"的.正式地，每个Type都有一个与其关联的索引，称为其Universe级别.通常在打印表达式时，该索引不可见.因此，对于任何索引j > i，该问题的正确答案是Type_i具有类型Type_j.这是确保Coq理论一致性的必要条件:如果只有一个Type，则有可能显示矛盾，类似于假设集合中有所有集合的情况下，集合理论中的矛盾.

Actually, this is a bit of a lie. If you ask for more details by issuing the directive Set Printing Universes., Coq will tell you that that Type is not the same as the first one, but a "bigger" one. Formally, every Type has an index associated to it, called its universe level. This index is not visible when printing expressions usually. Thus, the correct answer for that question is that Type_i has type Type_j, for any index j > i. This is needed to ensure the consistency of Coq's theory: if there were only one Type, it would be possible to show a contradiction, similarly to how one gets a contradiction in set theory if you assume that there is a set of all sets.

为了简化使用类型索引的工作，Coq为您提供了一些灵活性:实际上，没有任何类型具有与其相关联的固定索引.取而代之的是，每次您编写Type时，Coq都会生成一个新的索引变量，并跟踪内部约束以确保可以使用满足理论要求的约束的具体值实例化它们.

To make working with type indices easier, Coq gives you some flexibility: no type has actually a fixed index associated with it. Instead, Coq generates one new index variable every time you write Type, and keeps track of internal constraints to ensure that they can be instantiated with concrete values that satisfy the restrictions required by the theory.

您看到的错误消息意味着Coq的Universe级约束求解器表示您所要求的约束系统无法找到解决方案.问题在于nat定义中的forall是在Type_i上量化的，但是Coq的逻辑强制nat本身是Type_j类型的，并带有j > i.另一方面，应用程序n nat要求j <= i，这导致索引约束集无法满足.

The error message you saw means that Coq's constraint solver for universe levels says that there can't be a solution to the constraint system you asked for. The problem is that the forall in the definition of nat is quantified over Type_i, but Coq's logic forces nat to be itself of type Type_j, with j > i. On the other hand, the application n nat requires that j <= i, resulting in a non-satisfiable set of index constraints.

这篇关于什么是“错误:宇宙不一致"?在Coq中意味着什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！