我正在努力通过软件基础 http://www.cis.upenn.edu/~bcpierce/sf/current/目前正在做教堂数字的练习。这是自然数的类型签名：
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.
该错误消息的实际含义是什么？
在 Coq 中，一切都有类型。Type也不例外：如果你问 CoqCheck命令，它会告诉你它的类型是...Type!
事实上，这有点谎言。如果您通过发布指令要求了解更多详细信息Set Printing Universes.，Coq 会告诉你Type与第一个不一样，而是一个“更大”的。正式来说，每Type有一个与其关联的索引，称为其宇宙级别。通常打印表达式时该索引是不可见的。因此，该问题的正确答案是Type_i有类型Type_j，对于任何索引j > i。这是为了确保 Coq 理论的一致性所必需的：如果只有一个Type，就有可能表现出矛盾，类似于如果假设存在所有集合的集合，人们如何在集合论中得到矛盾。
为了使使用类型索引更容易，Coq 为您提供了一些灵活性：实际上没有类型具有与其关联的固定索引。相反，每次您写入时，Coq 都会生成一个新的索引变量Type，并跟踪内部约束，以确保它们可以用满足理论所需限制的具体值进行实例化。
您看到的错误消息意味着 Coq 的宇宙级别约束求解器表明您要求的约束系统无法找到解决方案。问题是forall在定义中nat被量化超过Type_i，但是 Coq 的逻辑力nat成为其本身的类型Type_j, with j > i。另一方面，应用n nat要求j <= i，导致一组不可满足的索引约束。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
