Hubungan mendalam antara logik matematik dan kod program komputer: cermin imej antara satu sama lain

Sesetengah penemuan saintifik diberi kepentingan yang besar kerana sesuatu yang baru didedahkan, seperti struktur double helix DNA atau kewujudan lubang hitam. Tetapi pendedahan ini mempunyai makna yang lebih mendalam, kerana ia menunjukkan bahawa dua konsep lama yang sebelum ini kelihatan sangat berbeza sebenarnya adalah sama. Sebagai contoh, James Clerk Maxwell menemui sistem persamaan yang menunjukkan bahawa elektrik dan kemagnetan adalah aspek fenomena yang sama, manakala kerelatifan am mengaitkan graviti dengan ruang-masa yang melengkung.

Begitu juga dengan surat-menyurat Curry-Howard, dan ia bukan hanya mengaitkan dua konsep berbeza dalam satu bidang, tetapi dua disiplin lengkap: sains komputer dan logik matematik. Surat-menyurat ini juga dikenali sebagai isomorfisme Curry-Howard (isomorfisme merujuk kepada surat-menyurat satu-dengan-satu tertentu antara dua perkara), yang mewujudkan hubungan tertentu antara pembuktian matematik dan program komputer .

Ringkasnya, surat-menyurat Currie-Howard percaya bahawa dua konsep dalam sains komputer (jenis dan program) adalah bersamaan dengan dua konsep dalam logik (proposisi dan bukti).

Salah satu hasil daripada surat-menyurat ini ialah pembangunan program telah ditingkatkan ke tahap matematik yang ideal, sedangkan sebelum ini orang biasanya menganggap pembangunan program hanyalah kerja kraf. Pembangunan program bukan hanya "menulis kod", ia telah menjadi tindakan membuktikan teorem. Ini memformalkan tingkah laku pembangunan program dan menyediakan cara untuk membuat alasan secara matematik tentang ketepatan program.

Nama surat-menyurat ini berasal daripada dua penyelidik, yang secara bebas menemui surat-menyurat ini. Pada tahun 1934, ahli matematik dan logik Haskell Curry melihat persamaan antara fungsi dalam matematik dan hubungan implikasi dalam logik. Bentuk hubungan implikasi ialah pernyataan "jika-maka" antara dua proposisi.

Diilhamkan oleh pemerhatian Currie, ahli logik matematik William Alvin Howard menemui pada tahun 1969 hubungan yang lebih mendalam antara pengiraan dan logik menunjukkan bahawa: Program komputer sangat mirip dengan bukti logik yang dipermudahkan. Apabila anda menjalankan program komputer, setiap baris kod "dinilai" untuk menghasilkan output. Begitu juga, apabila bekerja pada bukti, anda bermula dengan pernyataan yang kompleks dan kemudian memudahkannya (contohnya, dengan menghapuskan langkah berlebihan atau menggantikan ungkapan kompleks dengan yang lebih mudah) sehingga anda mencapai beberapa kesimpulan - daripada banyak Pernyataan peralihan membawa kepada yang lebih ringkas kenyataan.

Walaupun huraian ini memberikan gambaran kasar tentang maksud surat-menyurat ini, memahami sepenuhnya ia memerlukan mengetahui lebih lanjut tentang apa yang dipanggil oleh saintis komputer sebagai "teori jenis."

Mari kita mulakan dengan paradoks yang terkenal: Terdapat seorang tukang gunting rambut di sebuah kampung yang bercukur untuk dan hanya untuk mereka yang tidak mencukur dirinya sendiri. Jadi adakah tukang gunting rambut ini mencukur dirinya sendiri? Jika jawapannya ya, maka dia tidak boleh mencukur dirinya sendiri (kerana dia hanya bercukur untuk orang yang tidak bercukur sendiri). Jika jawapannya tidak, maka dia mesti mencukur dirinya sendiri (kerana dia mencukur setiap orang yang tidak bercukur sendiri). Ini adalah versi tidak formal paradoks yang ditemui oleh Bertrand Russell ketika dia cuba membentuk asas matematik menggunakan konsep yang dipanggil set. Maksudnya: adalah mustahil untuk menentukan set yang mengandungi semua set yang tidak mengandungi dirinya, dan percanggahan pasti akan berlaku dalam proses ini.

Penyelidikan Russell menunjukkan bahawa untuk mengelakkan paradoks ini, kita boleh menggunakan jenis. Secara kasarnya, jenis adalah kategori yang nilai konkritnya dipanggil objek. Sebagai contoh, jika terdapat jenis Nat yang mewakili nombor asli, maka objeknya ialah 1, 2, 3, dan seterusnya. Penyelidik sering menggunakan titik bertindih untuk menunjukkan jenis objek. Sebagai contoh, untuk nilai jenis integer 7, ia boleh ditulis sebagai "7: Integer". Kita boleh menggunakan fungsi untuk menukar objek jenis A kepada objek jenis B, atau kita boleh menggunakan fungsi untuk menggabungkan dua objek jenis A dan B menjadi objek baharu jenis "A×B".

Jadi, untuk menyelesaikan paradoks ini, salah satu cara adalah dengan melapisi jenis ini supaya ia hanya mengandungi elemen satu tahap di bawah mereka. Kemudian jenis tidak boleh mengandungi dirinya sendiri, yang mengelakkan rujukan diri yang mencipta paradoks di atas.

Dalam dunia teori jenis, proses membuktikan sesuatu kenyataan itu benar mungkin berbeza daripada kebiasaan kita. Jika kita ingin membuktikan bahawa integer 8 adalah genap, maka kunci kepada masalah adalah untuk membuktikan bahawa 8 sebenarnya adalah objek jenis "genap", dan peraturan jenis ini mentakrifkan bahawa unsur-unsur boleh dibahagikan dengan 2. Selepas mengesahkan bahawa 8 boleh dibahagikan dengan 2, kita boleh membuat kesimpulan bahawa 8 ialah "penduduk" jenis "genap".

Currie dan Howard membuktikan bahawa jenis pada asasnya bersamaan dengan proposisi logik. Apabila fungsi "menghuni" jenis tertentu, iaitu, apabila fungsi adalah objek jenis itu, kita boleh membuktikan dengan berkesan bahawa proposisi yang sepadan adalah benar. Oleh itu, fungsi yang mengambil objek jenis A sebagai input dan objek jenis B sebagai output (ditandakan sebagai jenis A → B) mesti sepadan dengan implikasi: "Jika A, maka B." proposisi "Jika hujan, maka tanah basah. "Dalam teori jenis, proposisi ini akan dimodelkan sebagai fungsi jenis "hujan → tanah basah". Kedua-dua perwakilan ini kelihatan berbeza, tetapi secara matematik adalah sama.

Walaupun sambungan ini kelihatan abstrak, ia bukan sahaja mengubah cara pengamal matematik dan sains komputer berfikir tentang kerja mereka, tetapi juga membawa kepada beberapa aplikasi praktikal dalam kedua-dua bidang. Dalam sains komputer, sambungan ini menyediakan asas teori untuk pengesahan perisian, proses memastikan ketepatan perisian. Dengan menerangkan tingkah laku yang diingini dari segi proposisi logik, pembangun program boleh membuktikan secara matematik sama ada program berkelakuan seperti yang diharapkan. Dan sambungan ini juga menyediakan asas teori yang kukuh untuk mereka bentuk bahasa pengaturcaraan berfungsi yang lebih berkuasa.

Dalam bidang matematik, surat-menyurat ini telah menimbulkan alat pembantu bukti, juga dikenali sebagai prover teorem interaktif. Alat perisian ini boleh membantu dalam membina bukti rasmi, contohnya termasuk Coq dan Lean. Dalam Coq, setiap langkah pembuktian pada dasarnya adalah program, dan kesahihan pembuktian disemak melalui algoritma penyemakan jenis. Ahli matematik juga telah menggunakan pembantu bukti (terutamanya pembukti teorem Lean) untuk memformalkan matematik, yang melibatkan mewakili konsep, teorem dan bukti matematik dalam format yang ketat yang boleh disahkan oleh komputer. Ini membolehkan kadangkala bahasa matematik tidak formal diuji oleh komputer.

Penyelidik juga sedang meneroka kemungkinan hasil hubungan antara matematik dan pengaturcaraan ini. Surat-menyurat Curry-Howard asal menyatukan pembangunan program dengan sejenis logik yang dipanggil logik intuisi, tetapi ternyata terdapat banyak lagi jenis logik yang boleh disatukan.

Saintis komputer Cornell University Michael Clarkson berkata: "Dalam abad sejak Currie memperoleh pandangannya, kami terus mencari lebih banyak contoh 'sistem logik X sepadan dengan sistem pengiraan Y.'" Penulis Penyelidikan juga telah mengaitkan pengaturcaraan kepada jenis logik lain, seperti logik linear yang melibatkan konsep "sumber" dan logik modal yang melibatkan konsep kemungkinan dan keperluan.

Dan walaupun surat-menyurat ini membawa nama Curry dan Howard, mereka bukanlah satu-satunya penemu surat-menyurat ini. Ini menunjukkan sifat asas surat-menyurat ini: orang ramai melihatnya berulang kali. Clarkson berkata: "Hubungan mendalam antara pengkomputeran dan logik nampaknya tidak disengajakan

Atas ialah kandungan terperinci Hubungan mendalam antara logik matematik dan kod program komputer: cermin imej antara satu sama lain. Untuk maklumat lanjut, sila ikut artikel berkaitan lain di laman web China PHP!