Bagaimana saya bisa mempelajari teori yang mendasari asisten bukti Coq?
40
Saya akan mempelajari catatan kursus di CIS 500: Yayasan Perangkat Lunak dan latihannya sangat menyenangkan. Saya hanya pada set latihan ketiga tetapi saya ingin tahu lebih banyak tentang apa yang terjadi ketika saya menggunakan taktik untuk membuktikan hal-hal sepertiforall (n m : nat), n + n = m + m -> n = m.
Satu tempat untuk memulai adalah manual referensi Coq ( pdf ). Bab 4 menjelaskan logika yang mendasari Coq, dan akhirnya semuanya didasarkan pada ini. Ini disebut kalkulus konstruksi induktif (co), dan banyak makalah menjelaskan. Mendapatkan buku Coq'Art Anda, Provor Teorema Interaktif dan Pengembangan Program menyediakan pengenalan Coq yang lebih santai tapi tidak murah.
Untuk membangun teori yang dibutuhkan, Anda perlu belajar tentang Type Theory . Yang paling dekat hubungannya dengan teori yang mendasari seorang asisten pembuktian mungkin adalah Catatan (atau buku ) Tipe Teori Per Martin-Löf atau buku Programming dalam Teori Tipe Martin-Löf , yang benar-benar tentang penulisan dan pembuktian teorema dalam teori tipe. Perspektif bahasa pemrograman tentang teori jenis dapat diperoleh dari Jenis - Jenis dan Bahasa Pemrograman Pierce . Bukti dan Jenis Girard et al , yang juga membahas pentingnya Korespondensi Curry-Howard , adalah referensi bagus lainnya. Maka Anda mungkin baik dan benar-benar siap untuk membaca Coquand dan HuetKalkulus Konstruksi . Akhirnya kejar beberapa referensi di bagian belakang manual Coq.
Ada asisten bukti lainnya , HOL, NuPRL, Mizar, Twelf, dll, dan mereka juga memiliki teorinya, sehingga Anda dapat belajar banyak juga dengan membaca ke arah itu.
Akhirnya, untuk ikhtisar sejarah dan masa depan asisten bukti, lihat artikel terbaru oleh Herman Geuvers.
Daftar yang bagus. Saya akan menambahkan urutan membaca. Pierce's TAPL mencakup latar belakang; sebagian besar sisanya tidak akan masuk akal sampai Anda fasih dengan aturan mengetik. Bab 2 ATTAPL memperkenalkan tipe-tipe dependen secara relatif lembut. Kemudian Anda dapat membaca bab 4 dari manual Coq, yang memiliki aturan pengetikan (Anda perlu memeriksa daftar pustaka untuk beberapa hal lanjut seperti aturan persis untuk rekursi). Secara paralel, buku Coq'Art memiliki pandangan yang lebih praktis. Kiat bonus: Show Treedalam coq.
Gilles 'SO- stop being evil'
2
Saya seseorang yang kurang lebih memiliki posisi yang sama dengan OP meskipun sedikit lebih jauh. Setelah beberapa percobaan, saya akhirnya menemukan urutan 1) Belajar pemrograman fungsional 2) membaca TAPL 3) Baca tentang tipe dependen dalam ATTAPL untuk bekerja lebih baik daripada hal-hal lain. Senang mengetahui bahwa saya berada di jalur yang benar.
John Salvatier
1
Saya di sini juga, dan mendapat buku Coq'Art. Ini benar-benar sempurna untuk memahami, mereka masuk ke setiap taktik secara rinci dan menjelaskan kapan dan bagaimana menggunakannya. Buku ini juga memandu Anda dengan cepat melalui setiap aturan dasar dalam teori tipe, mengajarkan Anda notasi dan bagaimana menggunakannya dalam Coq. Suka buku ini.
Lance Pollard
15
Adapun kalkulus lambda yang diketik, logika intuitionistic, berbagai sistem bukti dan Curry-Howard isomorphism, yang semuanya adalah bagian dari latar belakang matematika Coq, saya sangat merekomendasikan "Ceramah tentang Curry-Howard Isomorphism" (oleh P. Urzyczyn dan M. Sørensen).
Show Treedalam coq.Adapun kalkulus lambda yang diketik, logika intuitionistic, berbagai sistem bukti dan Curry-Howard isomorphism, yang semuanya adalah bagian dari latar belakang matematika Coq, saya sangat merekomendasikan "Ceramah tentang Curry-Howard Isomorphism" (oleh P. Urzyczyn dan M. Sørensen).
sumber
Buku Luo tentang Extended Calculus of Constructions juga merupakan referensi yang bagus. ECC cukup berpengaruh dalam desain teori tipe Coq.
sumber
Buku Yayasan Perangkat Lunak saat ini tidak menjelaskan semua ini nanti: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html
Jadi jika Anda mengikuti buku ini, baca saja :)
sumber