Вселенные в теории зависимых типов

Я читаю о теории зависимых типов в онлайн-книге « Теория гомотопических типов» .

В разделе 1.3 главы « Теория типов» вводится понятие иерархии вселенных : , где $\mathcal{U}_0 : \mathcal{U}_1 : \mathcal{U}_2 : \cdots$

каждая вселенная является элементом следующей вселенной . Более того, мы предполагаем, что наши вселенные являются кумулятивными, то есть все элементы вселенной также являются элементами вселенной . $\mathcal{U}_i$ $\mathcal{U}_{i+1}$ $i^{\mathrm{th}}$ $(i+1)^{\mathrm{th}}$

Тем не менее, когда я смотрю на правила формирования для различных типов в приложении A, на первый взгляд, если вселенная появляется над планкой в качестве предпосылки, та же самая вселенная появляется ниже. Например, для правила формирования видов побочных продуктов:

\frac{Γ ⊢ A : U_{i} Γ ⊢ B : U i}{Γ ⊢ A + B : U_{i}} (+ - F O R M)

$\dfrac{\Gamma \vdash A : \mathcal{U}_i \quad \Gamma \vdash B : \mathcal{U}i}{\Gamma \vdash A + B : \mathcal{U}_i}(+\mbox{-}FORM)$

Итак, мой вопрос: зачем нужна иерархия? При каких обстоятельствах вам нужно прыгать со вселенной на одну высшую в иерархии? Мне действительно не очевидно, как при любой комбинации вы можете получить тип , которого нет в . Более подробно: правила формирования в разделах приложения A.2.4, A.2.5, A.2.6, A.2.7, A.2.8, A.2.9, A.2.10, A.3.2, либо упоминают в предпосылке и суждении, или только в суждении. $A_m: \mathcal{U}_i$ $B$ $\mathcal{U}_i$ $\mathcal{U}_i$

Книга также намекает на то, что существует формальный способ назначения вселенных:

Если есть какие-либо сомнения относительно правильности аргумента, способ проверить его состоит в том, чтобы попытаться последовательно назначить уровни всем появляющимся в нем юниверсам.

Каков процесс последовательного присвоения уровней?

$\mathcal{U}:\mathcal{U}$ приведет к парадоксу Рассела . Избегание парадокса Рассела явно упоминается в книге (стр. 24). Также более подробно рассматриваются страницы 54, 55, в которых используются «вселенные в стиле Рассела», а не «вселенные в стиле Тарского». Поэтому на очень высоком уровне я считаю само собой разумеющимся, что теория хочет избежать парадокса. К сожалению, у меня нет опыта, чтобы понять это напрямую. В этом вопросе я хочу узнать лишь о том, как получить некоторые примеры вещей в а не в для и может быть чем-то еще, что дает мне ощущение за то, как работают иерархии. $\mathcal{U}_j$ $\mathcal{U}_i$ $j > i$

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

@huynhjl Использование вселенных необязательно, чтобы избежать парадоксов, например, ни теория множеств ZF, ни NF Куайна, их используют две альтернативные математические основы. Вселенные - это удобный способ избежать парадоксов (или мы на это надеемся), в то же время обладая способностью создавать очень выразительные типы.

Мартин Бергер

Ответы:

Вопрос, при каких обстоятельствах нам нужно перепрыгнуть со вселенной на одну высшую в иерархии, является хорошим. Наличие иерархии и умение лазать по ней очень важно. Вам нужно перепрыгивать уровни, когда вы хотите рассматривать юниверс как тип или как часть типа. Например, чтобы определить функции (независимого) типа вы должны показать, что находится во вселенной. Но это не может быть или какая-то меньшая вселенная. Так что же нам делать? Чтобы справиться с этой проблемой (без использования непонятного ), нам нужно вскочить во вселенную. Правило, которое позволяет нам сделать этот переход, является -Intro

A \to U_{i}

$A \rightarrow \mathcal{U}_i$

A \to U_{i}

$A \rightarrow \mathcal{U}_i$

U_{i}

$\mathcal{U}_i$

U_{i} : U_{i}

$\mathcal{U}_i : \mathcal{U}_i$

U

$\mathcal{U}$

\frac{⊢ Γ : c t x}{Γ ⊢ U_{i} : U_{i + 1}},

$\frac{\vdash \Gamma : ctx}{\Gamma \vdash \mathcal{U}_i : \mathcal{U}_{i+1}},$ приведенный в Приложении A.2.3. Суть иерархии вселенных в том, что мы можем сделать это. Это можно рассматривать как безопасное приближение наличия вселенных.

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

Я немного исправлю ответ Мартина, чтобы объяснить, откуда берется совокупность (правило, которое гласит, что и влекут за собой ). Предположим, у нас есть и мы хотим присвоить тип . Правило формирования для таково: (Если является сокращением для то вышеприведенное правило может быть получено из правила формирования для $X : \mathcal{U}_i$ $i \leq j$ $X : \mathcal{U}_j$ $A : \mathcal{U}_{42}$ $A \to \mathcal{U}_{99}$ $\to$

\frac{Γ ⊢ X : U_{i} Γ ⊢ Y : U_{i}}{Γ ⊢ (X \to Y) : U_{i}}

$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \vdash Y : \mathcal{U}_i}{\Gamma \vdash (X \to Y) : \mathcal{U}_i}$

X \to Y

$X \to Y$

Π_{x : X} Y

$\Pi_{x : X} Y$

Π

$\Pi$ , но давайте не будем об этом беспокоиться.) Чтобы использовать это правило, оба типа, участвующие в формировании типа функции, должны находиться в одной и той же вселенной. В нашем случае у нас есть в и в . Таким образом, мы сначала используем совокупность, чтобы определить, что , а затем переходим к тому, чтобы показать, что имеет тип .

A

$A$

U_{42}

$\mathcal{U}_{42}$

U_{99}

$\mathcal{U}_{99}$

U_{100}

$\mathcal{U}_{100}$

A : U_{100}

$A : \mathcal{U}_{100}$

A \to U_{99}

$A \to \mathcal{U}_{99}$

U_{100}

$\mathcal{U}_{100}$

Мы могли бы избавиться от накопления, но тогда правила стали бы более сложными. Например, формирование будет читать или В любом случае теория типов имеет много тонких вариаций, и кажется, что заставить их всех играть вместе приятно быть немного искусства. $\to$

\frac{Γ ⊢ X : U_{i} Γ ⊢ Y : U_{j}}{Γ ⊢ (X \to Y) : U_{max (i, j)}}

$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \vdash Y : \mathcal{U}_j}{\Gamma \vdash (X \to Y) : \mathcal{U}_{\max(i,j)}}$

\frac{Γ ⊢ X : U_{i} Γ ⊢ Y : U_{j} i \leq k j \leq k}{Γ ⊢ (X \to Y) : U_{k}}

$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \vdash Y : \mathcal{U}_j \qquad i \leq k \qquad j \leq k}{\Gamma \vdash (X \to Y) : \mathcal{U}_k}$

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