Czytam ten dobrze znany artykuł o wszechświatach w teorii typów . Na początku spodziewałem się czegoś podobnego do Setω
Agdy, ale okazuje się, że jest to nawet coś bardziej ogólnego. Wydaje się uogólniać konstrukcję wszechświata od zwykłego typu indukcyjno-rekurencyjnego do spoiwa (podobnego do i ). Główne pytanie, które chcę zadać, to jaki jest tego zamiar?
Oto kod Idris definiujący zwykłe wszechświaty w stylu Tarskiego:
mutual
public export data U : (level : Nat) -> Type where
GroundU : Ground -> U level
BinderU : Binder -> (a : U level) -> (b : (x : T {level} a) -> U level) -> U level
UnivU : U (S level)
LiftU : U level -> U (S level)
public export T : {level : Nat} -> (code : U level) -> Type
Próbuję uogólnić na coś takiego
mutual
public export data U : (a : Type) -> (b : (x : a) -> Type) -> Type where
GroundU : Ground -> U a ???
...
Co powinno ???
być Autor artykułu powiedział właśnie, że wszechświaty powinny być zamknięte pod ustalonymi twórcami.
edycja: Myślę, że ???
jest po prostu b
...
Nat
wiele wszechświatów? Nie jest jasne, o co pytasz.Setω
, więc poszukałem artykułów na temat superwszechświatów, aby sprawdzić, czy mogę się czegoś nauczyć. Jest naprawdę niewiele artykułów na ten temat, a ten jest najważniejszy. Aby to zrozumieć, sam próbowałem to wdrożyć. Chociaż teraz nie sądzę, by zapewniło to wgląd w mój nowy pomysł, nadal chcę to zrozumieć.Odpowiedzi:
Jednym z celów stojących za zamkniętym pod nim operatorem wszechświata i superwszechświatem jest podanie teoretycznej wersji dużych kardynalnych aksjomatów znanych z teorii mnogości. Liczba nieosiągalna jest jak typ-teoretyczny wszechświata. Kolejnym interesującym rodzajem kardynała jest kardynał Mahlo . Mówiąc intuicyjnie, kardynał Mahlo to taki, który ma pod sobą „całą masę” niedostępnych kardynałów. Co by to było w kategoriach teoretycznych? To powinien być jakiś wszechświatU z dużą ilością wszechświatów. Do tego zmierza Palmgren, gdy rozważa superwszechświaty.
Istnieje również bardziej praktyczna strona posiadania wielu wszechświatów. Przydatne jest posiadanie typów indukcyjno-rekurencyjnych w teorii typów do różnych celów. Ale pozwalają nam zdefiniować nowe wszechświaty, więc pytanie brzmi: ile ? Aby poczuć, co robi Palmgren, zamiast od razu strzelać do superwszechświata, wypróbuj następującą sekwencję konstrukcji w Agda (używając rekurencji-indukcji):
Zdefiniuj jeden wszechświatU0 , zawierający (kod) N. i zamknięty pod Π i Σ . Ten rodzaj wszechświata odpowiada niedostępnemu kardynałowi .
Zdefiniuj operatoraU który przyjmuje dowolny typ ZA i definiuje wszechświat, który zawiera (kod) ZA i jest zamknięty pod Π i Σ . Ten rodzaj operatora wszechświata jest podobny do aksjomatu wszechświatów Grothendiecka . Ile wszechświatów możemy uzyskać poprzez wielokrotne stosowanieU , zaczynając od N. ?
Aby uzyskać jeszcze więcej wszechświatów, postulujemy superwszechświatV. który zawiera wiele wszechświatów, jak następuje:
Ile wszechświatów robiV. zawierać? Pamiętaj, że możemy dostać rodzinęB : N → V. takie, że B ( n ) jest n -ty wszechświat i tak dalej V. musi zawierać wszechświat Uω który zawiera je wszystkie. A to dopiero początek!
źródło
nat
zamiastnat
, użyłem go jako podstawowego typu, od którego możemy zacząć. Gdybym użyłbool
, również byś się czuł (z wyjątkiem gdybyś musiał przejść jeden wszechświat wyżej, aby dostać się do nieskończonych typów, ponieważ pierwszy wszechświat zawierałby tylko typy skończone zbudowane zbool
użycia