podświetlany i polaryzujący typy Pi

18

W ostatnim wątku na liście mailingowej Agdy pojawiło się pytanie o prawa $\eta$ , w których Peter Hancock wypowiedział się prowokująco .

Rozumiem, że prawa $\eta$ mają typy negatywne, tj. łączniki, których zasady wprowadzania są odwracalne. Aby wyłączyć $\eta$ 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 $\Sigma$ . Istnieje tradycyjny eliminator podziału Martin-Löf , w pozytywnym stylu:

\begin{array}{l} Γ ⊢ f : (a : A) (b : B a) \to C (a, b) \\ Γ ⊢ p : Σ a : A . B \\ Γ ⊢ s p l i t f p : C p \end{array}

$\begin{array}{l} \Gamma \vdash f : (a : A)(b : B\: a) \to C (a , b) \\ \Gamma \vdash p : \Sigma a : A. B \\ \hline \\ \Gamma \vdash \mathrm{split}\: f\: p : C\: p \end{array}$

I jest wersja negatywna:

\begin{array}{l} Γ ⊢ p : Σ a : A . B \\ Γ ⊢ π_{0} p : A \end{array} \begin{array}{l} Γ ⊢ p : Σ a : A . B \\ Γ ⊢ π_{1} p : B [π_{0} p / a] \end{array}

$\begin{array}{l} \Gamma \vdash p : \Sigma a : A. B \\ \hline \\ \Gamma \vdash \pi_0\: p : A \end{array} \qquad \begin{array}{l} \Gamma \vdash p : \Sigma a : A. B \\ \hline \\ \Gamma \vdash \pi_1\: p : B[\pi_0\: p / a] \end{array}$

Ta ostatnia prezentacja ułatwia uzyskanie $\eta$ dla par, tj. $(\pi_0 p , \pi_1 p) == 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 $\Pi$ są zwykle (i, jak sądzę, bez kontrowersji) traktowane negatywnie:

\begin{array}{l} Γ ⊢ f : Π a : A . B \\ Γ ⊢ s : A \\ Γ ⊢ f s : B [s / a] \end{array}

$\begin{array}{l} \Gamma \vdash f : \Pi a : A. B \\ \Gamma \vdash s : A \\ \hline \\ \Gamma \vdash f s : B[s / a] \end{array}$

Co daje nam $\eta$ dla funkcji: $\lambda x. f x == 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:

\begin{array}{l} f \in Π (A, B) \\ C (v) S e t [v \in Π (A, B)] \\ d (y) \in C (λ (y)) [y (x) \in B (x) [x \in A]] \\ f u n s p l i t (f, d) \in C (f) \end{array}

$\begin{array}{l} f \in \Pi(A, B) \\ C(v)\: Set [v \in \Pi(A, B)] \\ d(y) \in C(\lambda(y)) [y(x) \in B(x) [x \in A]] \\ \hline \\ \mathrm{funsplit}(f, d) \in C(f) \end{array}$

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, . $\lambda$

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? $\Pi$

Jak częste / ciekawe jest to dla teoretyków dowodów w tej dziedzinie?

— pedagand
źródło

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. $\mathrm{funsplit}$

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

\begin{array}{l} Γ ⊢ f : Π x : A . B \\ Γ, z : Π x : A . B ⊢ C : S e t \\ Γ, [x : A] F (x) : B ⊢ e : C {λ x : A . F (x) / z} \\ m a t c h f w i t h λ x : A . F (x) \Rightarrow e : C {f / z} \end{array}

$\begin{array}{l} \Gamma\vdash f : \Pi x:A. B \\ \Gamma, z:\Pi x:A. B\vdash C : Set\\ \Gamma, [x:A]F(x):B\vdash e : C\{\lambda x:A.F(x)/z\}\\ \hline \\ \mathrm{match}\ f\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow e : C\{f/z\} \end{array}$

Gdzie jest a $F$ meta zmiennej typu w kontekście . $B$ $x:A$

Reguła przepisywania staje się następnie:

m a t c h λ x : A . t w i t h λ x : A . F (x) \Rightarrow e \to e {t {u / x} / F (u)}

$\mathrm{match}\ \lambda x:A.t\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow e\quad \rightarrow\quad e\{t\{u/x\}/F(u)\}$

Pozwala to zdefiniować aplikację jako:

a p p (t, u) = m a t c h t w i t h λ x : A . F (x) \Rightarrow F (u)

$\mathrm{app}(t,u)=\mathrm{match}\ t\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow 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]] = {t ∣ \forall u \in [[A]], t u \in [[B]]_{x \mapsto u}}

$[\![\Pi x:A.B]\!] = \{t\mid \forall u\in [\![ A]\!], tu \in[\![B]\!]_{x\mapsto u} \}$

i

[[Π x : A . B]] = {t ∣ t \to^{*} λ x . t^{'}, \forall u \in [[A]], t^{'} {u / x} \in [[B]]_{x \mapsto u}}

$[\![\Pi x:A.B]\!] = \{t\mid t\rightarrow^* \lambda x.t', \forall u\in[\![A]\!], t'\{u/x\}\in[\![B]\!]_{x\mapsto u}\}$

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

$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 . $\beta$ $\eta$

Oznacza to, że możemy zdefiniować parę zależną w następujący sposób:

teraz zauważyć, że łatwo definiowane:

\exists x : X . Y [x] ≜ \forall α : * . (Π x : X . Y [x] \to α) \to α

$\exists x:X.\;Y[x] \triangleq \forall \alpha:\ast.\; (\Pi x:X.\;Y[x] \to \alpha) \to \alpha$

π_{1}

$\pi_1$

Jednak nie można zdefiniować drugiego rzutu

π_{1} : \exists x : X . Y [x] \to X ≜ λ p : (\exists x : X . Y [x]) . p X (λ x y . x)

$\pi_1 : \exists x:X.\;Y[x] \to X \triangleq \lambda p:(\exists x:X.\;Y[x]).\;p\;X\;(\lambda x\;y.x)$

- spróbuj! Możesz zdefiniować dla niego tylko słaby eliminator, dlatego napisałem go egzystencjalnie.

π_{2} : Π p : (\exists x : X . Y [x]) . Y [π_{1} p]

$\pi_2 : \Pi p:(\exists x:X.\;Y[x]).\; Y[\pi_1\;p]$

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. $\pi_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, żenie występują wolne wlub. Jeśli złagodzimy ten warunek, otrzymamy regułę podziału, która ma lewą regułę, która wygląda jak

\frac{Γ, x : X, y : Y [x], Γ^{'} ⊢ e^{'} : C}{Γ, p : \exists x : X . Y [x], Γ^{'} ⊢ l e t (x, y) = p i n e^{'} : C}

$\frac{\Gamma, x:X, y:Y[x],\; \Gamma' \vdash e' : C} {\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : C}$

p

$p$

Γ^{'}

$\Gamma'$

C

$C$

\frac{Γ, x : X, y : Y [x], [(x, y) / p] Γ^{'} ⊢ e^{'} : [(x, y) / p] C}{Γ, p : \exists x : X . Y [x], Γ^{'} ⊢ l e t (x, y) = p i n e^{'} : C}

$\frac{\Gamma, x:X, y:Y[x],\; [(x,y)/p]\Gamma' \vdash e' : [(x,y)/p]C} {\Gamma, p:\exists x:X.\,Y[x],\; \Gamma' \vdash \mathsf{let}(x,y)=p\;\mathsf{in}\;e' : 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 $\Pi$ typy), funsplit można przenosić z powyższą regułą aplikacji + etos zdania, tj. dwie następujące reguły:

\frac{m : Π (ZA, b)}{η (m) : {ja re}_{Π (ZA, b)} (m, λ x . m \cdot x)} (Π -Rekwizyt- η)

$\frac{m : \Pi(A,B)}{\eta(m) : \mathsf{Id}_{\Pi(A,B)}(m, \lambda x . m\cdot x)} \qquad (\Pi\text{-Prop-$\eta$)}$

\frac{x : ZA ⊢ fa (x) : b (x)}{η (λ (fa)) = r mi fa l (λ (fa)) : {ja re}_{Π (ZA, b)} (λ (fa), λ (fa))} (Π -Rekwizyt- η -Comp)

$\frac{x : A \vdash f(x) : B(x)}{\eta(\lambda(f)) = \mathsf{refl}(\lambda(f)) : \mathsf{Id}_{\Pi(A,B)}(\lambda(f), \lambda (f))} \qquad (\Pi\text{-Prop-$\eta$-Comp)}$

Oznacza to, że jeśli masz funsplit, możesz zdefiniować aplikację i $\eta$ jak wyżej, że $(\Pi\text{-Prop-$\eta$-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 $\Sigma$ typy, aby pokazać ten sam wynik dla $\mathsf{split}$ vs prognozy.

Zauważ, że gdybyś miał definitywne reguły eta, z pewnością miałbyś je także propozycyjnie (z $\eta(m) := \mathsf{refl}(m)$ ). Dlatego myślę, że twoje stwierdzenia „[...], które nam daje $\eta$ dla funkcji ”i„ [...] ta ostatnia prezentacja ułatwia uzyskanie $\eta$ dla par ”są błędne. Agda jednak implementuje $\eta$ dla obu funkcji i par (jeśli $\Sigma$ jest zdefiniowany jako rekord), ale nie wynika to z samej aplikacji.

— Fredrik Nordvall Forsberg
źródło