如何实现 Coq？

Question

如果一个人希望重新实现归纳结构的微积分，那么实现这一目标的“最短”路径是什么？特别是，内核内部到底发生了什么？

我的思维模型表明我们需要两件事：

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

然而，由于语言是依赖类型的，类型检查器很可能依赖于在确定两种类型相等时的计算能力。

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

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

Answer 1

这听起来有点像自我广告，但也许值得一看metacoq项目https://metacoq.github.io/metacoq/（或者直接github仓库https://github.com/MetaCoq/metacoq）。以及与之相关的论文。 \n我们指定了 Coq 的类型理论（现在减去 \xce\xb7、模板多态性和模块）并为其编写了一个健全的类型检查器。

\n\n

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

\n\n

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

\n