你将如何解释归纳谓词？它们是用来做什么的？他们背后的理论是什么？它们只存在于依赖类型系统中，还是存在于其他系统中？它们在某种程度上与 GADT 相关吗？为什么它们在 Coq 中默认为 true？
这是 Coq 的一个例子：
Inductive even : nat -> Prop :=
| even0 : even 0
| evens : forall p:nat, even p -> even (S (S P))
你会如何使用这个定义？它是数据类型还是命题？
问问题
1432 次
2 回答
4
回答问题的另一部分。归纳谓词/定义不仅存在于依赖类型系统中（例如，Isabelle/HOL 也有它们）。原则上，它们要老得多，并且只描述在某些给定推理规则下封闭的最小谓词（或集合）。这是否定义明确取决于规则。存在易于检查的充分条件（例如，定义的谓词本身仅在规则前提中肯定出现）。然后 Knaster-Tarski 定理产生了预期的结果。
如果我没记错的话，Glynn Winskel 的书The Formal Semantics of Programming Languages: An Introduction介绍了数学基础。
于 2014-04-29T14:47:52.013 回答
4
我认为我们将归纳谓词对象称为归纳定义并排序在Prop.
它们用于以归纳方式定义属性（duh）。背后的理论可能可以在归纳结构的文献中找到。例如，搜索有关 CIC（归纳构造的演算）的论文。
它们在某种程度上与 GADT 相关，尽管使用依赖类型它们可以表达更多的东西。如果我没记错的话，对于 GADT，每个构造函数都生活在一个特定的家族中，而依赖类型的添加允许构造函数根据其参数居住在不同的家族中。
我不知道您所说的“Coq 默认情况下为真”是什么意思。
even正如您定义的那样，它是一种归纳数据类型。nat -> Prop正如类型所表明的那样，它还不是一个命题。一个命题是even 0or even 1。它可以像 中那样有人居住（可证明）even 0，也可以不在 中even 1。
于 2014-04-11T22:36:14.743 回答