Как реализовать Coq?

Question

Если кто-то хочет заново реализовать исчисление индуктивных конструкций, каков «кратчайший» путь к этому? В частности, что на самом деле происходит внутри ядра?

Моя ментальная модель говорит, что нам нужны две вещи:

• способность вычислять / сводить термины к значениям .
• возможность проверки типа, чтобы убедиться, что доказательства правильны.

Однако, поскольку язык типизирован зависимо, средство проверки типов, скорее всего, будет зависеть от способности вычислять, когда решив, что два типа равны.

Так, на самом деле, какова операционная семантика оценщика Coq? Каковы правила вывода проверки типов ? И насколько сложно их реализовать?

Я хотел бы получить стабильную стандартную справку об этих двух фактах, чтобы я мог заново реализовать небольшое ядро ​​CI C.

Answer 1

Звучит немного как самореклама, но, возможно, стоит взглянуть на проект metacoq https://metacoq.github.io/metacoq/ (или непосредственно на репозиторий github https://github.com/MetaCoq/metacoq). Вместе с документами, связанными с этим. Мы уточняем теорию типов Coq (минус η, шаблонный полиморфизм и модули на данный момент) и пишем для нее звуковую проверку типов.

Поэтому я согласен, что один ключевой ингредиент способен сравнить типов (и, следовательно, терминов из-за зависимостей). Это зависит от оценки, но обычно не вызов по значению (следовательно, я не согласен с частью value ). Например, мы выполняем преобразование, используя слабое уменьшение головы.

CI C все еще довольно большой, поэтому вы можете захотеть поискать что-то более простое, в этом случае "Как реализовать теорию типов за час" от Andrej Бауэр определенно стоит посмотреть.