Jaka jest rola predykatywności w definicjach indukcyjnych w teorii typów?

Często chcemy zdefiniować obiekt zgodnie z pewnymi regułami wnioskowania. Zasady te oznaczają funkcję generowania F , która gdy jest monotonna, daje się przynajmniej stały punkt | j F . Bierzemy A : = μ F być „definicja indukcyjna” od A . Co więcej, monotoniczność F pozwala nam rozumować za pomocą „zasady indukcji” w celu ustalenia, kiedy zbiór zawiera A (tj. Kiedy właściwość powszechnie trzyma się A ).$A \in U$$F$$\mu F$$A := \mu F$$A$$F$$A$$A$

W Coq odpowiada pisania definicji A w jednoznaczny wstępie. Chociaż definicja ta oznacza określoną funkcję F , funkcja ta niekoniecznie jest monotoniczna. Coq stosuje zatem pewne kontrole składniowe, aby zagwarantować „prawidłowość” definicji. W pewnym przybliżeniu odrzuca występowanie A w pozycjach ujemnych w typach warunków wstępu.$\mathtt{Inductive}$$A$$F$$A$

(Jeśli moje rozumienie do tej pory jest błędne, proszę mnie poprawić!)

Po pierwsze, kilka pytań w kontekście Coq:

1) Czy kontrola składniowa w Coq służy jedynie zapewnieniu, że definicja ma charakter predykcyjny ? (Jeśli tak, to czy impredykatywność jest jedynym sposobem, w jaki definicja byłaby źle zdefiniowana?) Czy też sprawdza monotoniczność? (Odpowiednio, czy niemonotyczność może go zabić?)$A$

2) czy takie zdarzenie negatyw musi oznaczać, że definicji jest to impredicative / niemonotoniczny? A może Coq po prostu nie jest w stanie zweryfikować, czy w tym przypadku jest dobrze zdefiniowany?$A$$A$

I bardziej ogólnie:

3) Jaki jest związek między predykcyjnością definicji indukcyjnej a monotonicznością funkcji generującej tę definicję? Czy to dwie strony tej samej monety? Czy są niezwiązani? Nieformalnie, który z nich ma większe znaczenie?

Nie, w tym przypadku predykcyjność i monotoniczność nie są ściśle powiązane.

Kontrola pozytywności w Coq / Adga ma na celu upewnienie się, że z grubsza zajmujesz najmniej ustalony punkt monotonnej rzeczy.

Oto, jak myśleć o typach indukcyjnych w kategoriach operatorów kratowych i monotonicznych. Przypomnijmy, że twierdzenie Knastera-Tarskiego mówi, że na pełnej sieci każdy operator monotoniczny f : L → L ma najmniej ustalony punkt μ ( f ) . Następnie możemy myśleć o typach w teorii typów jako o formowaniu sieci pod dowartościowalnością. Oznacza to, że typ S jest poniżej T jeśli prawda S oznacza, że z T . Teraz chcielibyśmy wziąć monotoniczny operator F na typach i użyć Knaster-Tarski, aby uzyskać interpretację najmniej ustalonego punktu tego operatora$L$$f : L \to L$$\mu(f)$$S$$T$$S$$T$$F$ . $\mu(F)$

Jednak typy w teorii typów nie są tylko siatką: tworzą kategorię. Oznacza to, że biorąc pod uwagę dwa typy i T , istnieje potencjalnie wiele sposobów S jest poniżej T , z jednym sposób dla każdej próbnym e : S → T . Tak więc operator typu F musi również zrobić coś sensownego na tych dowodach. Właściwym uogólnieniem monotoniczności jest funkcjonalność . Oznacza to, że chcemy, aby F miał operator na typach, a także działał na dowody, tak że jeśli e : S → T , to F $S$$T$$S$$T$$e : S \to T$$F$$F$$e : S \to T$ .$F(e) : F(S) \to F(T)$

Funkcjonalność jest teraz zachowywana przez sumy i iloczyny (tj. Jeśli i G są endofunkorami na typach, to F + G i F × G (działając punktowo) są również funktorami na typach (zakładając, że mamy sumy i iloczyny w naszej algebrze jednak nie jest zachowywany przez przestrzeń funkcji, ponieważ wykładnik dwufunkcyjny F → G jest sprzeczny w swoim lewym argumencie. Więc kiedy piszesz definicję typu indukcyjnego, definiujesz funktor, który ma przyjąć co najmniej ustalony punkt. Aby upewnić się, że rzeczywiście jest to funktor, należy wykluczyć występowanie parametru rekurencyjnego po lewej stronie przestrzeni funkcji - stąd kontrola pozytywności.$F$$G$$F+G$$F\times G$$F \to G$

Generalnie unika się impredykatywności (w sensie Systemu F), ponieważ jest to zasada, która zmusza do wyboru między klasyczną logiką a modelami teoretycznymi. Nie możesz interpretować typów jako zbiorów w klasycznej teorii zbiorów, jeśli masz indeksowanie w stylu F. (Zobacz słynny „Polimorfizm nie jest teoretyczny” Reynoldsa.)

Kategorycznie, impredykatywność w stylu F mówi, że kategoria typów i terminów tworzy małą kompletną kategorię (to znaczy, homs i obiekty są zarówno zestawami, jak i istnieją granice wszystkich małych diagramów). Klasycznie wymusza to kategorię poety. Wielu konstruktywistów jest konstruktywnych, ponieważ chcą, aby ich twierdzenia opierały się na większej liczbie systemów niż tylko na logice klasycznej, a zatem nie chcą udowodnić niczego, co byłoby klasycznie fałszywe. Dlatego są nieufni wobec impredykatywnego polimorfizmu.

Jednak polimorfizm pozwala powiedzieć wiele warunków, które są klasycznie „duże” wewnętrznie w stosunku do teorii typów - a pozytywność jest jednym z nich! Operator typu jest funkcyjny, jeśli można wytworzyć termin polimorficzny:$F$

Widzisz, jak to odpowiada funkcjonalności? IMO, to byłaby bardzo fajna opcja w Coq, ponieważ pozwoliłaby ci na łatwiejsze programowanie ogólne. Syntaktyczna natura kontroli pozytywności stanowi dużą przeszkodę dla programowania ogólnego i chętnie wymieniłbym możliwość klasycznych aksjomatów na bardziej elastyczne programy funkcjonalne.

EDYCJA: Pytanie, które zadajesz na temat różnicy między Prop i Set, wynika z faktu, że programiści Coq chcą pozwolić ci myśleć o twierdzeniach Coq w naiwnych terminach teoretycznych, jeśli chcesz, bez zmuszania cię do tego. Technicznie dzielą Prop i Set, a następnie zabraniają zestawom zależeć od obliczeniowej zawartości Prop.

Możesz więc interpretować Prop jako wartości prawdy w ZFC, które są booleanami prawdą i fałszem. Na tym świecie wszystkie dowody twierdzeń są równe, a więc oczywiście nie powinieneś być w stanie rozgałęzić się na dowodzie zdania. Zatem zakaz zestawów w zależności od obliczeniowej zawartości dowodów Prop jest całkowicie rozsądny. Co więcej, 2-elementowa sieć boolowska jest oczywiście kompletną siecią, więc powinna wspierać indeksowanie impredykatywne, ponieważ istnieją arbitralne wartości ustalone. Ograniczenie predyktywności dla zbiorów wynika z faktu (wspomnianego powyżej), że indeksowanie w stylu F jest zdegenerowane w klasycznych modelach teorii zbiorów.

Coq ma inne modele (to logika konstruktywna!), Ale chodzi o to, że z półki nigdy nie udowodni niczego, czym mógłby się zastanawiać klasyczny matematyk.

Istnieje bardzo głęboki związek między definicjami indukcyjnymi a impredykatywnością, ale rozumiem, że w kontekście tego, o czym mówisz, (nie) predykatywność nie jest szczególnie istotna, a test ma na celu wyłącznie zagwarantowanie monotoniczności, aby teoria punktów stałych mogła być stosowane, a mianowicie, że zasada indukcji jest dobrze zdefiniowana. (Jestem gotów zostać poprawionym w tym punkcie).

Zależność pomiędzy definicjami impredicativity i indukcyjnych jest badane w tej rozmowie przez Coquand. Wraca do niektórych wyników z lat 50. autorstwa G. Takeuti, że definicje impredykatywne można sprowadzić do definicji indukcyjnych. Książka

• Teoria dowodowa impredykatywnych podsystemów analizy - monografie i podręczniki fizyki 2 W. Buchholza, K. Schutte

daje dobrą analizę tego tematu, jeśli możesz go zdobyć. Te slajdy zawierają przegląd.

Aby uzupełnić doskonałe wyjaśnienie Neila, impredykatywność ma „miękkie” poczucie: definiowanie zbiorów lub kolekcji za pomocą odniesienia do nich samych. W tym sensie:

Inductive Lam : Set :=
| Var : Nat -> Lam
| App : Lam -> Lam -> Lam
| Abs : (Lam -> Lam) -> Lam

jest definicją impredykatywną, ponieważ definiuje typ indukcyjny, Lam za pomocą przestrzeni funkcji (Lam -> Lam), która odnosi się do samej kolekcji. W tej sytuacji impredykatywność jest szkodliwa : można użyć twierdzenia Cantora, aby udowodnić Fałsz. W rzeczywistości jest to ta sama marka impredykatywności, która dyskontuje naiwną Teorię Setów jako spójny fundament matematyki. Dlatego jest zabronione w Coq. Jak wiesz, dozwolona jest inna forma impredykatywności :

Definition Unit : Prop := forall X:Prop, X -> X

Definicja Unit jako propozycji odnosi się do zbioru wszystkich propozycji, których jest członkiem. Jednak z nieco niejasnych dla mnie powodów ta impredykatywność nie jest szkodliwa, ponieważ występuje w ZFC (w formie nieograniczonego zrozumienia ), o którym nie wiadomo, że jest niekonsekwentna.

Podsumowując, negatywne występowanie typów indukcyjnych w definicjach jest formą impredykatywności, ale nie taką, o której zwykle mówi się w przypadku CoC jako ramy impredykatywnej .