Teknik bukti terkait korespondensi Curry-Howard

Saya mencari sumber tentang gagasan formal tentang program. Ini tampaknya terkait erat dengan korespondensi Curry-Howard, tetapi orang juga bisa melacak ini kembali ke Mesin Universal Turing dan kemampuannya untuk membaca deskripsi dan input dari setiap TM.

Ketika membaca tentang koresponden Curry-Howard, saya merasa bahwa keutamaan UTM-s dapat merusak penelitian pada program-program dengan kesimpulan unik bahwa program apa pun dapat direduksi menjadi simbol, status, dan aturan. Apakah ada pendekatan yang berlawanan, di mana sistem komputasi tingkat tinggi didefinisikan dan diperiksa? Apa sumber daya yang bagus tentang itu?

Apa yang Anda inginkan ada, dan merupakan bidang penelitian yang sangat besar: ini adalah seluruh teori bahasa pemrograman.

Secara longgar, Anda dapat melihat komputasi dengan dua cara. Anda bisa memikirkannya mesin , atau Anda bisa memikirkan bahasa .

Sebuah mesin pada dasarnya semacam kontrol terbatas yang ditambah dengan beberapa (mungkin tidak terbatas) memori. Inilah sebabnya mengapa kelas pengantar TOC beralih dari automata terbatas ke automata pushdown ke mesin Turing --- setiap kelas mengambil kontrol terbatas dan menambahkan lebih banyak memori ke dalamnya. (Saat ini, kontrol terbatas seringkali lebih terbatas, seperti pada model rangkaian.) Yang penting adalah bahwa kontrol terbatas diberikan di depan, dan sekaligus.

Sebuah bahasa adalah cara menentukan seluruh keluarga kontrol, dengan cara komposisi. Anda memiliki formulir primitif untuk kontrol dasar, dan operator untuk membangun kontrol yang lebih besar dari yang lebih kecil. Bahasa primordial, lambda-calculus, sebenarnya menentukan tidak apa pun selain kontrol - satu-satunya hal yang dapat Anda definisikan adalah abstraksi fungsi, aplikasi, dan referensi variabel.

$snm$ teorema pada dasarnya adalah bukti bahwa mesin Turing dapat mengimplementasikan abstraksi fungsi dan aplikasi, dan pengkodean Gereja menunjukkan bahwa lambda-calculus dapat menyandikan data. Tetapi ada konten nontrivial dalam kedua teorema ini, dan karenanya Anda tidak boleh membuat kesalahan dengan berpikir bahwa dua cara memahami komputasi adalah sama.

Para peneliti dalam kompleksitas dan algoritma biasanya menganggap mesin sebagai hal yang mendasar, karena mereka tertarik pada biaya dan hasil kelayakan . Untuk sedikit melebih-lebihkan, pertanyaan dasar penelitian yang mereka miliki adalah:

Apa mesin paling tidak kuat yang dapat memecahkan masalah tertentu?

Peneliti bahasa menganggap bahasa sebagai hal yang mendasar, karena kami tertarik pada hasil ekspresif dan ketidakmungkinan . Dengan pernyataan yang sama, pertanyaan dasar penelitian kami adalah:

Bahasa apa yang paling ekspresif yang mengesampingkan jenis perilaku buruk tertentu?

Sebagai tambahan, perhatikan bagaimana dua barang yang masing-masing jenis nilai teoretis secara langsung bertentangan! Kerja bagus dalam algoritma dan kompleksitas memungkinkan Anda memecahkan masalah yang lebih sulit, menggunakan lebih sedikit sumber daya. Kerja bagus dalam bahasa memungkinkan pemrogram melakukan lebih banyak hal, sementara melarang lebih banyak perilaku buruk. (Konflik ini pada dasarnya mengapa penelitian sulit.)

Sekarang, Anda mungkin bertanya mengapa lebih banyak tipe Teori A tidak menggunakan bahasa, atau mengapa lebih banyak peneliti Teori B tidak menggunakan mesin. Alasannya muncul dari bentuk pertanyaan penelitian dasar.

Perhatikan bahwa pertanyaan penelitian dasar bergaya dalam algoritma / kompleksitas adalah pertanyaan batas bawah - Anda ingin tahu bahwa Anda memiliki solusi terbaik, dan bahwa tidak ada cara yang mungkin untuk melakukan yang lebih baik, tidak peduli seberapa pintar Anda. Definisi bahasa memperbaiki cara komposisi program , dan jadi jika Anda membuktikan bahwa batas bawah dengan model bahasa, maka Anda mungkin dibiarkan dengan pertanyaan apakah mungkin tidak mungkin melakukan lebih baik jika Anda memperluas bahasa Anda dengan beberapa fitur baru. Model mesin memberi Anda kontrol penuh dalam sekali jalan, dan Anda tahu segala sesuatu yang dapat dilakukan mesin sejak awal.

Tetapi spesifikasi mesin adalah hal yang salah untuk mengatakan hal-hal menarik tentang memblokir perilaku buruk. Sebuah mesin memberi Anda kendali penuh di muka, tetapi mengetahui bahwa satu program tertentu baik-baik saja atau buruk tidak membantu Anda ketika Anda ingin memperpanjang atau menggunakannya sebagai subrutin - seperti yang dikatakan epigram Perlis, "Setiap program adalah bagian dari beberapa program lain dan jarang cocok. " Karena peneliti bahasa tertarik untuk mengatakan hal-hal tentang seluruh kelas program, bahasa jauh lebih cocok untuk tujuan.