表示归纳类型

Question

表示归纳类型

coqagdadependent-typeidris

3

我按照这篇文章的思路实现了依赖类型的λ演算：http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf该演算法可用，我还尝试了一些扩展：多个宇宙，硬编码归纳公理。然而，我想添加归纳类型以做更复杂的事情。

我正在考虑两种方式：

引入Fin-N、Product和W类型，并用它们表示归纳类型。
生成归纳和递归公理。

我不喜欢任何一种方式。第一种方法太低级，需要大量努力将高级语言转换为核心语言。第二种方法相当费力，容易出错，因为对于复杂的归纳类型生成递归原则有许多特殊情况，即正/负出现。

那怎么做呢？Coq、Agda和Idris等现有系统如何实现类型？

- Konstantin Solomatov

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Vinz · Accepted Answer

抱歉，我不了解Idris。

对于Agda，我建议作为起点阅读Ulf Norell博士论文，但该系统已经发展了。

Coq在您的列表中引入了第三个要点：自动生成谓词。每个归纳类型都带有3个（在某些特殊情况下为1个）归纳方案，这些方案会自动为用户定义，并命名为your_type_rect，your_type_rec和your_type_ind（只有在特殊情况下才是后者）。这些实际上是语言的术语，由系统自动生成并供用户使用，而不是公理，可以被induction策略使用（最后一个我不确定）。

实际上，您可以关闭此自动生成功能，并自己编写归纳方案。

有关induction的一些文档可以在此处找到here。我建议您在Coq邮件列表上提出问题，开发人员可能会更深入地了解Coq的内部情况。

最好， V。