Apakah analog Curry-Howard untuk logika linier?

Seperti yang didefinisikan oleh Wikipedia,

(Korespondensi Curry-Howard) adalah generalisasi dari analogi sintaksis antara sistem logika formal dan kalkulus komputasi yang pertama kali ditemukan oleh ahli matematika Amerika Haskell Curry dan ahli logika William Alvin Howard.

Terkait dengan itu adalah λ-cube, yang merupakan representasi grafis dari kemungkinan penyempurnaan dari tipe sederhana ke kalkulus konstruksi, yang memiliki interpretasi logis:

Sejauh yang saya tahu, korespondensi Curry-Howard adalah hubungan antara teori tipe dan logika klasik. Pertanyaan saya adalah: apakah ada korespondensi analog antara sistem tipe dan logika linier ?

Anda dapat memaksakan persyaratan yang serupa di dalam sistem tipe Anda, yang berarti mengharuskan objek tidak pernah dihancurkan atau digandakan. Untuk contoh aplikasi praktis, lihat Jenis Linear dapat Mengubah Dunia! oleh Philip Wadler, yang menentukan aturan mengetik untuk ini. Ini juga menunjukkan bagaimana sistem tipe dapat menggabungkan tipe linear dan non-linear.

Untuk aplikasi praktis ini, lihat std::unique_ptrdi C ++. Di sini, linearitas memastikan bahwa deallokasi selalu terjadi tepat sekali.

Dalam bahasa fungsional, linearitas juga memberikan kemungkinan pembaruan destruktif (yang tampak murni bagi programmer). Namun, dalam praktiknya sepertinya monad adalah pendekatan yang lebih umum untuk menyelesaikan masalah ini.

Pembaruan : Saya perhatikan bahwa dalam tabel NLab Computational Trinitarianism tidak adanya kontraksi dalam logika (yaitu tidak dapat menduplikasi asumsi) sesuai dengan Teorema No-Kloning dari mekanika kuantum. Saya (sayangnya) tidak mengerti implikasi dari ini, tetapi saya pikir Anda mungkin menganggapnya menarik.

Logika linier berhubungan dengan sistem tipe untuk kalkulus proses (varian dari kalkulus π internal ), di mana:

• bukti sesuai dengan proses ;
• proposisi sesuai dengan jenis sesi (protokol komunikasi).

Ini adalah area penelitian yang cukup aktif. Sementara orang mengharapkan korespondensi antara logika linier dan beberapa model konkurensi sejak dimulainya logika linear oleh Girard [1987] , menemukan sesuatu yang memuaskan dari perspektif pemodelan logis dan konkurensi agak sulit dipahami.

Berikut ini ringkasan perkembangan kunci sejauh ini.

• Abramsky [1994] dan Bellin dan Scott [1994] mengusulkan korespondensi "Proofs as Processes" pertama, di mana proposisi linear adalah tipe untuk saluran linear dalam kalkulus proses. Misalnya, proposisi ditafsirkan sebagai tipe saluran "send and "; digunakan untuk mengetik proses yang menggunakan saluran untuk menampilkan pesan termasuk sesuatu tipe dan$A \otimes B$$A$$B$$A$$B$(sepasang, jika Anda suka), masing-masing, dan kemudian saluran tersebut tidak boleh digunakan lagi. Gagasan utamanya adalah aturan potong logika linier dapat digunakan untuk mengetik eksekusi paralel dari dua proses yang berkomunikasi melalui saluran pribadi. Pemeriksaan dualitas yang dilakukan oleh aturan potong dalam logika linier berhubungan dengan memeriksa bahwa dua proses menggunakan saluran pribadi bersama dengan cara yang kompatibel.
• Ide dualitas mengilhami juga beberapa disiplin pengetikan untuk kalki proses, terutama tipe linier dan tipe sesi, tetapi hubungan langsung ke logika linier hilang. Jenis sesi khususnya, oleh Honda [1993] , menggambarkan protokol komunikasi dan penerapannya menjadi jelas segera: ide tersebut melahirkan area penelitian.
• Tujuh tahun kemudian setelah Honda mengembangkan tipe sesi, Caires dan Pfenning [2010] menemukan bahwa proposisi dalam logika linier intuitionistic dapat diartikan sebagai tipe sesi. Sebagai contoh, proposisi ditafsirkan sebagai protokol "kirim dan kemudian lanjutkan sebagai ". Penemuan ini telah meremajakan jalur penelitian "Bukti sebagai Proses": ada banyak makalah tentang topik ini yang diterbitkan dalam dekade terakhir. Berkat fondasi logisnya, kita dapat mengimpor ide dari logika untuk memperluas disiplin pengetikan tipe sesi.$A \otimes B$$A$$B$
• Wadler [2014] merumuskan kembali korespondensi dengan tipe sesi untuk logika linier klasik dan meresmikan koneksi pertama antara presentasi standar tipe sesi untuk bahasa fungsional dan logika linier.
• Ada "masalah" yang dibagikan oleh semua karya yang dikutip di atas: sementara sisi logika linier adalah yang diharapkan, sisi kalkulus proses tidak, baik secara sintaksis dan semantik. Sebagai contoh, perbedaan yang mencolok adalah bahwa komposisi paralel ( ) bukan konstruktor istilah mandiri, karena tidak memiliki aturan yang sesuai untuk alasan tentang hal itu secara langsung dalam logika linier. Masalah ini telah diatasi dalam [Kokke et al., 2019] (disclaimer: Saya salah satu penulis), dengan merumuskan kembali secara konservatif aturan untuk , potong, dan campuran. Ini memunculkan transformasi bukti baru, yang ternyata sesuai dengan semantik pengamatan yang diharapkan dari kalkulus..$P|Q$$\otimes$

Jika Anda mencari beberapa kertas untuk memulai, saya akan mulai dari [Wadler, 2014] dan kemudian [Kokke et al., 2019] (untuk melihat sistem terbaru).