funsplit dan polaritas tipe-Pi

Dalam benang baru-baru ini di milis Agda, pertanyaan dari $\eta$ hukum muncul, di mana Peter Hancock membuat pemikiran komentar .

Pemahaman saya adalah bahwa $\eta$ undang-undang datang dengan tipe negatif, yaitu. penghubung yang aturan pengantarnya tidak bisa dibalik. Untuk menonaktifkan $\eta$ untuk fungsi, Hank menyarankan menggunakan eliminator yang dibuat khusus, funsplit , alih-alih aturan aplikasi yang biasa. Saya ingin memahami ucapan Hank dalam hal polaritas.

Misalnya, ada dua presentasi $\Sigma$ -jenis. Ada eliminator split Martin-Löf tradisional , dalam gaya positif:

$$\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}$$

Dan ada versi negatifnya:

$$\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}$$

Presentasi terakhir ini membuatnya mudah untuk mendapatkan untuk pasangan, yaitu. ( π 0 p , π 1 p ) = = p untuk setiap pasangan p (di mana == adalah singkatan dari kesetaraan definisi). Dalam hal provabilitas, perbedaan ini tidak masalah: secara intuisi, Anda dapat mengimplementasikan proyeksi dengan terbelah, atau sebaliknya.$\eta$$(\pi_0 p , \pi_1 p) == p$$p$

Sekarang, -jenis biasanya (dan saya kira tidak kontroversial) dianggap negatif:$\Pi$

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

Yang memberi kita untuk fungsi: λ x . f x = = f .$\eta$$\lambda x. f x == f$

Namun, dalam surat itu, Hank ingat eliminator funsplit (Pemrograman dalam teori tipe ML, [http://www.cse.chalmers.se/research/group/logic/book/], hal.56). Ini dijelaskan dalam kerangka logis oleh:

$$\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}$$

Menariknya, Nordstrom et al. memotivasi definisi ini dengan mengatakan bahwa "bentuk non-kanonik alternatif [ini] didasarkan pada prinsip induksi struktural". Ada aroma positif yang kuat pada pernyataan ini: fungsi akan 'didefinisikan' oleh konstruktornya, .$\lambda$

Namun, saya tidak bisa cukup memberikan presentasi yang memuaskan dari aturan itu dalam deduksi alami (atau, bahkan lebih baik, kalkulus berurutan). Penggunaan (ab) kerangka logis untuk memperkenalkan tampaknya sangat penting di sini.$y$

Jadi, apakah funsplit merupakan presentasi positif -type? Apakah kita juga memiliki sesuatu yang serupa dalam kalkulus urutan (tidak tergantung)? Seperti apa bentuknya?$\Pi$

Seberapa umum / penasaran itu untuk pembuktian teori di lapangan?

Penyajian eliminasi fungsional menggunakan yang pasti bukan kejadian biasa di sebagian besar perawatan teori tipe. Namun, saya percaya bahwa bentuk ini memang presentasi "positif" dari penghapusan jenis fungsional. Masalahnya di sini adalah bahwa Anda memerlukan bentuk pencocokan pola Orde Tinggi, lihat misalnya Dale Miller .$\mathrm{funsplit}$

Izinkan saya merumuskan kembali aturan Anda dengan cara yang lebih jelas bagi saya:

$$\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}$$

Dimana adalah meta-variabel dari tipe B dalam konteks x : A .$F$$B$$x:A$

Aturan penulisan ulang kemudian menjadi:

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

Ini memungkinkan Anda untuk mendefinisikan aplikasi sebagai:

$$\mathrm{app}(t,u)=\mathrm{match}\ t\ \mathrm{with}\ \lambda x:A. F(x)\Rightarrow F(u)$$

Di luar kenyataan bahwa ini membutuhkan sistem tipe "gaya kerangka logis" untuk valid, kerumitan (dan kebutuhan terbatas) dari penyatuan tingkat tinggi membuat formulasi ini tidak populer.

Namun, ada tempat di mana perbedaan positif / negatif hadir dalam literatur: perumusan predasi hubungan logis . Dua definisi yang mungkin (dalam kasus unary) adalah

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

dan

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

Versi kedua kurang umum, tetapi dapat ditemukan misalnya di Dowek dan Werner .

Inilah perspektif yang sedikit berbeda pada jawaban Fredrik. Pada umumnya kasus bahwa pengkodean tipe Gereja yang tidak sesuai akan memenuhi hukum relevan , tetapi tidak akan memenuhi hukum η .$\beta$$\eta$

Jadi ini berarti kita dapat mendefinisikan pasangan dependen sebagai berikut:

Sekarang, perhatikan bahwa π 1 mudah didefinisikan: π 1 : ∃ x : X

$$\exists x:X.\;Y[x] \triangleq \forall \alpha:\ast.\; (\Pi x:X.\;Y[x] \to \alpha) \to \alpha$$ $\pi_1$ Namun, Anda tidak dapat menentukan proyeksi kedua π 2 : Π p : ( ∃ x : X $$\pi_1 : \exists x:X.\;Y[x] \to X \triangleq \lambda p:(\exists x:X.\;Y[x]).\;p\;X\;(\lambda x\;y.x)$$ - coba! Anda hanya dapat mendefinisikan eliminator yang lemah untuk itu, itulah sebabnya saya menulisnya dengan eksistensial.$\pi_2 : \Pi p:(\exists x:X.\;Y[x]).\; Y[\pi_1\;p]$

Namun, proyeksi kedua dapat diwujudkan , dan dalam model parametrik Anda dapat menunjukkan bahwa ia memiliki perilaku yang tepat juga. (Lihat konsep saya baru-baru ini dengan Derek Dreyer tentang parametrik dalam Kalkulus Konstruksi untuk lebih lanjut tentang ini.) Jadi saya pikir bahwa proyeksi mendasar menuntut beberapa sifat ekstensionalitas yang kuat agar masuk akal.$\pi_2$

Dalam hal kalkulus berurutan, eliminator lemah memiliki aturan yang sedikit mirip:

$$\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$$\Gamma'$$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}$$

Richard Garner telah menulis artikel yang bagus tentang aplikasi vs funsplit, Tentang kekuatan produk dependen dalam teori tipe Martin-Löf (APAL 160 (2009)), yang juga membahas sifat urutan tinggi dari aturan funsplit (dengan mengacu pada Peter Schroeder-Heister's Sebuah ekstensi alami deduksi alami (JSL 49 (1984))).

Richard menunjukkan bahwa di hadapan jenis identitas (dan aturan pembentukan dan pengenalan untuk $\Pi$ jenis), funsplit dapat ditafsirkan dengan aturan aplikasi di atas + eta proposisional, yaitu dua aturan berikut:

$$\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 : 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)}$$

Artinya, jika Anda memiliki funsplit, Anda dapat menentukan aplikasi dan $\eta$ seperti di atas supaya $(\Pi\text{-Prop-$\eta$-Comp})$memegang. Lebih menarik, jika Anda memiliki aplikasi dan aturan eta proposisional, maka Anda dapat mendefinisikan funsplit.

Selain itu, funsplit benar-benar lebih kuat daripada aplikasi: aturan eta proposisional tidak dapat didefinisikan dalam teori dengan hanya aplikasi - maka funsplit tidak dapat ditentukan, karena aturan eta proposisional juga akan berlaku. Secara intuitif, ini karena aturan aplikasi memberi Anda sedikit lebih kendur: tidak seperti funsplit (dan eta), mereka tidak memberi tahu Anda apa fungsinya, hanya saja mereka dapat diterapkan pada argumen. Saya yakin argumen Richard bisa diulangi$\Sigma$ jenis juga, untuk menunjukkan hasil yang sama untuk $\mathsf{split}$ vs proyeksi.

Perhatikan bahwa jika Anda memiliki aturan eta definisi, Anda tentu akan memilikinya secara proposisi (dengan $\eta(m) := \mathsf{refl}(m)$). Jadi, saya pikir pernyataan Anda "[...] yang memberi kami$\eta$ untuk fungsi "dan" [...] presentasi terakhir ini membuatnya mudah diperoleh $\eta$ untuk pasangan "salah. Agda, bagaimanapun, mengimplementasikan $\eta$ untuk fungsi dan pasangan (jika $\Sigma$ didefinisikan sebagai catatan), tetapi ini tidak mengikuti hanya dari aplikasi.