W ostatnim wątku na liście mailingowej Agdy pojawiło się pytanie o prawa , w których Peter Hancock wypowiedział się prowokująco .
Rozumiem, że prawa mają typy negatywne, tj. łączniki, których zasady wprowadzania są odwracalne. Aby wyłączyć dla funkcji, Hank sugeruje użycie niestandardowego eliminatora, funsplit , zamiast zwykłej reguły aplikacji. Chciałbym zrozumieć uwagę Hanka pod względem biegunowości.
Na przykład istnieją dwie typy prezentacji . Istnieje tradycyjny eliminator podziału Martin-Löf , w pozytywnym stylu:
I jest wersja negatywna:
Ta ostatnia prezentacja ułatwia uzyskanie dla par, tj. dla dowolnej pary (gdzie == oznacza definicję równości). Pod względem niezawodności ta różnica nie ma znaczenia: intuicyjnie możesz realizować projekcje z podziałem lub na odwrót.
Teraz typy są zwykle (i, jak sądzę, bez kontrowersji) traktowane negatywnie:
Co daje nam dla funkcji: .
Jednak w tej wiadomości Hank przypomina eliminator funsplit (Programowanie w teorii typów ML, [http://www.cse.chalmers.se/research/group/logic/book/], s. 56). Jest to opisane w ramach logicznych przez:
Co ciekawe, Nordstrom i in. uzasadnij tę definicję stwierdzeniem, że „[ta] alternatywna niekanoniczna forma opiera się na zasadzie indukcji strukturalnej”. Jest silny zapach pozytywności do tego stwierdzenia: funkcje byłyby „zdefiniowane” przez ich konstruktora, .
Nie mogę jednak do końca dopracować zadowalającej prezentacji tej reguły w naturalnej dedukcji (a nawet, lepiej, w rachunku różniczkowym). Kluczowe wydaje się tutaj użycie (ab) logicznego frameworka do wprowadzenia .
Czy więc funsplit to pozytywna prezentacja typów ? Czy mamy również coś podobnego w (niezależnym) rachunku sekwencyjnym? Jak by to wyglądało?
Jak częste / ciekawe jest to dla teoretyków dowodów w tej dziedzinie?
źródło
Oto nieco inne spojrzenie na odpowiedź Fredrika. Generalnie jest tak, że impredykatywne kodowanie typów Kościoła spełnia odpowiednie prawa , ale nie spełnia praw η .β η
Oznacza to, że możemy zdefiniować parę zależną w następujący sposób:
teraz zauważyć, że π 1 łatwo definiowane: π 1 : ∃ x : x .
Druga projekcja jest jednak możliwa do zrealizowania , a w modelu parametrycznym można pokazać, że ma również właściwe zachowanie. (Zobacz mój ostatni szkic z Derekiem Dreyerem na temat parametryczności w rachunku konstrukcji, aby uzyskać więcej na ten temat.) Myślę więc, że projekcja zasadniczo wymaga pewnych silnych właściwości ekstensywności, aby miała sens.π2
Jeśli chodzi o rachunek sekwencyjny, słaby eliminator ma regułę, która wygląda trochę jak:
Tutaj ukryte w warunkach dobrze ukształtowania wynika, żePnie występują wolne wy'lubC. Jeśli złagodzimy ten warunek, otrzymamy regułę podziału, która ma lewą regułę, która wygląda jak Γ,x:X,y:Y[x],
źródło
Richard Garner napisał fajny artykuł na temat zastosowania vs funsplit, o sile zależnych produktów w teorii typów Martina- Löfa (APAL 160 (2009)), w którym omawia także naturę reguły funsplit wyższego rzędu (w odniesieniu do Peter Schroeder-Heister's Naturalne rozszerzenie naturalnej dedukcji (JSL 49 (1984))).
Richard pokazuje, że w obecności typów tożsamości (oraz zasad formacji i wprowadzenia dlaΠ typy), funsplit można przenosić z powyższą regułą aplikacji + etos zdania, tj. dwie następujące reguły:
Oznacza to, że jeśli masz funsplit, możesz zdefiniować aplikację iη jak wyżej, że ( Π -Prop- η-Comp ) trzyma. Co ciekawsze, jeśli masz aplikację i reguły eta zdania, możesz zdefiniować funsplit.
Co więcej, funsplit jest ściśle silniejszy niż aplikacja: reguły etosu zdań nie są definiowalne w teorii tylko z aplikacją - stąd funsplit nie jest definiowalny, ponieważ wtedy zasady etosu zdania byłyby również. Intuicyjnie dzieje się tak, ponieważ reguły aplikacji dają ci trochę więcej luzu: w przeciwieństwie do funsplit (i eta), nie mówią ci, jakie są funkcje, tylko że można je zastosować do argumentów. Wierzę, że argument Richarda mógłby zostać powtórzonyΣ typy, aby pokazać ten sam wynik dla s p l i t vs prognozy.
Zauważ, że gdybyś miał definitywne reguły eta, z pewnością miałbyś je także propozycyjnie (zη( m ) : = r e fl (m) ). Dlatego myślę, że twoje stwierdzenia „[...], które nam dajeη dla funkcji ”i„ [...] ta ostatnia prezentacja ułatwia uzyskanie η dla par ”są błędne. Agda jednak implementuje η dla obu funkcji i par (jeśli Σ jest zdefiniowany jako rekord), ale nie wynika to z samej aplikacji.
źródło