predicate - 什么是归纳谓词？

Question

你如何解释归纳谓词？它们是做什么用的？他们背后的理论是什么？它们仅存在于依赖类型系统中，还是也存在于其他系统中？它们在某种程度上与 GADT 相关吗？为什么它们在 Coq 中默认为 true？

这是 Coq 的一个例子:

Inductive even : nat -> Prop :=
| even0 : even 0
| evens : forall p:nat, even p -> even (S (S P))

你会如何使用这个定义？它是数据类型还是命题？

Answer 1

我认为我们称归纳谓词对象是归纳定义并在 Prop 中排序的对象。 .

它们用于归纳地定义属性(duh)。背后的理论可能可以在归纳构造的文献中找到。例如，搜索有关 CIC(归纳构造演算)的论文。

它们与 GADT 有点相关，尽管它们可以通过依赖类型表达更多的东西。如果我没记错的话，对于 GADT，每个构造函数都位于一个特定的家族中，而依赖类型的添加允许构造函数根据它们的参数位于不同的家族中。

我不知道你所说的“在 Coq 中默认为 true”是什么意思。
even正如您定义的那样，它是一种归纳数据类型。这还不是命题，因为类型 nat -> Prop表示。一个命题是 even 0或 even 1 .它可以居住(可证明)，如 even 0 , 或者不像 even 1 .