Coq中的"错误:宇宙不一致"是什么意思？

Question

我正在通过软件基础工作,目前正在进行关于教会数字的练习.这是自然数的类型签名:

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

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

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

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

Error: Universe inconsistency.

这个错误信息实际意味着什么？

Answer 1

在Coq,一切都有类型.Type也不例外:如果你问Coq Check命令,它会告诉你它的类型是...... Type!

实际上,这有点谎言.如果您通过发出指令要求更多细节Set Printing Universes.,Coq会告诉您这Type与第一个不同,但是"更大".形式上,每个Type都有一个与之关联的索引,称为宇宙级别.通常在打印表达式时,此索引不可见.因此,该问题的正确答案是,对于任何索引Type_i都有类型.这需要确保Coq理论的一致性:如果只有一个,那么就有可能表现出矛盾,类似于如果假设存在一组所有集合,如何在集合论中得到矛盾.Type_jj > iType

为了更容易地使用类型索引,Coq为您提供了一些灵活性:没有类型实际上有与之关联的固定索引.相反,Coq每次编写时都会生成一个新的索引变量Type,并跟踪内部约束,以确保它们可以使用满足理论要求的限制的具体值进行实例化.

您看到的错误消息意味着Coq的Universe级别约束求解器表示无法解决您要求的约束系统.问题在于forall定义中nat的定量是Type_i,但是Coq的逻辑力nat本身就是类型Type_j,有j > i.另一方面,应用程序n nat要求j <= i,导致一组不可满足的索引约束.