Вопрос по «Учебной реализации зависимо типизированного лямбда-исчисления»

Question

У меня небольшая техническая проблема с этот чудесный мастер-класс.На странице 5 руководства рассказывается о правилах ввода для просто типизированных лямбда-выражений и представлено следующее суждение, выводимое с помощью правил, показанных на рисунке 3.

Я не смог доказать ни то, ни другое id ни const по той же причине.Возьмем, к примеру, id пример.

• Скажем, я просматриваю правило проверки типов CHK.Там сказано, что для того, чтобы check types Я должен сначала выполнить вывод, а затем сравнить результат с тем, что я ожидаю.
• Чтобы сделать вывод о приложении, мне нужно использовать APP правило, которое немедленно заставляет меня сделать вывод о типе левой части приложения, а именно (id :: α -> α)
• Для этого я использую ANN правило, которое заставляет меня это проверять α -> α — это тип (и я могу это доказать без проблем).Потом я получил это голым id символ и должны доказать, что это тип α -> α.
• Наконец, вот проблема.Для этого мне придется использовать var правило, которое требует типа id должно быть задано в контексте Гамма явно, но это не делается, поэтому доказательство разваливается.

Answer 1

$\mathsf{id}$ и $\mathsf{const}$ являются не переменными исчисления, а синтаксическим сахаром для $\lambda x ightarrow x$ и $\lambda x ightarrow \lambda y ightarrow x$ соответственно.Это указано в конце §2.2 и тонко передано с помощью шрифта без засечек, а не курсива (это типографское соглашение данного конкретного документа, а не общепринятое соглашение).

Так, например, суждение о типе$$ alpha ::\ast, y ::\alpha \vdash (\mathsf{id} ::\alpha ightarrow \alpha) \:й::rightarrow alpha $$это также типовое суждение$$ alpha ::\ast, y ::\alpha \vdash (\lambda x ightarrow x ::\alpha ightarrow \alpha) \:й::rightarrow alpha.$$Это разные обозначения одного и того же математического объекта.