为什么我的定义不允许，因为严格的积极性？

我有以下两个定义，它们导致两个不同的错误消息。 第一个定义由于严格的正性而被否定，第二个定义由于宇宙的不一致而被否定。

(* non-strictly positive *)
Inductive SwitchNSP (A : Type) : Type :=
| switchNSP : SwitchNSP bool -> SwitchNSP A.


Fail Inductive UseSwitchNSP :=
| useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP.


(* universe inconsistency *)
Inductive SwitchNSPI : Type -> Type :=
| switchNSPI : forall A, SwitchNSPI bool -> SwitchNSPI A.


Fail Inductive UseSwitchNSPI :=
| useSwitchNSPI : SwitchNSPI UseSwitchNSPI -> UseSwitchNSPI.

在 Gitter 上聊天显示，宇宙(in)一致性首先被检查，也就是说，第一个定义符合这个检查，但是由于严格的积极性问题而失败。

就我对严格正性限制的理解而言，如果 Coq 允许非严格正性数据类型定义，我就可以不使用 fix构造非终止函数(这非常糟糕)。

为了使其更加混乱，第一个定义在 Agda 被接受，而第二个定义给出了严格的正误差。

data Bool : Set where
True : Bool
False : Bool


data SwitchNSP (A : Set) : Set where
switchNSP : SwitchNSP Bool -> SwitchNSP A


data UseSwitchNSP : Set where
useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP


data SwitchNSPI : Set -> Set where
switchNSPI : forall A -> SwitchNSPI Bool -> SwitchNSPI A


data UseSwitchNSPI : Set where
useSwitchNSP : SwitchNSPI UseSwitchNSPI -> UseSwitchNSPI

现在我的问题有两个方面: 第一，我可以用上述定义来构建什么样的“恶例”？第二，规则中哪一个适用于上述定义？

一些注意事项:

  • 为了澄清，我认为我确实理解为什么第二个定义在类型检查方面是不允许的，但是仍然觉得在允许定义的情况下，这里没有发生什么“邪恶”的事情。
  • 我首先认为我的示例是 这个问题的一个实例，但是启用宇宙多态性对第二个定义没有帮助。
  • 我是否可以使用一些“技巧”来调整我的定义，使它被 Coq 所接受？
1481 次浏览
小开
最佳答案

不幸的是，这个例子没有什么特别深刻的内容。正如你所提到的，Agda 接受它，而 Coq 的问题在于参数缺乏一致性。例如，它接受这一点:

Inductive SwitchNSPA (A : Type) : Type :=
| switchNSPA : SwitchNSPA A -> SwitchNSPA A.


Inductive UseSwitchNSPA :=
| useSwitchNSPA : SwitchNSPA UseSwitchNSPA -> UseSwitchNSPA.

像 Coq 使用的积极性标准是不完整的，所以它们会拒绝无害的类型; 支持更多类型的问题是，它通常会使积极性检查器更复杂，而这已经是内核中最复杂的部分之一。

至于它为什么拒绝它的具体细节，嗯，我不是100% 肯定。按照说明书的规定，我 好好想想应该接受吗？

编辑 : 手册是 正在更新。

具体来说，使用以下较短的名称来简化以下内容:

Inductive Inner (A : Type) : Type := inner : Inner bool -> Inner A.
Inductive Outer := outer : Inner Outer -> Outer.

  1. 正确规则 image

  2. 阳性反应
    image 给你,

    X = Outer
T = forall x: Inner X, X

    所以我们在第二个案子里

    U = Inner X
V = X
    1. V很简单，所以让我们先做这个: V = (X)在第一种情况下下降，没有 t_i，因此对 X 是正的
    2. 对于 U: U = Inner X是 绝对肯定还是 X？ image 给你, 
      T = Inner X
      因此，我们在最后一种情况下: T转换为 (I a1)(没有 t_i) 
      I = Inner
a1 = X
      而 X不会出现在 t_i中，因为没有 t_i。 构造函数的实例化类型是否满足嵌套正性条件？ 只有一个构造函数:
      2. 这个满足 嵌套阳性条件嵌套阳性条件吗？ 给你, 
        T = forall x: Inner bool, Inner X.
        所以我们在第二个案子里 
        U = Inner bool
V = Inner X
        1. X在 U中不发生，所以 X在 U中严格为正。
        2. V是否满足 X的嵌套阳性条件？ 给你, 
          T = Inner X
          因此，我们在第一种情况下: T转换为 (I b1)(没有 u_i) 
          I = Inner
b1 = X
          没有 u_i，所以 V满足嵌套正性条件。

我打开了一个 漏洞报告。手册正在修理。

还有两件小事:

  1. 我忍不住指出你的类型是空洞的:

    Theorem Inner_empty: forall A, Inner A -> False.
Proof. induction 1; assumption. Qed.

  2. 你写道:

    如果 Coq 允许非严格正数的数据类型定义，那么我可以不使用 fix 构造非终止函数(这非常糟糕)。

    这几乎是正确的，但并不完全正确: 如果 Coq 没有强制执行严格的正性，您可以构造非终止函数 句号，这是不好的。它们是否使用 fix并不重要: 逻辑中的非终止性基本上使它不合理(因此 Coq 阻止您编写不通过延迟减少终止的固定点)。


提交答案