coq - 如何实现 Coq？

Question

如果希望重新实现归纳结构的微积分，那么“最短”路径是什么？特别是，内核中实际上发生了什么？

我的心智模型表明我们需要两件事:

• 能够计算/将项简化为值。
• 能够进行类型检查以确保证明是正确的。

然而，由于语言是依赖类型的，类型检查器很可能会取决于判断两种类型是否相等时的计算能力。

那么，实际上，Coq 求值器的操作语义是什么？什么是类型检查推理规则？它们实现起来有多困难？

我想要这两个事实的稳定、标准引用，以便我可以重新实现一个小型 CIC 内核。

Answer 1

这听起来有点像 self 宣传，但 metacoq 项目可能值得一看 https://metacoq.github.io/metacoq/ (或直接在 github repo https://github.com/MetaCoq/metacoq )。连同与之相关的文件。我们指定了 Coq 的类型理论(暂时不包括 η、模板多态性和模块)，并为其编写了一个可靠的类型检查器。

因此，我同意一个关键要素是能够比较 类型(以及由于依赖关系而产生的术语)。这依赖于评估，但通常不是按值调用(因此我不同意值部分)。例如，我们使用弱头减少进行转换。

CIC 仍然很大，所以您可能想寻找更简单的东西，在这种情况下，Andrej Bauer 的“如何在一小时内实现类型理论”绝对值得一看。