什么是归纳谓词？

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。

它们用于归纳定义属性（废话）。背后的理论可能可以在归纳结构的文献中找到。例如，搜索有关 CIC（归纳构造微积分）的论文。

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

我不知道“Coq 中默认为 true”是什么意思。

even正如您所定义的，它是一种归纳数据类型。正如类型所示，它还不是一个命题nat -> Prop。一个命题是even 0或even 1。它可以像 中那样有人居住（可证明）even 0，也可以像 中那样不有人居住even 1。