Bagaimana saya harus berpikir tentang jaring bukti?

Dalam jawabannya untuk pertanyaan ini , Stephane Gimenez menunjuk saya ke algoritma normalisasi waktu polinomial untuk bukti dalam logika linier. Buktinya dalam makalah Girard menggunakan jaring bukti, yang merupakan aspek dari logika linier yang sebenarnya saya tidak tahu banyak tentang itu.

Sekarang, saya sudah mencoba membaca makalah tentang jaring bukti sebelumnya (seperti catatan Pierre-Louis Curien ), tetapi saya belum benar-benar memahaminya. Jadi pertanyaan saya adalah: bagaimana saya harus memikirkannya? Dengan "cara berpikir tentang mereka", yang saya maksud adalah intuisi informal di belakang mereka (misalnya, bagaimana mereka berperilaku secara komputasi, atau bagaimana mereka terkait dengan urutan), dan juga teorema mana tentang mereka yang harus saya buktikan pada diri saya sendiri untuk benar-benar mendapatkannya.

Dalam menjawab pertanyaan ini, Anda dapat mengasumsikan (1) Saya tahu teori bukti logika linier dengan baik (termasuk hal-hal seperti bagaimana bukti cut-elimination berjalan, dan dalam bentuk terfokus juga), (2) semantik kategorikal mereka dalam hal ruang koherensi atau melalui konvolusi Day, dan (3) dasar yang sangat mendasar dari konstruksi Pemerintah Indonesia.

Jaring bukti pada dasarnya menarik karena tiga alasan:

1) IDENTITAS BUKTI. Mereka memberikan jawaban untuk masalah "kapan dua bukti sama"? Dalam kalkulus berurutan Anda mungkin memiliki banyak bukti berbeda dari proposisi yang sama yang berbeda hanya karena kalkulus berurutan memaksa urutan di antara aturan deduksi bahkan ketika ini tidak diperlukan. Tentu saja, seseorang dapat menambahkan relasi ekivalensi pada bukti kalkulus berurutan, tetapi kemudian kita harus menunjukkan bahwa cut-elimination berperilaku baik pada kelas-kelas ekivalensi, dan juga perlu beralih ke penulisan ulang modulo, yang jauh lebih teknis daripada penulisan ulang biasa. Jala bukti memecahkan masalah berurusan dengan kelas ekivalensi dengan menyediakan sintaksis di mana setiap kelas ekivalensi diciutkan pada satu objek. Situasi ini memang agak idealis, karena untuk banyak alasan jaring bukti sering diperpanjang dengan beberapa bentuk kesetaraan.

2) TANPA LANGKAH-LANGKAH PENGHAPUSAN KOMUTATIF. Eliminasi potong pada jaring bukti memiliki rasa yang sangat berbeda dari pada kalkulus berurutan karena langkah eliminasi potongan komutatif menghilang. Alasannya adalah bahwa dalam jaring bukti aturan pengurangan hanya dihubungkan oleh hubungan sebab akibat mereka. Kasus komutatif dihasilkan oleh fakta bahwa satu aturan dapat disembunyikan oleh aturan lain yang tidak terkait. Ini tidak dapat terjadi dalam jaring bukti, di mana aturan yang tidak terkait secara berjauhan terpisah jauh. Karena sebagian besar kasus eliminasi cut bersifat komutatif, maka penyederhanaan cut-eliminasi sangat mencolok. Ini sangat berguna untuk mempelajari kalkulus lambda dengan substitusi eksplisit (karena eksponensial = substitusi eksplisit). Sekali lagi, situasi ini diidealkan karena beberapa presentasi jaring bukti memerlukan langkah komutatif. Namun,

3) KRITERIA KEBENARAN. Jaring bukti dapat didefinisikan dengan terjemahan bukti kalkulus secara berurutan, tetapi biasanya sistem jaring bukti tidak diterima kecuali jika dilengkapi dengan kriteria kebenaran, yaitu seperangkat prinsip-prinsip teoretis-grafik yang mencirikan serangkaian grafik yang diperoleh dengan menerjemahkan suatu bukti kalkulus berurutan. Alasan untuk memerlukan kriteria kebenaran adalah bahwa bahasa grafis gratis yang dihasilkan oleh set konstruktor jaring bukti (disebut tautan) mengandung "terlalu banyak grafik", dalam arti bahwa beberapa grafik tidak sesuai dengan bukti apa pun. Relevansi pendekatan kriteria kebenaran biasanya sepenuhnya disalahpahami. Ini penting karena memberikan definisi non-induktif tentang apa yang merupakan bukti, memberikan perspektif yang sangat berbeda tentang sifat deduksi. Fakta bahwa penokohannya bersifat non-induktif biasanya dikritik, padahal itulah yang menarik. Tentu saja, tidak mudah menerima formalisasi, tetapi, sekali lagi, inilah kekuatannya: jaring bukti memberikan wawasan yang tidak tersedia melalui perspektif induktif yang biasa mengenai bukti dan ketentuan. Teorema dasar untuk jaring bukti adalah teorema sekuensialisasi, yang mengatakan bahwa setiap grafik yang memenuhi kriteria kebenaran dapat didekomposisi secara induktif sebagai bukti kalkulus berurutan (menerjemahkan kembali ke grafik yang benar).

Biarkan saya menyimpulkan bahwa tidak tepat untuk mengatakan bahwa jaring bukti adalah versi klasik dan linear dari deduksi alami. Intinya adalah mereka memecahkan (atau mencoba memecahkan) masalah identitas bukti dan bahwa deduksi alami berhasil memecahkan masalah yang sama untuk logika intuitionistic minimal. Tetapi jaring bukti dapat dilakukan juga untuk sistem intuitionistic dan untuk sistem non-linear. Sebenarnya, mereka bekerja lebih baik untuk sistem intuitionistic daripada sistem klasik.

$-A$$A$$-A$$A$

Girard memperhatikan bahwa deduksi alami asimetris persis seperti ini. Itu sebabnya cocok dengan logika intuitionistic. Jaring bukti merupakan upaya Girard untuk menemukan bentuk deduksi alami yang simetris .

$\land\to$

$\Gamma \vdash A$$\vdash \Gamma^\perp, A$

Sesuatu yang saya lewatkan dalam jawaban asli saya: Jaring bukti adalah cara menulis bukti, dan kita tahu bahwa bukti adalah program. Jadi, jaring bukti juga merupakan cara penulisan program.

Notasi fungsional tradisional untuk program penulisan adalah asimetris, seperti halnya deduksi alami. Jadi, jaring bukti menunjukkan cara menulis program dalam bentuk simetris . Begitulah cara kalkuli memasukkan gambar.

Cara lain untuk merepresentasikan simetri adalah melalui pemrograman logika, yang telah saya jelajahi dalam dua makalah: Yayasan yang diketik untuk program logika arah dan aspek-aspek tingkat tinggi dari pemrograman logika

Saya fokus pada bagaimana jaring bukti terkait dengan kalkulus berurutan, meninggalkan hal-hal yang lebih dinamis.

Bukti jaring bukti kalkulus berurutan: jaring bukti mewakili sekumpulan bukti kalkulus berurutan. Jaring bukti melupakan perbedaan yang tidak penting antara bukti kalkulus berurutan (seperti rumus mana yang diuraikan di bawah ini). Teorema penting di sini adalah "sekuensialisasi", yang mengubah jaring bukti menjadi bukti kalkulus berurutan.

Ini sebagian besar berkaitan dengan bagian "bagaimana mereka berperilaku secara komputasi" dari pertanyaan Anda. Salah satu cara untuk memahami jaring bukti dengan baik dari perspektif komputasi adalah dengan melihat interpretasi yang sedikit lebih konkret (misalnya, proses aljabar).

Anda mungkin tertarik pada yang berikut ini:

• Makalah oleh Abramsky (bagian CLL tentang Bukti Ekspresi): Interpretasi Komputasi Logika Linear . Makalah ini juga menyajikan beberapa hasil yang dekat dengan yang sesuai untuk jaring bukti, jadi mungkin membantu dalam aspek kedua dari pertanyaan Anda.

• Makalah oleh Honda dan Laurent yang menunjukkan bagaimana jenis Jaring Bukti khusus, yang disebut Polarized Proof Nets, sesuai dengan proses Pi-calculus, dan yang disebutkan di atas oleh Martin Berger: Korespondensi yang tepat antara pi-calculus yang diketik dan bukti terpolarisasi- jaring

• (di sini saya tanpa malu-malu mengiklankan karya saya sendiri) Konsep: Jaring Bukti dalam Bentuk Aljabar Proses

Ada juga beberapa karya yang berhubungan dengan jaring bukti dan kalkulus lambda, yang juga memberikan intuisi yang substansial. Misalnya, berikut ini oleh Delia Kesner dan Stéphane Lengrand:

• Operator Sumber Daya untuk λ-calculus

Anda mungkin juga tertarik dengan jenis pekerjaan ini (sangat berorientasi pada aspek teoritis) yang bergantung pada Struktur Bukti untuk membuktikan secara detail properti Normalisasi Kuat LL, oleh Michele Pagani dan Lorenzo Tortora de Falco.

• Properti Normalisasi yang Kuat untuk Logika Linear Orde Kedua (makalah ini berisi peta bagus dari teorema-teorema penting).

Secara umum, teorema mana yang harus dipelajari? Yah, saya hampir tidak memiliki otoritas tetapi Anda mungkin ingin melihat "Sequentialisation" (terkait Bukti Nets dan Sequent Proofs; lihat makalah TCS asli pada LL), dan bukti normalisasi yang kuat (agak terlibat, seperti yang diharapkan, tetapi banyak yang penting Teorema PN terkait dengannya [atau, digunakan untuk membuktikannya]).

Jika Anda terbiasa dengan fokus, Anda mungkin juga tertarik dengan makalah ini oleh Andreoli:

• Fokus dan Bukti-Jaring dalam Linear dan Logika Non-komutatif

Semoga ini membantu. Sekali lagi, referensi ini benar-benar tidak lengkap.

terbaik, Dimitris

Ada pekerjaan yang menarik baru-baru ini pada membuat hubungan antara jaring bukti dan kalkulator lebih ketat, menggunakan varian "multi-fokus" di mana Anda mungkin memiliki beberapa lubang kiri simultan, dan mempelajari bukti "fokus maksimal". Jika Anda memilih kalkulus dengan benar, bukti yang berfokus maksimal dapat sesuai dengan jaring bukti MLL atau, dalam logika klasik, dengan bukti ekspansi ( The Isomorphism Antara Bukti Ekspansi dan Bukti Urutan Multi-Fokus , Kaustuv Chaudhuri, Stefan Hetzl dan Dale Miller, 2013)

Anda dapat memeriksa makalah saya " Sebuah survei jaring bukti dan matriks untuk logika substruktural ".

Abstrak:

Makalah ini adalah survei dari dua jenis skema bukti "terkompresi", metode \ emph {matrix} dan \ emph {proof nets}, seperti yang diterapkan pada berbagai logika mulai dari hierarki substruktural dari klasik sampai ke sistem Lambek nonassociative. Perlakuan baru terhadap jaring bukti untuk yang terakhir disediakan. Deskripsi jaring bukti dan matriks diberikan dalam notasi seragam berdasarkan urutan, sehingga sifat skema untuk berbagai logika dapat dengan mudah dibandingkan.