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

10

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

Во многих ссылках, которые я читал, разрешаемость проверки типов указана как следствие сильной нормализации, и я верю в это в тех случаях, но мне интересно, как можно на самом деле показать это.

В частности, я застрял на следующем:

  • Тот факт, что хорошо типизированные термины сильно нормализуют, не означает, что алгоритм не будет зацикливаться вечно на входах с неправильной типизацией.
  • Так как логические отношения обычно используются для демонстрации сильной нормализации, нет удобного убывающего показателя, поскольку мы продвигаем термины проверки типов. Поэтому, даже если мои правила типов направлены на синтаксис, нет гарантии, что применение правил в конечном итоге прекратится.

Мне интересно, есть ли у кого-нибудь хорошая ссылка на доказательство разрешимости проверки типов для зависимо типизированного языка? Если это небольшое исчисление ядра, это нормально. Все, что обсуждает методы доказательства для определения разрешимости, было бы замечательно.

jmite
источник
7
Обычные алгоритмы двунаправленной проверки типов никогда не пытаются нормализовать термин (или тип), не проверив сначала, что он хорошо типизирован (или правильно сформирован). Вам не нужно беспокоиться о нормализации нетипизированных терминов.
Андрей Бауэр
7
Что касается применения правил: все правила для терминов и типов уменьшают цель, кроме преобразования типов. Таким образом, нам нужно контролировать преобразование типов, что мы делаем, используя двунаправленный подход.
Андрей Бауэр

Ответы:

9

Здесь действительно есть тонкость, хотя в случае проверки типов все работает хорошо. Я напишу эту проблему здесь, поскольку она, похоже, возникает во многих связанных потоках, и попытаюсь объяснить, почему все работает хорошо при проверке типов в «стандартной» теории зависимых типов (я буду намеренно расплывчатым, так как эти проблемы имеют тенденцию возникать независимо):

DΓt:ADΓA:ssutBΔDΔu:B

Этот приятный факт несколько трудно доказать, и он компенсируется довольно неприятным контрафактом:

Факт 2: В общем, и не являются под-производными от !DD DD

Это немного зависит от точной формулировки вашей системы типов, но большинство «операционных» систем, реализованных на практике, удовлетворяют Факту 2.

Это означает, что вы не можете «переходить к подсловам», рассуждая по индукции о деривациях, или делать вывод, что индуктивное утверждение верно в отношении типа термина, о котором вы пытаетесь что-то доказать.

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

Тем не менее , в случае вывода типа, вы можете задать алгоритм вывода типа одновременного типа и типа (тип типа) путем наведения на структуру термина, которая может включать алгоритм, ориентированный на тип, как предлагает Андрей. Для данного термина (и контекста вы либо не справляетесь, либо находите такие, что и . Вам не нужно использовать индуктивную гипотезу, чтобы найти последнее деривация, и, в частности, вы избегаете проблемы, описанной выше.tΓA,sΓt:AΓA:s

Ключевой случай (и единственный случай, который действительно требует преобразования) - это приложение:

infer(t u):
   type_t, sort_t <- infer(t)
   type_t' <- normalize(type_t)
   type_u, sort_u <- infer(u)
   type_u' <- normalize(type_u)
   if (type_t' = Pi(A, B) and type_u' = A' and alpha_equal(A, A') then
      return B, sort_t (or the appropriate sort)
   else fail

Каждый вызов нормализации был сделан на хорошо типизированных терминах, так как это инвариант inferуспеха России.


Между прочим, поскольку это реализовано, Coq не имеет разрешимой проверки типов, поскольку он нормализует тело fixоператоров перед попыткой проверки типов.

Во всяком случае, границы нормальных форм хорошо типизированных терминов настолько астрономичны, что теорема о разрешимости в этом случае в основном академическая. На практике вы запускаете алгоритм проверки типов до тех пор, пока у вас есть терпение, и пробуете другой маршрут, если он еще не закончился.

Коди
источник
Я нашел ваш ответ очень полезным, спасибо. У меня два вопроса: 1. Что означает «операционные системы»? Какая альтернатива? 2. Можете ли вы быть более точным в этом примере: что это значит (какой факт мы пытаемся доказать?) «Системы с типизированным преобразованием эквивалентны системам с нетипизированным преобразованием»? Спасибо!
Лукаш Лью
1
@ ŁukaszLew Альтернативой операционной системе (реализованной на практике, например, в программном обеспечении Coq или Agda) будет теоретическая система, которая полезна для доказательства мета-теоретических свойств, но неэффективна или неудобна для использования на практике. Доказательство эквивалентности операционной и теоретической системы часто является важной частью проектирования системы. Подробнее об этом я расскажу здесь: cstheory.stackexchange.com/a/41457/3984
cody
Я думаю, что стоит упомянуть, что Леннарт Огюсссон проще, проще! , Это минимальная реализация проверки типов в Haskell и некоторый вывод для лямбда-исчисления с зависимой типизацией. Есть код, который близко соответствует коди infer(t u):; чтобы найти его, найдите " tCheck r (App f a) =". Для более полной, но все же простой реализации вы можете проверить MortetypeWith .
Лукаш Лью
1
@ ŁukaszLew Проблема типизированного и нетипизированного преобразования - это хорошо известный открытый вопрос, который касается двух формулировок теорий типов и был решен довольно недавно: pauillac.inria.fr/~herbelin/articles/…
cody
Что это означает ? ut
jonaprieto