“...的非严格阳性发生”

Question

我尝试定义以下类型

Inductive t : Type -> Type :=
  | I : t nat
  | F : forall A, (t nat -> t A) -> t A.

我收到以下错误：

Non strictly positive occurrence of "t" in "forall A : Type, (t nat -> t A) -> t A".

• 这个错误是什么意思？
• 有没有办法“修复”定义以使其有效？
• 我在哪里可以了解更多相关信息？

谢谢！

Answer 1

您可以在 Coq 参考手册中查找常见错误消息：https ://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html?highlight = positive#coq:exn.non-strictly -positive-occurrence-of-ident-in-type

本质上，如果构造函数包含函数（例如t nat -> t A），则它们不能提及被定义为参数（t nat）的一部分的归纳类型。

        vvvvvvvvvvvvvv argument
F : ... (t nat -> t A)               -> t A
                  ^ OK ("positive occurence")
         ^ Not OK ("negative occurence")

具有依赖类型的认证编程 (CPDT) 中的这一部分通过一个简化示例解释了该问题：http : //adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html#lab30

如果你可以定义类型

Inductive term : Set :=
| App : term -> term -> term
| Abs : (term -> term) -> term.

然后你可以定义函数

Definition uhoh (t : term) : term :=
  match t with
    | Abs f => f t
    | _ => t
  end.

并且uhoh (Abs uhoh)会发散。