agda - Agda 中通过归纳原理定义的函数

Question

在 Agda 中玩证明验证时，我意识到我对某些类型明确使用了归纳原则，而在其他情况下则使用模式匹配。
我终于在维基百科上找到了一些关于模式匹配和归纳原则的文字:“在 Agda 中，依赖类型模式匹配是该语言的一种原语，核心语言没有模式匹配转化为的归纳/递归原则。”

那么由于 Agdas 模式匹配，Agda 中的类型理论归纳和递归原则(定义类型上的函数)是完全多余的吗？像这样的东西( Path induction implied )那时只会有教学值(value)。

http://en.wikipedia.org/wiki/Agda_%28programming_language%29#Dependently_typed_pattern_matching

Answer 1

我对Agda不熟悉，但我认为在这一点上，它与Coq相似，我可以为Coq回答相应的问题。两种语言均基于 intuitionistic type theory with inductive types .

在直觉类型理论中，可以从足够通用的固定点组合器以及依赖模式匹配中推导出递归原理。模式匹配是不够的:虽然这允许破坏归纳类型，但仅模式匹配不允许在该类型上编写递归函数。以维基百科的例子为例:

add zero n = n
add (suc n) m = suc (add n m)

这个定义是良构的这一事实并不需要对 ℕ 的归纳原理。但是除了在 add的第一个参数上形成的模式匹配之外，它需要一个规则，说明第二种情况下的递归调用是良构的。

通过模式匹配和递归，归纳原则可以定义为一等对象:

nat_ind f_zero f_suc zero = f
nat_ind f_zero f_suc (suc n) = f_suc (nat_ind f_zero f_suc n)