MLTT эффективно pCiC без поддержки?

11

Является ли теория типов Мартина-Лёфа в основном предикативным исчислением индуктивных конструкций без предиктивного ?Prop

Если они тесно связаны , но с большим количеством различий , чем просто , каковы эти различия?Prop

type-theory calculus-of-constructions пользователь
источник
В моей книге MLTT - это (старая и устоявшаяся) интуиционистская теория зависимых типов, а я связываю исчисление конструкций с помощником по доказательству Coq. Но я могу ошибаться.
Томас Климпел
1
MLTT использует типы идентичности, чтобы иметь дело с равенством. Каким будет равенство в предикативном фрагменте CiC?
Мартин Бергер
2
@MartinBerger: CiC также имеет типы идентификации!
Коди
1
Это немного похоже на вопрос, является ли Великобритания ЕС без других 27 государств-членов :-)
Андрей Бауэр
3
@AndrejBauer Если бы я был достаточно остроумен, я бы придумал шутку с брекситом, но, к сожалению, нет. :-P
пользователь

Ответы:

17

Короткий ответ - да, MLTT может быть разумно приравнен к CIC без каких-либо последствий Prop.

Основная техническая проблема заключается в том, что существуют десятки вариантов, когда кто-то говорит о теории типов Мартина-Лёфа, и, что более удивительно, когда кто-то говорит о CIC. Например, принимая версию CIC определяется в диссертации Бенджамина Вернера, он даже не имеет смысла , чтобы удалить Prop, так как один не имеет ни Setили вселенные Type.

Основные варианты, которые можно рассмотреть в любой из этих теорий:

  1. Юниверсы : сколько и как они определены (Palmgren, « О юниверсах в теории типов» , обсуждается множество неэквивалентных вариаций), а также допускается ли универсальный полиморфизм .

  2. Какие индуктивные типы / семейства : Agda допускает индуктивно-рекурсивные типы, но существует гораздо больше мирских вариаций в зависимости от того, насколько «велики» типы в конструкторах и элиминаторах, разрешены, обрабатываются параметры по сравнению с индексами и т. Д.

  3. Инъективность конструкторов типов . Это приводит к системе, несовместимой с EM в Агде. Конечно, у Эпиграммы есть более экстремальная «теория типов наблюдений», но это может рассматриваться как нечто совершенно иное.

  4. Аксиома К : это бесплатно для определенных версий сопоставления с образцом.

  5. Γ⊢t:IdType A BΓ⊢A = B

  6. Наличие коиндуктивных типов и связанных с ними принципов исключения.

Все вышеперечисленные варианты (кроме OTT) были рассмотрены в литературе и связаны с именем «Теория типов Мартина-Лёфа» или «Исчисление индуктивных конструкций», в основном из-за их связи с системами Agda и Coq соответственно.

Поэтому длинный ответ заключается в том, что нет единого мнения о том, каково точное определение любой из этих систем.

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