Я нахожусь в ситуации, когда мне нужно показать, что проверка типов решаема для исчисления с зависимым типом, над которым я работаю. До сих пор я был в состоянии доказать, что система сильно нормализуется, и, таким образом, равенство определений разрешимо.
Во многих ссылках, которые я читал, разрешаемость проверки типов указана как следствие сильной нормализации, и я верю в это в тех случаях, но мне интересно, как можно на самом деле показать это.
В частности, я застрял на следующем:
- Тот факт, что хорошо типизированные термины сильно нормализуют, не означает, что алгоритм не будет зацикливаться вечно на входах с неправильной типизацией.
- Так как логические отношения обычно используются для демонстрации сильной нормализации, нет удобного убывающего показателя, поскольку мы продвигаем термины проверки типов. Поэтому, даже если мои правила типов направлены на синтаксис, нет гарантии, что применение правил в конечном итоге прекратится.
Мне интересно, есть ли у кого-нибудь хорошая ссылка на доказательство разрешимости проверки типов для зависимо типизированного языка? Если это небольшое исчисление ядра, это нормально. Все, что обсуждает методы доказательства для определения разрешимости, было бы замечательно.
Ответы:
Здесь действительно есть тонкость, хотя в случае проверки типов все работает хорошо. Я напишу эту проблему здесь, поскольку она, похоже, возникает во многих связанных потоках, и попытаюсь объяснить, почему все работает хорошо при проверке типов в «стандартной» теории зависимых типов (я буду намеренно расплывчатым, так как эти проблемы имеют тенденцию возникать независимо):
Этот приятный факт несколько трудно доказать, и он компенсируется довольно неприятным контрафактом:
Факт 2: В общем, и не являются под-производными от !D′ D′′ DD
Это немного зависит от точной формулировки вашей системы типов, но большинство «операционных» систем, реализованных на практике, удовлетворяют Факту 2.
Это означает, что вы не можете «переходить к подсловам», рассуждая по индукции о деривациях, или делать вывод, что индуктивное утверждение верно в отношении типа термина, о котором вы пытаетесь что-то доказать.
Этот факт довольно сильно кусает вас, когда вы пытаетесь доказать кажущиеся невинными утверждения, например, что системы с типизированным преобразованием эквивалентны системам с нетипизированным преобразованием.
Тем не менее , в случае вывода типа, вы можете задать алгоритм вывода типа одновременного типа и типа (тип типа) путем наведения на структуру термина, которая может включать алгоритм, ориентированный на тип, как предлагает Андрей. Для данного термина (и контекста вы либо не справляетесь, либо находите такие, что и . Вам не нужно использовать индуктивную гипотезу, чтобы найти последнее деривация, и, в частности, вы избегаете проблемы, описанной выше.t Γ A,s Γ⊢t:A Γ⊢A:s
Ключевой случай (и единственный случай, который действительно требует преобразования) - это приложение:
Каждый вызов нормализации был сделан на хорошо типизированных терминах, так как это инвариант
infer
успеха России.Между прочим, поскольку это реализовано, Coq не имеет разрешимой проверки типов, поскольку он нормализует тело
fix
операторов перед попыткой проверки типов.Во всяком случае, границы нормальных форм хорошо типизированных терминов настолько астрономичны, что теорема о разрешимости в этом случае в основном академическая. На практике вы запускаете алгоритм проверки типов до тех пор, пока у вас есть терпение, и пробуете другой маршрут, если он еще не закончился.
источник
infer(t u):
; чтобы найти его, найдите "tCheck r (App f a) =
". Для более полной, но все же простой реализации вы можете проверить MortetypeWith
.