时间戳

首页 > 解决方案 > Coq 的类型系统 CiC 和 lambda cube 有什么关系？

coq - Coq 的类型系统 CiC 和 lambda cube 有什么关系？

问题描述

我阅读了https://en.wikipedia.org/wiki/Lambda_cube#Formal_definition并对 CiC 和 lambda 立方体之间的关系感到困惑。据我了解，CiC 扩展了作为 lambda 立方体角的 CoC，因此在 Coq 中也应该满足 lambda 立方体的规则。

例如，coq 似乎接受 (*,*)。因为类型nat -> nat是Set哪个是nat（右侧）的类型。

但似乎 Coq 不接受 (□,＊)。如果是，那么 的类型Set -> nat必须是Set，而不是Type。但 Coq 的答案Check (Set -> nat)是Type.

我是否误解了 wiki 页面上的描述？

标签： coqtype-systems

解决方案

Coq 没有单个不可类型的□，而是可类型的层次结构。（特别是，□:□ 是一种打字规则的粗略近似。）因此，由于这些“宇宙”，Coq 不太适合 lambda 立方体的设置。

至于Set -> nat是 type Set，就看是否Set是不可言喻的了。默认情况下，它是谓词，因此Set -> nat需要有一个严格大于Set自身的类型，即Type. 但是您可以更改Set为不可预测的：

$ coqtop -impredicative-set
Welcome to Coq 8.11.1 (April 2020)

Coq < Check (Set -> nat).
Set -> nat
     : Set

推荐阅读