podświetlany i polaryzujący typy Pi

18

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:

Γf:(a:A)(b:Ba)C(a,b)Γp:Σa:A.BΓsplitfp:Cp

I jest wersja negatywna:

Γp:Σa:A.BΓπ0p:AΓp:Σa:A.BΓπ1p:B[π0p/a]

Ta ostatnia prezentacja ułatwia uzyskanie η dla par, tj. (π0p,π1p)==p dla dowolnej pary p (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:

Γf:Πa:A.BΓs:AΓfs:B[s/a]

Co daje nam η dla funkcji: λx.fx==f .

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:

fΠ(A,B)C(v)Set[vΠ(A,B)]d(y)C(λ(y))[y(x)B(x)[xA]]funsplit(f,d)C(f)

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 .y

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?

pedagand
źródło

Odpowiedzi:

12

Prezentacja eliminacji funkcjonalnej za pomocą jest zdecydowanie nie jest zwykle występowanie w większości zabiegów teorii typu. Uważam jednak, że ta forma jest rzeczywiście „pozytywną” prezentacją eliminacji typów funkcjonalnych. Problem polega na tym, że potrzebujesz formy dopasowania wzorca wyższego rzędu, patrz np.Dale Miller.funsplit

Pozwól mi sformułować twoją regułę w sposób, który jest dla mnie jaśniejszy:

Γf:Πx:A.BΓ,z:Πx:A.BC:SetΓ,[x:A]F(x):Be:C{λx:A.F(x)/z}match f with λx:A.F(x)e:C{f/z}

Gdzie jest aF meta zmiennej typu w kontekście x : .Bx:A

Reguła przepisywania staje się następnie:

match λx:A.t with λx:A.F(x)ee{t{u/x}/F(u)}

Pozwala to zdefiniować aplikację jako:

app(t,u)=match t with λx:A.F(x)F(u)

Poza faktem, że wymaga to posiadania systemu typu „logiczny styl ramowy”, kłopot (i ograniczona potrzeba) unifikacji wyższego rzędu sprawiają, że ta formuła jest niepopularna.

Istnieje jednak miejsce, w którym w literaturze występuje rozróżnienie dodatnie / ujemne: sformułowanie predykatów relacji logicznych . Dwie możliwe definicje (w jednym przypadku) to

[[Πx:A.B]]={tu[[A]],tu[[B]]xu}

i

[[Πx:A.B]]={ttλx.t,u[[A]],t{u/x}[[B]]xu}

Druga wersja jest mniej popularna, ale można ją znaleźć np. W Dówek i Werner .

cody
źródło
1
Wydaje się, że jest to związane ze składnią abstrakcyjną wyższego rzędu, która jest szeroko stosowana w ramach logicznych. W szczególności wydaje się tutaj meta-funkcją. F
dzień
13

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 .

x:X.Y[x]α:.(Πx:X.Y[x]α)α
π1 Jednak nie można zdefiniować drugiego rzutu π 2 : Π p : ( x : X
π1:x:X.Y[x]Xλp:(x:X.Y[x]).pX(λxy.x)
- spróbuj! Możesz zdefiniować dla niego tylko słaby eliminator, dlatego napisałem go egzystencjalnie.π2:Πp:(x:X.Y[x]).Y[π1p]

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],

Γ,x:X,y:Y[x],Γe:CΓ,p:x:X.Y[x],Γlet(x,y)=pine:C
pΓC
Γ,x:X,y:Y[x],[(x,y)/p]Γe:[(x,y)/p]CΓ,p:x:X.Y[x],Γlet(x,y)=pine:C
Neel Krishnaswami
źródło
1
Naprawdę podoba mi się te wszystkie odpowiedzi! Wydaje mi się, że istnieje pewne pojęcie „introspekcji” (zdolność do poznania, że ​​termin ma wartość) ukrytej w odpowiedzi Fredrika, która jest prawdziwym problemem z eta: parametryczność oznacza introspekcję oznacza eta.
cody
10

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:

m:Π(ZA,b)η(m):jareΠ(ZA,b)(m,λx.mx)(Π-Rekwizyt-η)
x:ZAfa(x):b(x)η(λ(fa))=rmifal(λ(fa)):jareΠ(ZA,b)(λ(fa),λ(fa))(Π-Rekwizyt-η-Comp)

Oznacza to, że jeśli masz funsplit, możesz zdefiniować aplikację i η jak wyżej, że (Π-Rekwizyt-η-Komp)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 spljat vs prognozy.

Zauważ, że gdybyś miał definitywne reguły eta, z pewnością miałbyś je także propozycyjnie (z η(m): =rmifal(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.

Fredrik Nordvall Forsberg
źródło