Teorema gratis, di mana?

8

Saya telah menemukan aplikasi web ini yang memungkinkan Anda menghasilkan teorema gratis untuk jenis tertentu.

Teorema yang dihasilkan mengukur lebih dari jenis dan hubungan pada jenis ini. Teorema ini (rumus) adalah teorema yang mana dari teori / sistem logis? Bagaimana sistem ini berhubungan dengan teori persamaan bahasa?

lo.logic functional-programming type-systems parametricity logical-relations pengguna13264
sumber
3
Ini tampaknya menjadi repost dari pertanyaan yang sama tentang Stack Overflow , di mana itu dianggap di luar topik, dan hanya mengumpulkan jawaban sepintas yang menghubungkan ke kertas "Theorems for Free". Sekali lagi, tautan ini relevan.
CA McCann
Terima kasih untuk referensi. Saya telah melihat kertas Wadler, tetapi saya tidak begitu memahaminya. Dia bekerja dengan bingkai semantik, maka hubungan tampaknya ada di antara elemen-elemen dalam bingkai ini. Bagaimana hubungan antara elemen-elemen ini berhubungan dengan logika persamaan bahasa (dalam kasus Wadler, Sistem F)? Dia instantiates hubungan dengan fungsi, apakah fungsi-fungsi ini harus dapat dihitung dalam Sistem F?
user13264
aplikasi web sedang down, adakah mirror di mana saja?
user833970

Jawaban:

14

Rumusnya adalah rumus logika Abadi-Plotkin, yang mereka gambarkan dalam makalah mereka A Logic for Parametric Polymorphism .

Semantik Sistem F yang digunakan Abadi dan Plotkin untuk menafsirkan logika mereka dapat ditemukan di Bainbridge, Freyd, Scedrov, makalah Functorial Polymorphism karya Scott .

Neel Krishnaswami
sumber
2
Terima kasih, makalah pertama sepertinya menjawab pertanyaan pertama saya. Ketika seseorang mengatakan "dengan parametrik jika I: / \ XX-> X, maka a. I {A} = I {A '}. A untuk a: A -> A'", tidak ada yang mengatakan "jika | - I: / \ XX-> X dan "| - a: A -> A 'lalu a. I {A} adalah beta-eta-sesuatu-setara dengan I {A '}. a "? Di mana hubungan ini dengan semantik operasional terjadi? Apa yang akan menjadi model non-parametrik dari Sistem F, dan bukankah itu tidak sesuai dengan semantik operasionalnya?
user13264
Pembicaraan ini menunjukkan contoh fungsi non-parametrik (yang tidak dapat diungkapkan dalam Sistem F). mpi-sws.org/~dreyer/talks/plmw2014-talk.pdf Untuk selebihnya, Anda perlu belajar tentang korespondensi antara denotasi dan semantik operasional, dan hubungan kesehatan . Model dapat berisi fungsi yang tidak sesuai dengan program. Ini melanggar abstracion penuh, tetapi tidak sehat.
Blaisorblade
7

Saya cukup menyukai kertas Wadler, The Girard-Reynolds Isomorphism yang menunjukkan bahwa ada terjemahan dari sistemFke dan dari Logika Predikat Orde Kedua (versi dengan tipe orde tinggi). Satu arah adalah "penghapusan ketergantungan", sebuah ide penting dalam tipe dependen, dan yang lainnya adalah "teorema parametrik" atau teorema yang bebas dari suatu tipe.

Wadler menunjukkan bahwa dalam beberapa kondisi, transformasi ini adalah kebalikan dari satu sama lain.

Jadi untuk menjawab pertanyaan Anda: teorema-gratis dapat diungkapkan dalam bentuk logika orde kedua, yang dijelaskan dalam makalah yang disebutkan di atas.

cody
sumber