Собственность Черча-Россера для лямбда-исчисления с зависимой типизацией?

13

Хорошо известно, что свойство Чёрча-Россера верно для редуцирования в простом типе лямбда-исчисления. Это означает , что исчисление соответствует, в том смысле , что не все уравнения с участием Х -терминов являются выводимыми: например, K I , так как они не разделяют ту же нормальную форму.βηλ

Также известно, что можно распространить результат на пары, которые соответствуют типам продуктов.

Но мне интересно, можно ли еще расширить результат для зависимо типизированного лямбда-исчисления (возможно) с полиморфными типами, например, исчислением конструкций?

Любые ссылки также будут великолепны!

Благодарность

StudentType
источник

Ответы:

8

Может быть полезно быстро привести контрпример к CR в типизированных исчислениях с и η :βη

t=λx:A.(λy:B. y) x

tβλx:A.x
tηλy:B.y

ABα нетипизированных терминах.

ABt

Для систем с зависимой типизацией необходимо доказать слияние до сохранения типа!

Π

Πx:A.B=βηΠx:A.B  A=βηAB=βηB
для доказательства инверсии, которая требуется для доказательства сохранения / уменьшения объекта.

βη сокращения сохраняют типы без слияния, но слияние даже не распространяется на нетипизированные / плохо набранные термины!

ηηtηλx:A.t x

λ

Другой, в последнее время довольно популярный подход, описан Абелем, Нетипизированное алгоритмическое равенство для логической структуры Мартина-Лёфа с сюръективными парами .

Коди
источник
7

λ

  • PTS только с β сокращением удовлетворяют CR на типизированных условиях. Это следует непосредственно из CR о «псевдотермах» вместе с сокращением предмета.

  • Для PTS с βη-редукцией CR на множестве псевдотерм ложна. Смотрите (2).

  • В ПТС с βη редукцией CR имеет место для хорошо типизированных членов фиксированного типа . Смотрите (1).

PTS являются очень общими формализмами и включают в себя System F, Fω, LF, а также исчисление конструкций. Последние два являются типизированными. Оба документа (1, 2) довольно старые, и я думаю, что в 2015 году станет известно больше.


λ вычислениях .

2. Недерпельт Р.П. Сильная нормализация в типизированном лямбда-исчислении с лямбда-структурированными типами .

Мартин Бергер
источник