Wszechświaty w teorii typów zależnych

11

Czytam o teorii typów zależnych w książce online The Homotopy Type Theory .

W sekcji 1.3 rozdziału Teoria typów wprowadza pojęcie hierarchii wszechświatów : , gdzie $\mathcal{U}_0 : \mathcal{U}_1 : \mathcal{U}_2 : \cdots$

każdy wszechświat jest elementem następnego wszechświata . Ponadto zakładamy, że nasze wszechświaty są kumulatywne, to znaczy, że wszystkie elementy wszechświata są również elementami wszechświata . $\mathcal{U}_i$ $\mathcal{U}_{i+1}$ $i^{\mathrm{th}}$ $(i+1)^{\mathrm{th}}$

Kiedy jednak przyjrzę się regułom formacji dla różnych typów w dodatku A, na pierwszy rzut oka, jeśli wszechświat pojawia się powyżej paska jako przesłanka, ten sam wszechświat pojawia się poniżej. Na przykład dla reguły tworzenia typów koproduktów:

\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)$

Więc moje pytanie brzmi: dlaczego konieczna jest hierarchia? W jakich okolicznościach musisz skakać ze wszechświata na wyższy w hierarchii? Naprawdę nie jest dla mnie oczywiste, jak biorąc pod uwagę jakąkolwiek kombinację , możesz otrzymać typ którego nie ma w . Bardziej szczegółowo: zasady formacji w sekcjach dodatku A.2.4, A.2.5, A.2.6, A.2.7, A.2.8, A.2.9, A.2.10, A.3.2, albo wspomnieć w przesłance i wyroku lub po prostu w wyroku. $A_m: \mathcal{U}_i$ $B$ $\mathcal{U}_i$ $\mathcal{U}_i$

Książka wskazuje również, że istnieje formalny sposób przypisywania wszechświatów:

Jeśli istnieją wątpliwości co do poprawności argumentu, sposobem na sprawdzenie tego jest próba konsekwentnego przypisywania poziomów do wszystkich pojawiających się w nim wszechświatów.

Jaki jest proces konsekwentnego przypisywania poziomów?

$\mathcal{U}:\mathcal{U}$ doprowadziłoby do paradoksu Russella . Unikanie paradoksu Russella jest wyraźnie wspomniane w książce (strona 24). Więcej informacji znajduje się na stronie 54, 55, która używa „wszechświatów w stylu Russella” zamiast „wszechświatów w stylu Tarskiego”. Dlatego na bardzo wysokim poziomie zakładam, że teoria chce uniknąć paradoksu. Niestety nie mam tła, aby bezpośrednio to zrozumieć. To, o co mi chodzi w tym pytaniu, to po prostu zarysowanie powierzchni, zdobywając kilka przykładów rzeczy w a nie w dla i może być czymkolwiek innym, co daje mi odczucie jak działają hierarchie. $\mathcal{U}_j$ $\mathcal{U}_i$ $j > i$

type-theory homotopy-type-theory dependent-types

— huynhjl
źródło

1

@huynhjl Używanie wszechświatów nie jest konieczne, aby uniknąć paradoksów, na przykład ani teoria zbiorów ZF, ani NF Quine'a, wykorzystują je dwie alternatywne podstawy matematyczne. Wszechświaty są wygodnym sposobem unikania paradoksów (a przynajmniej tak mamy nadzieję), a jednocześnie mają zdolność konstruowania bardzo ekspresyjnych typów.

— Martin Berger,

14

Pytanie, w jakich okolicznościach musimy przejść ze wszechświata na wyższy w hierarchii, jest dobre. Ważna jest hierarchia i umiejętność wspinania się. Musisz przeskakiwać poziomy, jeśli chcesz traktować wszechświat jako typ lub część typu. Na przykład, aby zdefiniować funkcje (niezależne) typu , musisz pokazać, że jest we wszechświecie. Ale to nie może być lub jakiś mniejszy wszechświat. Więc co robimy? Aby poradzić sobie z problemem (bez użycia unound ), musimy przeskoczyć wszechświat. Reguła, która pozwala nam wykonać ten skok, to -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}},$ podane w dodatku A.2.3. Istotą hierarchii wszechświatów jest to, że możemy to zrobić. Można to postrzegać jako bezpieczne przybliżenie zawierania się wszechświatów.

— Martin Berger
źródło

12

Nieznacznie zmienię odpowiedź Martina, aby wyjaśnić, gdzie pojawia się kumulatywność (reguła, która mówi, że i pociąga za sobą ). Załóżmy, że mamy i chcielibyśmy nadać typ . Reguła formowania dla jest następująca: (Jeśli jest skrótem dla to powyższą regułę można wyprowadzić z reguły formacji dla $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$ , ale nie martwmy się o to.) Aby skorzystać z tej reguły, oba typy zaangażowane w tworzenie typu funkcji muszą znajdować się w tym samym wszechświecie. W naszym przypadku mamy literę w i w . Dlatego najpierw używamy kumulatywności, aby wywnioskować, że , a następnie przejść do pokazania, że ma typ .

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}$

Moglibyśmy pozbyć się kumulatywności, ale wtedy zasady stają się bardziej złożone. Na przykład utworzenie by odczytałoby lub W każdym razie teoria typów ma wiele subtelnych odmian i wydaje się, że wszystkie razem dobrze się bawią być trochę sztuką. $\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}$

— Andrej Bauer
źródło