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

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

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

$$\bot \stackrel{def}{=} \Pi \alpha: Prop. \alpha \\ \neg A \stackrel{def}{=} A \to \bot \\ A \land B \stackrel{def}{=} \Pi C: Prop. (A \to B \to C) \to C \\ A \lor B \stackrel{def}{=} \Pi C: Prop. (A \to C) \to (B \to C) \to C \\ \exists_{x: S}(P(x)) \stackrel{def}{=} \Pi \alpha: Prop. (\Pi x: S. P x \to \alpha) \to \alpha \\ $$

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

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

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

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

Без непредсказуемой поддержки вам нужно немного больше работы. Как отмечено в комментариях, экстенсиональная система (система с функциональной экстенсиональностью в отношении равенства) может обойтись только с помощью и -types, , пустых и единичных типов и , и W-типы. В интенсивных условиях это невозможно: вам нужно гораздо больше индуктивов. Обратите внимание, что для создания полезных W-типов вы должны иметь возможность создавать типы путем исключения из например так:$\Sigma$$\Pi$$\mathrm{Bool}$$\bot$$\top$$\mathrm{Bool}$

$$\mathrm{if}\ b\ \mathrm{then}\ \top\ \mathrm{else}\ \bot$$

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

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

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

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

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

$\Pi$$\Sigma$$\mu$$\nu$

$\mu$$\nu$