Deep Link Menyamakan Pembuktian Matematika dan Program Komputer | Majalah Kuanta

Beberapa penemuan ilmiah penting karena mengungkap sesuatu yang baru - struktur heliks ganda DNA, misalnya, atau keberadaan lubang hitam. Namun, beberapa wahyu bersifat mendalam karena menunjukkan bahwa dua konsep lama, yang dulu dianggap berbeda, sebenarnya adalah sama. Misalnya persamaan James Clerk Maxwell yang menunjukkan bahwa listrik dan magnet adalah dua aspek dari fenomena tunggal, atau relativitas umum yang menghubungkan gravitasi dengan ruang-waktu yang melengkung.

Korespondensi Curry-Howard melakukan hal yang sama tetapi dalam skala yang lebih besar, menghubungkan tidak hanya konsep-konsep yang terpisah dalam satu bidang, tetapi seluruh disiplin ilmu: Komputer Ilmu dan logika matematika. Juga dikenal sebagai isomorfisme Curry-Howard (istilah yang berarti terdapat semacam korespondensi satu-ke-satu antara dua hal), isomorfisme ini membangun hubungan antara bukti matematika dan program komputer.

Sederhananya, korespondensi Curry-Howard menyatakan bahwa dua konsep dari ilmu komputer (jenis dan program) masing-masing setara dengan proposisi dan pembuktian — konsep dari logika.

Salah satu dampak dari korespondensi ini adalah bahwa pemrograman — sering kali dipandang sebagai keahlian pribadi — diangkat ke tingkat matematika yang diidealkan. Menulis sebuah program bukan sekedar “coding”, tetapi menjadi suatu tindakan pembuktian sebuah teorema. Ini memformalkan tindakan pemrograman dan menyediakan cara untuk berpikir secara matematis tentang kebenaran program.

Nama korespondensi tersebut diambil dari nama dua peneliti yang menemukannya secara independen. Pada tahun 1934, ahli matematika dan logika Haskell Curry memperhatikan kesamaan antara fungsi dalam matematika dan hubungan implikasi dalam logika, yang berbentuk pernyataan “jika-maka” antara dua proposisi.

Terinspirasi oleh pengamatan Curry, ahli logika matematika William Alvin Howard menemukan hubungan yang lebih dalam antara komputasi dan logika pada tahun 1969, menunjukkan bahwa menjalankan program komputer mirip dengan menyederhanakan pembuktian logis. Saat program komputer dijalankan, setiap baris “dievaluasi” untuk menghasilkan satu keluaran. Demikian pula, dalam pembuktian, Anda memulai dengan pernyataan kompleks yang dapat Anda sederhanakan (dengan menghilangkan langkah-langkah yang berlebihan, misalnya, atau mengganti ekspresi kompleks dengan yang lebih sederhana) hingga Anda sampai pada suatu kesimpulan - pernyataan yang lebih ringkas dan ringkas yang berasal dari banyak pernyataan sementara. .

Meskipun uraian ini menyampaikan pengertian umum tentang korespondensi, untuk memahaminya sepenuhnya kita perlu belajar lebih banyak tentang apa yang oleh para ilmuwan komputer disebut sebagai “teori tipe”.

Mari kita mulai dengan sebuah paradoks yang terkenal: Di sebuah desa hiduplah seorang tukang cukur yang mencukur semua laki-laki yang tidak mencukur dirinya sendiri, dan hanya mereka saja. Apakah tukang cukur mencukur dirinya sendiri? Jika jawabannya ya, maka dia tidak boleh mencukur dirinya sendiri (karena dia hanya mencukur laki-laki yang tidak mencukur dirinya). Jika jawabannya tidak, maka dia harus mencukur dirinya sendiri (karena dia mencukur semua pria yang tidak mencukur dirinya). Ini adalah versi informal dari paradoks yang ditemukan Bertrand Russell ketika mencoba membangun dasar-dasar matematika menggunakan konsep yang disebut himpunan. Artinya, tidak mungkin mendefinisikan suatu himpunan yang memuat semua himpunan yang tidak memuat dirinya sendiri tanpa menemui kontradiksi.

Untuk menghindari paradoks ini, Russell menunjukkan, kita dapat menggunakan “tipe.” Secara kasar, ini adalah kategori yang nilai spesifiknya disebut objek. Misalnya, jika ada tipe yang disebut “Nat”, artinya bilangan asli, objeknya adalah 1, 2, 3, dan seterusnya. Peneliti biasanya menggunakan titik dua untuk menunjukkan jenis suatu objek. Angka 7 yang bertipe integer dapat dituliskan sebagai “7: Integer”. Anda bisa memiliki fungsi yang mengambil objek bertipe A dan mengeluarkan objek bertipe B, atau fungsi yang menggabungkan sepasang objek bertipe A dan bertipe B menjadi tipe baru, yang disebut “A × B.”

Oleh karena itu, salah satu cara untuk menyelesaikan paradoks ini adalah dengan menempatkan tipe-tipe ini ke dalam hierarki, sehingga tipe-tipe tersebut hanya dapat berisi elemen “tingkat yang lebih rendah” dari dirinya sendiri. Maka suatu tipe tidak dapat memuat dirinya sendiri, sehingga menghindari referensialitas diri yang menciptakan paradoks.

Dalam dunia teori tipe, pembuktian bahwa suatu pernyataan benar bisa terlihat berbeda dari yang biasa kita lakukan. Jika kita ingin membuktikan bahwa bilangan bulat 8 adalah bilangan genap, maka yang harus kita lakukan adalah menunjukkan bahwa 8 memang merupakan suatu benda dengan tipe tertentu yang disebut “Genap”, yang aturan keanggotaannya adalah habis dibagi 2. Setelah memverifikasi bahwa 8 habis dibagi dengan 2, kita dapat menyimpulkan bahwa 8 memang merupakan “penghuni” tipe Genap.

Curry dan Howard menunjukkan bahwa tipe pada dasarnya setara dengan proposisi logis. Ketika suatu fungsi “menghuni” suatu tipe — yaitu, ketika Anda berhasil mendefinisikan fungsi yang merupakan objek dari tipe tersebut — Anda secara efektif menunjukkan bahwa proposisi terkait adalah benar. Jadi fungsi yang mengambil masukan bertipe A dan menghasilkan keluaran bertipe B, dilambangkan dengan tipe A → B, harus sesuai dengan implikasi: “Jika A, maka B.” Misalnya saja proposisi “Jika hujan, berarti tanahnya basah”. Dalam teori tipe, proposisi ini akan dimodelkan oleh fungsi dengan tipe “Raining → GroundIsWet.” Formulasi yang tampak berbeda pada kenyataannya secara matematis sama.

Walaupun keterkaitan tersebut terdengar abstrak, hal ini tidak hanya mengubah cara para praktisi matematika dan ilmu komputer memikirkan pekerjaan mereka, namun juga menghasilkan beberapa penerapan praktis di kedua bidang tersebut. Untuk ilmu komputer, ini memberikan landasan teoritis untuk verifikasi perangkat lunak, proses memastikan kebenaran perangkat lunak. Dengan membingkai perilaku yang diinginkan dalam bentuk proposisi logis, pemrogram dapat membuktikan secara matematis bahwa suatu program berperilaku seperti yang diharapkan. Ini juga memberikan landasan teoritis yang kuat untuk merancang bahasa pemrograman fungsional yang lebih kuat.

Dan bagi matematika, korespondensi telah menyebabkan lahirnya asisten bukti, juga disebut pembukti teorema interaktif. Ini adalah perangkat lunak yang membantu dalam membangun bukti formal, seperti Coq dan Lean. Di Coq, setiap langkah pembuktian pada dasarnya adalah sebuah program, dan validitas pembuktian diperiksa dengan algoritma pengecekan tipe. Matematikawan juga telah menggunakan asisten pembuktian — khususnya, Pembukti teorema lean — untuk memformalkan matematika, yang melibatkan penyajian konsep, teorema, dan bukti matematika dalam format yang ketat dan dapat diverifikasi oleh komputer. Hal ini memungkinkan bahasa matematika yang terkadang informal diperiksa oleh komputer.

Para peneliti masih mengeksplorasi konsekuensi dari hubungan antara matematika dan pemrograman. Korespondensi Curry-Howard yang asli menggabungkan pemrograman dengan sejenis logika yang disebut logika intuisionistik, namun ternyata lebih banyak jenis logika yang dapat menerima penyatuan tersebut juga.

“Apa yang terjadi dalam satu abad sejak penemuan Curry adalah bahwa kita terus menemukan lebih banyak contoh di mana 'sistem logika X berhubungan dengan sistem komputasi Y,'” kata Michael Clarkson, seorang ilmuwan komputer di Cornell University. Para peneliti telah menghubungkan pemrograman dengan jenis logika lain seperti logika linier, yang mencakup konsep “sumber daya”, dan logika modal, yang berhubungan dengan konsep kemungkinan dan kebutuhan.

Dan meskipun korespondensi ini memuat nama Curry dan Howard, mereka bukanlah satu-satunya yang menemukannya. Hal ini membuktikan sifat mendasar dari korespondensi: Orang-orang terus memperhatikannya berulang kali. “Tampaknya bukan suatu kebetulan bahwa ada hubungan yang mendalam antara komputasi dan logika,” kata Clarkson.