«Минимальная» интуиционистская теория типов?

18

Я удивлен, что люди продолжают добавлять новые типы в теории типов, но никто, кажется, не упоминает минимальную теорию (или я не могу найти ее). Я думал, что математики любят минимальные вещи, не так ли?

Если я правильно понимаю, в теории типов с непредсказуемым образом достаточно Propλ-абстракции и Π-типов. Говоря достаточно, я имею в виду, что это может быть использовано в качестве интуиционистской логики. Другие типы могут быть определены следующим образом:

знак равноdееΠα:проп,α¬Aзнак равноdееAAВзнак равноdееΠС:проп,(AВС)СAВзнак равноdееΠС:проп,(AС)(ВС)СИкс:S(п(Икс))знак равноdееΠα:проп,(ΠИкс:S,пИксα)α

Мой первый вопрос, будут ли они ( λ, Π) действительно хватает? Мой второй вопрос: что нам нужно минимально, если у нас нет непредсказуемого Prop, такого как в MLTT? В MLTT Черч / Скотт / любая кодировка не работает.

Редактировать: связанный

盛安安
источник
2
Каким был бы «минимальный» тип соотв. какие свойства это будет иметь, по вашему мнению?
Рафаэль
Будучи в состоянии доказать, что Coq может доказать? Признаюсь, у меня нет ясного ответа D:
盛安安
Но я слышал, что Coq добавил универсальный полиморфизм, для которого минимальная система, которую я предложил, очевидно, не работает. А как насчет «Возможность доказать, что может доказать MLTT (в обычном смысле)»? Я думал W-типы можно моделировать? Хотя я не обернул голову вокруг этого вообще.
盛安安
Подождите, кажется, что с непредсказуемым Propнам даже не нужно равенство.
盛安安

Ответы:

12

Чтобы развить пояснения Галле, теория типов с непредсказуемым Пропором и зависимыми типами может рассматриваться как некоторая подсистема исчисления конструкций, типично близкая к теории типов Чёрча . Взаимосвязь между теорией типов Черча и КП не так проста, но была исследована, в частности, в превосходной статье Geuvers .

Однако для большинства целей системы могут рассматриваться как эквивалентные. И действительно, вы можете обойтись совсем немного, в частности, если вас не интересует классическая логика, тогда единственное, что вам действительно нужно, - это аксиома бесконечности : в CoC невозможно доказать, что у любых типов более одного элемента! Но с помощью лишь аксиомы, выражающей, что некоторый тип бесконечен, скажем, натуральный тип чисел с принципом индукции и аксиомой , вы можете довольно далеко уйти: в этой системе можно формализовать большую часть студенческой математики (вроде как сложно что-то делать без исключенной середины).01

Без непредсказуемой поддержки вам нужно немного больше работы. Как отмечено в комментариях, экстенсиональная система (система с функциональной экстенсиональностью в отношении равенства) может обойтись только с помощью и -types, , пустых и единичных типов и , и W-типы. В интенсивных условиях это невозможно: вам нужно гораздо больше индуктивов. Обратите внимание, что для создания полезных W-типов вы должны иметь возможность создавать типы путем исключения из например так:ΣΠВооLВооL

яе б TчасеN  еLsе 

Для выполнения метаматематики вам, вероятно, понадобится хотя бы одна вселенная (скажем, для построения модели арифметики Хейтинга).

Все это выглядит много, и заманчиво искать более простую систему, которая не обладает безумной непредсказуемостью CoC, но все же относительно легко записать в нескольких правилах. Одна из последних попыток сделать это - система , описанная Altenkirch et al . Это не совсем удовлетворительно, поскольку проверка положительности, необходимая для согласованности, не является частью системы «как есть». Мета-теория еще должна быть проработана.ΠΣ

Полезный обзор - статья. Является ли ZF взломом? Freek Wiedijk, который фактически сравнивает жесткие числа во всех этих системах (количество правил и аксиом).

Коди
источник
Σ
На самом деле нет, я считаю, что вы должны принять это тоже. Моя ошибка.
Коди
11

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

С точки зрения минимальности системы, один из путей, упомянутых в комментариях, заключается в использовании контейнеров и (W / M) -типов, однако они довольно экстенсиональны, поэтому с такими системами, как Coq или Agda, работать не очень удобно.

ΠΣμν

μν

Gallais
источник