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
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 .
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:
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.U i 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?
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.U i j>i
Odpowiedzi:
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
źródło
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 dlaX:Ui i≤j X:Uj A:U42 A→U99 → X→YΠx:XYΠAU42U99U100A:U100A→U99U100
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ą.→ Γ⊢X: U i
źródło