В книге Hott, является ли большинство типов формирователей избыточными? И если так, то почему?

В главе 1 и Приложении A к книге Hott представлены несколько семейств примитивных типов (типы юниверсов, зависимые типы функций, типы зависимых пар, типы копроизведения, пустой тип, тип блока, тип натурального числа и типы идентификаторов), образующие основу для теории гомотопического типа.

Однако кажется, что с учетом типов юниверсов и зависимых типов функций вы можете создавать все эти другие «примитивные» типы. Например, тип Empty может быть определен как

ΠT:U.T

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

Многие из этих типов явно делаются избыточными с помощью типов Inductive / W, которые представлены в главах 5 и 6. Но типы Inductive / W, по-видимому, являются необязательной частью теории, поскольку существуют открытые вопросы о том, как они взаимодействуют с HoTT (в минимум на момент выхода книги).

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

Был ли сделан этот выбор

по некоторым метатеоретическим причинам, о которых я не знаю?
по историческим причинам, чтобы теория типов выглядела как теории типов прошлого (которые не обязательно были основополагающими)?
для «юзабилити» компьютерных интерфейсов?
для некоторого преимущества в поиске доказательства, о котором я не знаю?

Аналогично: минимальная спецификация теории типов Мартина-Лёфа , /cs/82810/reduc-products-in-hott-to-church-scott-encodings/82891#82891

type-theory dependent-type homotopy-type-theory user833970
источник

Они избыточны, но не так, как вы предлагаете. Вы должны спросить себя, для чего служит «минимальность фундамента»? И мы заботимся о цели?

Андрей Бауэр

Я предполагаю, что техническая работа минимальна по соглашению, где вещи не должны быть минимальными, если это явно удобно или явно отмечено иначе. Книга даже придерживается этого в других местах, например, когда она определяет типы усечения (определенные правилами, но явно не минимальные). Например, если бы я увидел натс, определенный в терминах 0,1,10, преемника и операции мощности, я был бы сбит с толку, но я мог бы по крайней мере понять, почему это удобно для обозначения. Хотт - намного более сложная область изучения, и я хочу знать, упускаю ли я что-нибудь очевидное.

user833970

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

user833970

@AndrejBauer Я бы хотел знать, почему они тоже вредны. Мое рассуждение о том, что основополагающий язык должен быть минимальным, - это причина бритвы occam, это неоправданная дополнительная сложность. Зачем останавливаться на достигнутом? Почему бы не добавить также списки, строки, пары, тройки, векторы? Это кажется произвольным выбором, что их оправдывает? Редактировать: я только что заметил, что на этот вопрос есть ответы; но я оставлю этот комментарий здесь только для того, чтобы отметить, почему меня это тоже заинтересует.

MaiaVictor

Я напишу в блоге.

Андрей Бауэр

Ответы:

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

Когда люди говорят «пустой тип», они могут иметь в виду одно из двух:

Одного типа , который является пустым в отношении всех типов. Такой тип имеет правило исключения: для каждого и типа семьи , существует отображение . $E$ $n$ $A : E \to U_n$ $e_{n,A} : E \to A$
Семейство типов , по одному для каждого уровня юниверса , так что является «пустым типом ». Такой тип должен удовлетворять , очевидно, а также: для каждого типа семьи , существует отображение . $E_k$ $k$ $E_k$ $U_k$ $E_k : U_k$ $A : E_{k} \to U_k$ $e_{k,A} : E_{k} \to A$

Без каких-либо оговорок, когда люди говорят «пустой тип», они ожидают первое значение выше.

Как мы можем получить ? Первая попытка может быть что-то вроде $E$ но это как раз тот вид подметания, который создает путаницу. Мы должны записать явные уровни вселенной. Если мы напишем что-то вроде

E = Π (T : U) . T

$E = \Pi (T : U) \,.\, T$

, то мы получим последовательность типов

,одному для каждого уровня

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

находится в

но предполагается, что она находится в

E_{k} = Π (T : U_{k}) . T

$E_k = \Pi (T : U_k) \,.\, T$

E_{0}, E_{1}, E_{2}, \dots

$E_0, E_1, E_2, \ldots$

k

$k$

E_{k}

$E_k$

U_{k + 1}

$U_{k+1}$

U_{k}

$U_k$

Еще одна попытка но теперь вы должны объяснить, что такое « ». Вы можете испытать искушение сказать, что существует тип вселенских уровней, и поэтому

E = Π n . Π (T : U_{n}) . T

$E = \Pi n \,.\,\Pi (T : U_{n}) \,.\, T$

Π n

$\Pi n$

L

$L$

Вы сейчас попали в ловушку, потому что я спрошу: в какой вселенной живет

? И в какой вселенной живет

? Это не сработает.

E = Π (n : L) . Π (T : U_{n}) . T

$E = \Pi (n : L) \,.\,\Pi (T : U_{n}) \,.\, T$

E

$E$

L

$L$

$U$ $B : U \to U$ $\Pi (X : U) B(X)$ $U$ $U$ $\Pi (X : U) X$ $U$

Могут быть организованы непредсказуемые вселенные. Однако известная теорема Тьерри Коканда (если я не ошибаюсь) показывает, что наличие двух непредсказуемых вселенных, одна из которых содержится в другой, приводит к противоречию.

Мораль этой истории такова: просто аксиоматизируйте пустой тип напрямую и перестаньте кодировать вещи.

Андрей Бауэр
источник

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

MaiaVictor

@MaiaVictor: в отличие от чего?

Андрей Бауэр

Сожалею? Я просто имею в виду, что вы убедительно обосновали, почему стоит аксиоматизировать пустой тип, в частности. Но OP также спросил о других вещах: «типы юниверсов, зависимые типы функций, типы зависимых пар, типы копроизведения, пустой тип, тип модуля, тип натурального числа и типы идентификаторов» (которые, как я полагаю, также являются примитивами системы, предложенной в HoTT книга). (Я, очевидно, не прошу вас всех оправдывать, просто проявляю мой интерес.)

MaiaVictor

1 = \prod_{X : U} (X \to X)

$\mathbb{1} = \prod_{X : U} (X \to X)$

@IngoBlechschmidt интересно узнать, какие проблемы! Это выглядит хорошо для меня ...

MaiaVictor

Вы задаете несколько вопросов, которые похожи, но различны.

Почему книга HoTT не использует церковные кодировки для типов данных?

Церковные кодировки не работают в теории типов Мартина-Лёфа по двум причинам.

$n$ $k < n$

Во-вторых, даже если вы определили типы данных, такие как натуральные числа, с кодировками Церкви, чтобы делать доказательства с этими типами, вам нужны принципы индукции, чтобы доказать что-то о них. Чтобы вывести принципы индукции для церковных кодировок, вам нужно использовать аргумент, основанный на параметричности Рейнольдса, и вопрос о том, как включить принципы параметричности в теорию типов, до сих пор не решен полностью. (Современное состояние - статья Нейпса, Веццози и Devriese ICFP 2017 « Параметрические квантификаторы для теории зависимых типов» - обратите внимание, что это хорошо после того, как книга HoTT была написана!)
Далее вы спрашиваете, почему фундамент не минимален. Это на самом деле одна из отличительных социологических особенностей теоретико-типовых оснований - теоретики типов рассматривают наличие небольшого набора правил как техническое удобство, без особого фундаментального значения. Гораздо важнее иметь правильный набор правил, а не наименьший набор правил.

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

Вот почему даже теоретико-типичные представления пропозициональной классической логики неизменно дают все логические связки, даже если формально это эквивалентно логике только с NAND. Конечно, все логические связки могут быть закодированы с помощью NAND, но это кодирование затемняет структуру логики.

Нил Кришнасвами
источник

Спасибо за этот ответ! Мне нужно прочитать эту статью (и вашу), и это может иметь больше смысла. Но я думал, что иерархия юниверсов была разработана так, чтобы выглядело так, как будто вы можете делать предикативные вещи: например, (λA: U.λa: Aa) (ΠA: UA → A) будет десагарно (λA: Un + 1.λa: Аа) (П А : Un.A → А). Я действительно думаю, что это странный выбор редакции - не объяснять это, каждая книга по логике, которую я знаю, указывает на несколько более минимальных кодировок, таких как CNF, DNF, NAND и так далее. И любой, кто привык к теории множеств, ожидает «естественного» кодирования Натса, чтобы продемонстрировать теорию. Но это могут быть просто мои классические предубеждения.

user833970

это должно быть "непредсказуемым" в моем последнем комментарии

user833970

\prod (T : U_{n}) . T

$\prod (T : U_n) . T$

U_{n}

$U_n$

U_{n + 1}

$U_{n+1}$

U_{n}

$U_n$

Возможно, я неправильно понимаю что-то о вселенских иерархиях. Я думал, что нас никогда не волнует, в каком конкретном юниверсе находится тип, только то, что номера юниверсов могут быть назначены, когда мы хотим проверить доказательство. Технически, ΠT: UT - это семейство типов, индексированных по юниверсам. Также как полиморфная идентичность - это семейство типов, индексируемых по вселенным. Но разве у нас нет той же проблемы с полиморфной идентичностью? Я был бы очень признателен, если бы вы расширили последние 2 предложения, я не думаю, что понимаю.

user833970

Когда вы говорите, что у него нет правильных свойств исключения, вы имеете в виду, что после установления юниверса в высших вселенных есть типы, которые не могут быть непосредственно синтезированы термином termT: Un.T?

user833970