如何实现 Coq？

Question

如果希望重新实现归纳构造的演算，那么实现这一目标的“最短”路径是什么？尤其是内核内部实际发生了什么？

我的心智模型说我们需要两件事：

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

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

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

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

Answer 1

这听起来有点像自我广告，但可能值得一看 metacoq 项目 https://metacoq.github.io/metacoq/（或直接在 github 存储库 https://github.com/MetaCoq/metacoq）。连同与之相关的论文。 我们指定了 Coq 的类型论（现在减去 η、模板多态性和模块）并为它编写了一个可靠的类型检查器。

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

CIC 还是挺大的，所以你可能想找一些更简单的，在这种情况下，Andrej Bauer 的“如何在一小时内实现类型理论”绝对值得一看。