为什么我的定义因为严格的正性条件而被禁止？

Question

为什么我的定义因为严格的正性条件而被禁止？

80

我有以下两个定义，导致了两个不同的错误信息。第一个定义被拒绝是因为严格的正性，第二个定义是因为宇宙不一致性。

(* 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 上聊天时发现宇宙（不）一致性首先得到检查，也就是说，第一个定义遵循此检查，但因为存在严格的正性问题而失败。

据我理解，如果 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接受？

- ichistmeinname

4

关于Agda，简单来说：Agda跟踪数据类型参数的极性，但不跟踪索引参数的极性，这就是为什么第一个定义被接受而第二个定义不被接受，尽管它们显然是同构的原因。这只是类型检查器的缺陷，不是理论上合理的拒绝。 - effectfully

那么，拒绝第二个定义是错误的吗？ - ichistmeinname

UseSwitchNSPI 不会给语言增加不一致性。也就是说，如果语言是一致的，那么使用 UseSwitchNSPI 就不可能构造出一个被接受的错误证明。"错误" 这个词有点过于强烈了，不允许使用 UseSwitchNSPI 可能有技术上的原因（例如它可能与语言的某些其他特性不兼容，可能太难实现等）。 - effectfully

2

我的措辞可能不太好，但是没错，那正是我想要的。我不明白为什么定义被拒绝了，因为我无法构建任何“恶意”内容，而通常如果我遇到NSP错误，我就可以这样做。 - ichistmeinname

6

Agda中的bug已被修复（参见https://github.com/agda/agda/issues/3778）。 - gallais

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Clément · Accepted Answer

很遗憾，这个例子并没有什么特别深刻的含义。正如您所指出的，Agda可以接受它，而Coq无法接受的原因在于参数的不统一。例如，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.

Correctness rules
Positivity condition
Here,
```
X = Outer
T = forall x: Inner X, X
```
So we're in the second case with
```
U = Inner X
V = X
```
1. V is easy, so let's do that first: V = (X) falls in the first case, with no t_i, hence is positive for X
2. For U: is U = Inner X strictly positive wrt X? Here,
```
T = Inner X
```
  Hence we're in the last case: T converts to (I a1) (no t_i) with
```
I = Inner
a1 = X
```
  and X does not occur in the t_i, since there are no t_i. Do the instantiated types of the constructors satisfy the nested positivity condition? There is only one constructor:
  1. inner : Inner bool -> Inner X. Does this satisfy the nested positivity condition? Here,
```
T = forall x: Inner bool, Inner X.
```
    So we're in the second case with
```
U = Inner bool
V = Inner X
```
    1. X does not occur in U, so X is strictly positive in U.
    2. Does V satisfy the nested positivity condition for X? Here,
```
T = Inner X
```
      Hence we're in the first case: T converts to (I b1) (no u_i) with
```
I = Inner
b1 = X
```
      There are no u_i, so V satisfies the nested positivity condition.

我已经开了一个错误报告。手册正在修复中。

还有两件小事：

I can't resist pointing that your type is empty:

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

You wrote:

if Coq allows non-strictly positivity data type definitions, I could construct non-terminating functions without using fix (which is pretty bad).

That's almost correct, but not exactly: if Coq didn't enforce strict positivity, you could construct non-terminating functions period, which is bad. It doesn't matter whether they use fix or not: having non-termination in the logic basically makes it unsound (and hence Coq prevents you from writing fixpoints that do not terminate by lazy reduction).