Parametrisitas unary vs parametrisitas biner

Saya baru-baru ini menjadi sangat tertarik pada parametrikitas setelah melihat makalah LICS Bernardy and Moulin 2012 ( https://dl.acm.org/citation.cfm?id=2359499 ). Dalam makalah ini, mereka menginternalisasi parametrisitas unary dalam sistem tipe murni dengan tipe dependen dan memberi petunjuk bagaimana Anda dapat memperluas konstruksi ke arities yang sewenang-wenang.

Saya hanya melihat parametrisitas biner yang didefinisikan sebelumnya. Pertanyaan saya adalah: apa contoh teorema menarik yang dapat dibuktikan dengan menggunakan parametrik biner, tetapi tidak dengan parametrik unary? Juga akan menarik untuk melihat contoh teorema yang dapat dibuktikan dengan parametrik tersier, tetapi tidak dengan biner (walaupun saya telah melihat bukti bahwa n-parametrikitas setara dengan n> = 2: lihat http: //www.sato.kuis .kyoto-u.ac.jp / ~ takeuti / art / par-tlca.ps.gz )

Biasanya, Anda menggunakan parametrisitas biner untuk membuktikan kesetaraan program. Adalah tidak wajar untuk melakukan ini dengan model unary, karena hanya berbicara tentang satu program pada satu waktu.

Biasanya, Anda menggunakan model unary jika semua yang Anda minati adalah properti unary. Sebagai contoh, lihat draf terakhir kami, Jenis Substruktural Superfisial , di mana kami membuktikan hasil kesehatan jenis menggunakan model unary. Karena kesehatan berbicara tentang perilaku satu program (jika maka itu baik menyimpang atau mengurangi ke nilai v : A ), model unary cukup. Jika kita ingin membuktikan kesetaraan program sebagai tambahan, kita akan membutuhkan model biner.$e : A$$v : A$

EDIT: Saya baru menyadari bahwa jika Anda melihat makalah kami, itu hanya terlihat seperti model hubungan / realisasi yang lama yang logis. Saya harus mengatakan sedikit lebih banyak tentang apa yang membuatnya (dan model lainnya) parametrik. Pada dasarnya, sebuah model adalah parametrik ketika Anda dapat membuktikan lemma ekstensi identitas untuknya: yaitu, untuk ekspresi tipe apa pun, jika semua variabel tipe bebas terikat pada hubungan identitas, maka ekspresi tipe adalah relasi identitas. Kami tidak secara eksplisit membuktikannya sebagai lemma (saya tidak tahu mengapa, tetapi Anda jarang perlu ketika melakukan model operasional), tetapi properti ini sangat penting untuk kesehatan bahasa kami.

Definisi "relasi" dan "relasi identitas" dalam parametrik sebenarnya agak diperebutkan, dan kebebasan ini sebenarnya penting jika Anda ingin mendukung tipe mewah seperti tipe yang lebih tinggi atau tipe dependen, atau ingin bekerja dengan struktur semantik yang lebih menarik. Akun yang paling mudah diakses dari yang saya tahu ini ada di draf makalah Bob Atkey, Parametricity Relasional untuk Jenis yang Lebih Tinggi .

Jika Anda memiliki selera yang baik untuk teori kategori, ini pertama kali dirumuskan secara abstrak oleh Rosolini dalam makalahnya Reflexive Graphs and Parametric Polymorphism . Sejak itu telah dikembangkan lebih lanjut oleh Dunphy dan Reddy dalam makalah Parametric Limits mereka , dan juga oleh Birkedal, Møgelberg, dan Petersen dalam Domain-teoretis Model Parametrik Polimorfisme Parametrik .

Ini seharusnya komentar untuk jawaban Neel, tapi agak panjang. Didorong oleh petunjuk dari Rasmus Petersen, saya menemukan yang berikut dalam tesis Møgelberg (tekankan milik saya):

Ivar Rummelhoff [36] telah mempelajari pengkodean bilangan asli dalam per-model pada PCA yang berbeda, dan menunjukkan bahwa dalam beberapa model ini, pengkodean berisi lebih dari bilangan alami. Jadi model ini tidak bisa parametrik. Meskipun ia tidak menyebutkannya, ini menunjukkan bahwa parametriitas unary berbeda dari parametrikitas biner (relasional), karena orang dapat dengan mudah menunjukkan bahwa pengkodean bilangan asli dalam setiap model adalah parametrik unary.

Makalah yang dikutip adalah Polynat dalam model PER .

$n$$n$$R$ dapat tertanam ke dalam $(n+1)$hubungan -ary dengan mendefinisikan $R'(\vec{x},y) \iff R(\vec{x}) \land y = x_i$ (untuk beberapa perbaikan $i \in [1..n]$). Dengan kata lain, Anda dapat menggunakannya$n$ argumen dari $n+1$argumen untuk mensimulasikan hubungan yang lebih kecil dan membuat argumen baru sama dengan yang lama. (Perhatikan bahwa kesetaraan adalah kunci untuk melakukan ini.) Jadi, Anda memiliki "lebih" hubungan di arity$n+1$ daripada yang Anda miliki di arity $n$, dan ini berlangsung tanpa batas . Karena lebih banyak relasi berarti parametrikitas yang lebih kuat dan keluarga fungsi yang lebih sedikit akan dianggap "parametrik", kami memahami bahwa "parametriitas sejati" adalah apa yang kami peroleh dalam batas, dan setiap parametrikitas finansial merupakan perkiraan terhadapnya.

Hubungan-hubungan tak terhingga ini telah diformalkan sebagai "hubungan logis Kripke dengan beragam aritas", juga disebut hubungan Jung-Tiuryn. Jung dan Tiuryn ​​telah menunjukkan bahwa parametriitas tak terbatas seperti itu sudah cukup untuk mengkarakterisasi defisiensi lambda, dan O'Hearn dan Riecke telah menunjukkan bahwa itu cukup untuk mengkarakterisasi model yang sepenuhnya abstrak untuk bahasa pemrograman, termasuk PCF berurutan. Ini adalah hasil yang fundamental dan indah!

Dengan demikian, parametrisitas unary adalah yang paling sederhana, dan paling ekspresif, perkiraan parametrisitas sejati, dan parametrisitas biner menjadi sedikit lebih baik. Pertanyaan Anda adalah "seberapa baik"? Kesan saya adalah bahwa itu jauh lebih baik. Alasannya adalah bahwa, pada tingkat unary, "hubungan identitas" adalah hubungan yang benar, yang tidak terlalu berarti. Pada tingkat biner, "hubungan identitas" adalah kesetaraan. Jadi, Anda mendapatkan lompatan tiba-tiba dalam kekuatan parametrikitas dalam beralih dari tingkat unary ke binary. Setelah itu, semakin disempurnakan.

Kurt Sieber telah mempelajari masalah ini secara mendalam: untuk urutan dan untuk bahasa seperti Algol .

Mungkin makalah termudah untuk membaca untuk aplikasi parametriitas biner adalah Teorema Wadler Gratis! .

Sebenarnya, saya sedikit terkejut dengan pertanyaan ini karena parametrik biner adalah yang paling sering disebutkan dalam makalah parametrik. Bahkan kertas Reynolds asli "Jenis, abstraksi dan parametrik polimorfisme" menyebutkannya di mana-mana. Ini lebih merupakan parametrik unary yang tidak banyak diketahui.