- Tipe dependen (type theory) mencakup objek bukti, tetapi penulis menilainya sebagai struktur yang tidak perlu dan tidak efisien
- Penulis pernah meneliti langsung sistem berbasis tipe dependen lama seperti AUTOMATH dan sistem formal Martin-Löf, tetapi Isabelle berkembang sebagai kerangka logika generik
- Isabelle/HOL yang berbasis pada teori tipe sederhana (higher-order logic) memiliki keunggulan dalam otomatisasi, pustaka skala besar, dan keterbacaan
- Melalui proyek ALEXANDRIA, telah dibuktikan bahwa bahkan hanya dengan logika orde tinggi pun formalisasi teorema matematika tingkat lanjut dimungkinkan
- Meski sistem tipe dependen seperti Lean makin matang, penulis tetap lebih memilih kepraktisan pendekatan logika orde tinggi karena masalah performa dan kompleksitas
Tipe dependen dan objek bukti
- Dalam teori tipe dependen, objek bukti (proof objects) bersifat esensial, tetapi penulis menganggapnya sebagai pemborosan ruang
- Dalam arsitektur LCF, hanya langkah pembuktian yang sah yang dapat dijalankan melalui pemeriksaan tipe di level bahasa implementasi, bukan di dalam logika itu sendiri
- Berkat wawasan Robin Milner, konsep proof kernel diperkenalkan dan menjadi fondasi Isabelle
- Menanggapi pertanyaan “mengapa tidak menggunakan tipe dependen”, penulis menjawab bahwa ia sudah lama menggunakannya
Pengalaman dengan AUTOMATH
- Pada 1977 di Caltech, penulis menghadiri kuliah N. G. de Bruijn tentang AUTOMATH, tetapi tidak sempat menggunakan sistemnya secara langsung
- Saat itu sistem universitas Eindhoven tidak terhubung ke ARPAnet, dan diperlukan komputer berbasis ALGOL 60
- AUTOMATH adalah sistem tipe dependen, tetapi tidak mengimplementasikan korespondensi Curry–Howard
- Pengguna harus menambahkan sendiri simbol dan aturan inferensi dari logika yang diinginkan sebagai aksioma
- de Bruijn mengibaratkannya sebagai “restoran besar yang menyediakan semua makanan”
- Isabelle mewarisi gagasan ini dan mengejar keumuman sebagai kerangka logika
- Namun, de Bruijn membenci teori himpunan dan memandang matematika pada dasarnya sebagai sesuatu yang berbasis tipe
- Penulis sempat mempertanyakan verifikasi keabsahan AUTOMATH, dan de Bruijn mengirimkan buku teori bahasa (300 halaman), tetapi itu tidak memuaskan
Teori tipe formal Martin-Löf
- Saat meneliti teori tipe formal Martin-Löf di Universitas Chalmers, Göteborg, penulis terpesona oleh kemungkinan sintesis program
- Ia menilai pendekatan ini jelas “benar” karena langsung mengimplementasikan prinsip logika intuisionistik Heyting
- Selama beberapa tahun penelitian, penulis mengimplementasikan versi awal Isabelle dengan teori Martin-Löf
- Hingga kini, itu masih disertakan dalam distribusi sebagai Isabelle/CTT
- Namun kemudian penelitian itu runtuh akibat suasana dogmatis yang berpusat pada Per Martin-Löf dan peralihan yang dipaksakan ke intensional equality intrinsik
- Sistem-sistem berikutnya seperti Calculus of Constructions(CoC), Rocq, dan Lean pun meninggalkan pertanyaan yang sama
- CoC telah melalui berbagai varian dan aksioma opsional selama puluhan tahun
Pilihan riset dan arah Isabelle
- Para peneliti harus memilih antara mengembangkan sistem formal baru dan memperluas serta memanfaatkan sistem yang sudah ada
- Isabelle dirancang sebagai kerangka yang digeneralisasi agar dapat menampung berbagai logika
- Pada 1985, Mike Gordon melakukan verifikasi perangkat keras dengan teori tipe sederhana Church
- Setelah itu John Harrison merancang pengodean dimensi vektor
- Isabelle/HOL menambahkan kelas tipe aksiomatik dan sistem modul locale ke teori Church
- Komunitas Lean, berbasis CoC, berhasil mencapai formalisasi matematika berskala besar (mathlib)
Proyek ALEXANDRIA dan uji batas logika orde tinggi
- Proyek ALEXANDRIA yang didukung ERC menekankan otomatisasi, pustaka, dan keterbacaan Isabelle
- Pada awalnya diperkirakan logika orde tinggi akan menemui batas, tetapi dalam praktiknya matematika tingkat lanjut seperti skema Grothendieck pun berhasil diformalkan
- Paulo Emílio de Vilhena dan Martin Baillon membuktikan bahwa setiap medan memiliki ekstensi tertutup aljabar
- Proyek ini meluas hingga hasil tingkat lanjut seperti teorema Balog–Szemerédi–Gowers
- Klaim bahwa “formalisasi matematika mustahil tanpa tipe dependen” menghilang, dan yang tersisa hanya klaim bahwa “tipe dependen lebih rapi”
Lean dan pandangan saat ini tentang tipe dependen
- Skala komunitas Lean dan alat Blueprint memang membuat iri, tetapi masalah performa dan kompleksitas tetap ada
- Benturan dengan intensional equality dan sulitnya menentukan kapan harus memakai tipe dependen terus dilaporkan berulang kali
- Penulis mengibaratkan tipe dependen seperti Full Self-Driving milik Tesla, untuk menunjukkan ekspektasi berlebihan dan ketidaknyamanan dalam praktik
Lampiran: batas teoretis logika orde tinggi
- Sebagian orang berpendapat bahwa logika orde tinggi lemah secara teori bukti, tetapi itu hanya berarti lebih lemah dibanding teori himpunan ZF
- Menurut hasil ALEXANDRIA, logika orde tinggi pun dapat menangani struktur matematika kompleks seperti skema Grothendieck
- Hanya dua bukti yang memerlukan penambahan aksioma ZF, dan keduanya adalah teorema yang secara langsung menyebut objek ZF
Catatan kaki
- Intuisionisme adalah filsafat yang memandang bahasa sebagai sarana pencatatan semata, dan berbeda dari matematika konstruktif (constructive mathematics) masa kini
Belum ada komentar.