Seperti yang disebutkan dalam judul, saya ingin tahu ada hubungan dan perbedaan antara CIC dan ITT. Bisakah seseorang menjelaskan atau menunjuk kepada saya beberapa literatur yang membandingkan kedua sistem ini? Terima kasih.
type-theory
hari
sumber
sumber
Jawaban:
Saya sudah menjawabnya sedikit, tetapi saya akan mencoba memberikan gambaran yang lebih rinci tentang tipe horizon teoretis, jika Anda mau.
Saya agak bingung dengan spesifikasi sejarah, sehingga pembaca yang lebih berpengetahuan harus memaafkan saya (dan mengoreksi saya!). Kisah dasarnya adalah bahwa Curry telah mengungkap korespondensi dasar antara combinator yang diketik sederhana (atau -terms) dan logika proposisional, yang diperluas oleh Howard untuk mencakup logika tingkat pertama, dan IIRC secara independen ditemukan oleh de Bruijn dalam penyelidikan di sekitar yang sangat besar. sistem Automath yang berpengaruh .λ
Sistem Automath adalah penyempurnaan teori tipe sederhana Gereja yang dengan sendirinya merupakan penyederhanaan dramatis teori tipe Russel dan Whitehead dengan alam semesta dan aksioma reducibilitas . Ini adalah medan logis yang relatif terkenal pada 1960-an.
Menentukan aturan eliminasi yang sesuai. Dia kemudian memberikan sistem dasar yang sangat kuat berdasarkan penilaian seperti itu, yang memungkinkannya untuk memberikan sistem dasar yang mirip dengan Automath menggunakan sangat sedikit konstruksi sintaksis. Girard menemukan bahwa sistem ini kontradiktif, mendorong Martin-Lof untuk mengadopsi alam semesta predikatif "gaya-Russel" , sangat membatasi ekspresi teori (dengan secara efektif menghilangkan aksioma reducibilitas) dan membuatnya sedikit lebih kompleks (tetapi memiliki keunggulan dari membuatnya konsisten).
Konstruksi elegan yang memungkinkan definisi simbol logis tidak berfungsi lagi, yang mendorong ML untuk memperkenalkan mereka dalam bentuk yang berbeda, sebagai keluarga yang didefinisikan secara induktif . Ini adalah ide yang sangat kuat, karena memungkinkan mendefinisikan segala sesuatu dari kesetaraan penilaian dan operator logis untuk bilangan alami dan tipe data fungsional seperti yang muncul dalam ilmu komputer. Perhatikan bahwa setiap keluarga yang kita tambahkan mirip dengan menambahkan sejumlah aksioma, yang perlu dibenarkan sebagai konsisten dalam setiap contoh. Sistem ini (tipe dependen + semesta + keluarga induktif) biasanya disebut sebagai ITT .
Namun ada beberapa frustrasi yang berkepanjangan, karena sistem dasar yang kuat tetapi sederhana tidak konsisten, dan sistem yang dihasilkan lebih kompleks, dan agak lemah (dalam arti sulit untuk mengembangkan banyak kerangka matematika modern di dalamnya). Masukkan Thierry Coquand, yang bersama atasannya Gerard Huet, memperkenalkan Calculus of Constructions (CoC) , yang sebagian besar memecahkan masalah ini: pendekatan terpadu untuk bukti dan tipe data, sistem dasar yang kuat (tak terduga) dan kemampuan untuk mendefinisikan "konstruksi" "Dari variasi logis atau matematis. Ini akhirnya berkembang menjadi implementasi aktual dari sebuah sistem yang dirancang sebagai alternatif modern untuk Automath, yang berpuncak pada sistem Coq yang kita kenal dan cintai.
Saya sangat menyarankan makalah mendasar ini pada CoC, karena Thierry mengetahui jumlah yang konyol tentang perkembangan sejarah teori jenis, dan mungkin menjelaskan ini jauh lebih baik daripada saya. Anda mungkin juga ingin memeriksa artikelnya tentang teori jenis, meskipun tidak jelaskan korespondensi CH secara mendetail.
sumber