一个如何实现Coq? [英] How does one implement Coq?
问题描述
如果希望重新实现归纳构造的演算，那么实现这一目标的最短"途径是什么?尤其是，内核内部实际上会发生什么?
If one wishes to re-implement the calculus of inductive constructions, what is the "shortest" path towards this? In particular, what actually goes on inside the kernel?
我的心理模型说我们需要两件事:
My mental model says that we need two things:
- 计算/将项简化为值的能力.
- 进行类型检查以确保证明正确的能力.
但是，由于语言是依赖类型的，因此类型检查器很可能会取决于确定两种类型相等时的计算能力.
However, since the language is dependently typed, the type-checker will most likely depend on the ability to compute when deciding two types are equal.
那么，实际上，Coq评估程序的操作语义是什么?什么是类型检查推断规则?它们实施起来有多困难?
So, really, what is the operational semantics of the Coq evaluator? What are the type checking inference rules? And how difficult are they to implement?
我希望对这两个事实有一个稳定的标准参考，以便我可以重新实现一个小的CIC内核.
I'd like a stable, standard reference of these two facts so I can re-implement a small CIC kernel.
推荐答案
听起来有点像自我广告，但值得一看的metacoq项目 https://github.com/MetaCoq/metacoq ).以及与之相关的论文.我们指定Coq的类型理论(现在为负η，模板多态性和模块)，并为其编写声音类型检查器.
It sounds a bit like self-advertising but it might be worth a look at the metacoq project https://metacoq.github.io/metacoq/ (or the github repo directly https://github.com/MetaCoq/metacoq). Along with the papers associated with it. We specify the type theory of Coq (minus η, template polymorphism and modules for now) and write a sound type-checker for it.
因此，我同意一个关键因素是能够比较类型(以及由于依赖性而产生的术语).这依赖于评估，但通常不按值调用(因此我不同意 value 部分).例如，我们使用弱水头缩小功能进行转换.
As such I agree that one key ingredient is being able to compare types (and thus terms because of dependencies). This relies on evaluation, but generally not call by value (hence I would disagree with the value part). For instance we do conversion using weak head reduction.
CIC仍然很大，因此您可能需要寻找更简单的方法，在这种情况下，Andrej Bauer撰写的如何在一小时内实现类型理论"绝对值得一看.
CIC is still quite big, so you might want to look for something simpler, in which case "How to implement type theory in an hour" by Andrej Bauer is definitely worth a look.
这篇关于一个如何实现Coq?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
