Rozgałęzienie teorii typu impredykatywnego

Większość teorii typów, które znam, są predykcyjne, przez co mam na myśli to

Void : Prop
Void = (x : Prop) -> x

nie jest dobrze wpisany w większość dowodów twierdzeń, ponieważ ten typ pi należy do tego samego wszechświata co Propi tak nie jest Prop : Prop. To czyni je predykatywnymi i nie pozwala na stosowanie takich impredykatywnych definicji jak wyżej. Jednak okropna liczba „języków tablicowych”, takich jak System F lub CoC, jest w rzeczywistości impredycyjna. W rzeczywistości ta impredykatywność jest niezbędna do zdefiniowania większości konstrukcji nie zawartych pierwotnie w języku.

Moje pytanie brzmi: dlaczego ktoś zrezygnowałby z impredykatywności, skoro ma moc definiowania logicznych konstrukcji? Słyszałem, jak kilka osób zauważyło, że impredykcyjność spieszy „obliczenia” lub „indukcję”, ale mam problem ze znalezieniem konkretnego wyjaśnienia.

Zamienię moje komentarze w odpowiedź. Początki predykatywnej teorii typów są prawie tak stare jak sama teoria typów, ponieważ jedną z motywacji Russela było zakazanie „okrągłych” definicji, które zostały zidentyfikowane jako część źródła niespójności i paradoksów XIX wieku. Thierry Coquand daje tutaj pouczający przegląd . W tej teorii predykaty nad „poziomem” lub typem należą do rodzajów „następnego” poziomu, na którym istnieje nieskończona (policzalna) liczba poziomów.

Chociaż predykatywna hierarchia Russela była (najwyraźniej) wystarczająca do odrzucenia znanych paradoksów, okazało się, że bardzo trudno ją zastosować jako system fundamentalny. W szczególności zdefiniowanie nawet czegoś tak prostego jak system liczb rzeczywistych było niezwykle trudne, dlatego Russel postulował aksjomat, aksjomat redukcji, który postulował, że wszystkie poziomy zostały „zredukowane” do jednego. Nie trzeba dodawać, że nie był to zadowalający rozwój.

Jednak w przeciwieństwie do „szkodliwych” stwierdzeń impredykatywnych (takich jak nieograniczone rozumienie), aksjomat ten nie wydawał się wprowadzać żadnych niespójności. Kolejne sformułowania fundamentalnych teorii ( teoria typ prosty , Zermelo teorii zbiorów ) przyjmowane im hurtowych, dzięki czemu rodziny orzeczników (kwantyfikujące nad ewentualnie cały wszechświat kompletów), predykaty na tym samym poziomie.

Około 1971 r. Martin-Löf wprowadził teorię typów zależnych, w której obowiązuje zarówno ta zasada, jak i dalszy aksjomat Type : Type. Ten system okazał się niespójny z subtelnych powodów: naiwnego paradoksu Russela nie można odtworzyć (w prosty sposób), ale sprytne kodowanie pozwala jednak na znalezienie sprzeczności. Doprowadziło to do kryzysu wiary podobnego do kryzysu Russela, skutkując predykatywną teorią typów z wszechświatami, które znamy i kochamy.

Istnieje sposób na naprawienie teorii w celu umożliwienia „niewinnej” impredykatywności teorii zbioru a la Zermelo, prowadzącej do teorii typu, takich jak Rachunek Konstrukcyjny, ale szkody zostały wyrządzone, a „szwedzka szkoła” teorii typów ma tendencję do odrzucania impredykatywności.

Kilka punktów:

1. Co to ma wspólnego z matematyką intuicyjną? Odpowiedź to niewiele. Na przełomie XIX i XX wieku matematycy mieli tendencję do łączenia używania zasad okólnych / impredykatywnych z niekonstruktywnym rozumowaniem (intuicja jest taka, że ​​impredykatywne rozumowanie zdaje się zakładać wcześniej istniejący wszechświat matematyczny, podobnie jak zastosowania wykluczonego środka). Istnieją jednak doskonale intuicyjne teorie impredykatywne (jak IZF ). Ludzie zainteresowani intuicyzmem nadal z jakiegoś powodu interesują się predykatywizmem (oczywiście jestem tego winny).

2. Co można zrobić w orzecznikowych matematyki? Jak Martin wskazuje w swojej odpowiedzi, Hermann Weyl (nie mylić z Andre Weilem) uruchomił program, który próbował zbadać moc ekspresyjną systemów predykatywnych, przyjmując za punkt wyjścia, że ​​systemy predykcyjne miały ekspresyjną siłę między arytmetyką Peano a drugim porządkiem Arytmetyka , która zgodnie z większością standardów zgodziła się, że jest impredycyjna (i jest porównywalna do Systemu F po stronie teorii typów). Program został później nazwany „matematyką odwrotną”, ponieważ próbował sklasyfikować siłę znanych twierdzeń matematycznych pod względem aksjomatów wymaganych do ich udowodnienia (odwrotność zwykłego podejścia). Thestrona wikipedia daje dobry przegląd; program był dość udany, ponieważ większość XIX-wiecznej matematyki można łatwo dostosować do bardzo słabych systemów. Wciąż pozostaje otwarte pytanie, czy program ten można skalować do najnowszych wyników, powiedzmy, teorii wyższych kategorii (podejrzewa się, że odpowiedź brzmi „tak, z wielkim wysiłkiem”).

Jednym z wymiarów jest wnioskowanie typu. Na przykład wnioskowanie typu w systemie F nie jest rozstrzygalne, ale niektóre jego predykatywne fragmenty mają rozstrzygalne (częściowe) wnioskowanie o typie.

Innym wymiarem jest spójność jako logika. Czcigodni myśliciele w przeszłości czuli się trochę nieswojo, mając impredykatywne podstawy matematyki. W końcu jest to forma okrągłego rozumowania. Myślę, że H. Weyl mógł być pierwszym lub jednym z pierwszych, którzy próbowali zrekonstruować tak dużo matematyki, jak to możliwe, w predykcyjny sposób ... po prostu po bezpiecznej stronie. Dowiedzieliśmy się, że cyrkulacje impredykatywności nie są problematyczne w klasycznej matematyce w tym sensie, że nigdy nie powstały sprzeczności z „oswojonych” definicji impredykatywnych. Z czasem nauczyliśmy się im ufać. Zauważ, że to (brak paradoksu) jest empiryczneobserwacja! Jednak znaczna część rozwoju teorii dowodu, z jego dziwnymi konstrukcjami porządkowymi, ma za ostateczny cel chęć zbudowania całej matematyki „od dołu”, tj. Bez impredykatywnych definicji. Ten program nie został ukończony. W ostatnich latach zainteresowanie predykatywnymi podstawami matematyki zmieniło się z obaw o paradoksy na obliczeniową zawartość dowodów, co jest interesujące z różnych powodów. Okazuje się, że impredykatywne definicje utrudniają wyodrębnianie treści obliczeniowych. Kolejny aspekt troski o spójność wynika z tradycji Curry-Howarda. Oryginalna teoria typów Martina-Löfa była impredycyjna ... i niesłuszna. Po tym szoku zaproponował tylko systemy predykcyjne, ale w połączeniu z indukcyjnymi typami danych, aby odzyskać dużą część mocy impredykatywności.

Teorie typów mają tendencję do przewidywania, głównie ze względów społeczno-technicznych.

Po pierwsze, nieformalną koncepcję impredykatywności można sformalizować (przynajmniej) na dwa różne sposoby. Po pierwsze, mówimy, że teoria typów, taka jak System F, jest impredycyjna, ponieważ kwantyfikacja typu może obejmować wszystkie typy (w tym typ, do którego należy kwantyfikator). Możemy więc zdefiniować ogólne operatory tożsamości i składu:

Należy jednak pamiętać, że w standardowej teorii zbiorów (np. ZFC) operacji tych nie można zdefiniować jako obiektów . W teorii zbiorów nie ma czegoś takiego jak „funkcja tożsamości”, ponieważ funkcja jest relacją między zestawem domen a zestawem kodomain, a jeśli pojedyncza funkcja może być funkcją tożsamości, możesz użyć jej do skonstruowania zestawu wszystkich zestawów. (W ten sposób John Reynolds pokazał, że polimorfizm w stylu System-F nie miał modeli teoretycznych).

$X$$S$$P$$X$$P$$X$

Dlatego impredykatywność w stylu F jest niezgodna z naiwnym spojrzeniem na typy jako zestawy. Jeśli używasz teorii typów jako asystenta dowodu, miło jest móc łatwo przenieść standardową matematykę na swoje narzędzie, dlatego większość osób wdrażających takie systemy po prostu usuwa impredykatywność. W ten sposób wszystko ma zarówno odczyt teoretyczny, jak i teoretyczny, i możesz interpretować typy w najbardziej dogodny dla ciebie sposób.