表示归纳类型答案

【问题标题】：Representing inductive types表示归纳类型
【发布时间】：2014-03-12 02:28:25
【问题描述】：

本着这篇文章的精神，我实现了依赖类型的 lambda 演算：http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf 演算，有效，我用它做了实验，并扩展了几件事：许多宇宙，硬编码的归纳公理。但是，我想添加归纳类型来做更复杂的事情。

我正在考虑两种方法

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

这两种方式我都不喜欢。第一个太低级，需要大量的努力才能从高级语言转换为核心语言。第二种方法工作量很大，而且容易出错，因为复杂归纳类型的递归原理的生成有很多极端情况，即正/负出现。

如何做到这一点？这些类型在 Coq、Agda 和 Idris 等现有系统中是如何实现的？

【问题讨论】：

标签： coq agda dependent-type idris

【解决方案1】：

抱歉，我不知道伊德里斯的情况。

对于 Agda，我建议以 Ulf Norell Phd Thesis 为起点，但系统自此演变而来。

Coq 在您的列表中引入了第三个项目符号：自动生成的谓词。每种归纳类型都有 3 个（在某些特殊情况下为 1 个）为用户自动定义的归纳方案，分别命名为 your_type_rect、your_type_rec 和 your_type_ind（在特殊情况下只有后一种）。这些是语言的实际术语，为用户自动生成，并由 induction 策略使用（我不是 100% 确定最后一个），而不是公理。

事实上你可以关闭这个自动生成并自己编写你的归纳方案。

关于induction 的一些文档可以在here 找到。我建议您在 Coq 邮件列表中提出您的问题，在那里开发人员可能会让您更深入地了解 Coq 的内部结构。

最好，五、

【讨论】：

coq的做法是第二点。归纳和递归原理实际上是公理。
如果您愿意，您实际上可以打印_rect _rec 和_ind 术语，它们是语言术语。这些方案的“正确性”涉及理解fix binder 和保护条件，但我不认为它们是公理。