Опечатка в исчислении конструкций бумаги?

10

В классическом исчислении конструкций бумаги есть правило, которое гласит

введите описание изображения здесь (стр. 7 из pdf, стр. 101 оригинального документа)

Это правило будет означать, что любой контекст сводится к члену этого контекста. Кажется, что это не должно быть правильно, так как это повлечет за собой

1 ≅ Nat
3 ≅ Nat
1 ≅ 3

если Nat это контекст.

Я думаю, что лучшая интерпретация заключается в том, что нижняя дельта должна была быть буквой М. Особенно с учетом правил, приведенных на следующей странице.

Так это просто опечатка или какое-то тонкое логическое правило, которое я не понимаю?

lo.logic calculus-of-constructions sequent-calculus user833970
источник

Ответы:

11

Вы правы, в этой статье есть ошибка, и правило должно гласить:

Γ⊢M:ΔΓ⊢M≅M

Я полагаю, что использование слагаемых этого стиля для равенства (иногда называемого «типизированным равенством») берет свое начало уже в Martin-Löf (см. здесь, например). Это часто заменяется нетипизированным рабочим определением в современных методах обработки, где нет никакого определения формы , и преобразование определяется на необработанных терминах.Γ⊢N≅M

Несколько нелогично, доказать, что система с типизированным преобразованием эквивалентна системе без типов, очень сложно, и она была утверждена в 2010 году Силезом и Гербелином .

Коди
источник
«Современные методы лечения» здесь означают «компьютерные методы лечения, которые в основном интересуются вычислениями».
Андрей Бауэр
Справедливо. Я почти воспитал «шведские» и «французские» школы теории типов, но я не уверен, что различие действительно существует.
Коди
Нет такого различия, о чем свидетельствует тот факт, что Тьерри Кокванд живет в Швеции. Они все вычислительные.
Андрей Бауэр
@cody: Я думал, что почти все современные компьютерные методы лечения используют типовые суждения, потому что это самый удобный способ получить eta для pi / sigma. (Конечно, Кок и Агда поддерживают это.)
Нил Кришнасвами
@NeelKrishnaswami Типовое преобразование необходимо, чтобы eta имела смысл в большинстве ситуаций, но у меня сложилось впечатление, что это может сделать мета-теорию значительно более сложной. Может быть, я совершенно не прав, и на самом деле все просто. Существует также вопрос оптимизации проверки конверсии для выполнения наименьшего объема работы, включая дополнительные обязательства по проверке типов. Конечно, это был бы отличный вопрос.
Коди