Apa batas-batas pemrograman fungsional total?

Apa keterbatasan pemrograman fungsional total? Ini bukan Turing-complete, tetapi masih mendukung sebagian besar dari program yang mungkin. Apakah ada konstruksi penting yang bisa Anda tulis dalam bahasa Turing-lengkap, tetapi tidak dalam bahasa fungsional total?

Dan apakah benar mengatakan bahwa program yang ditulis dalam bahasa fungsional total dapat sepenuhnya dianalisis secara statis, sementara analisis statis dalam bahasa lengkap Turing dibatasi oleh hal-hal seperti masalah penghentian? Dengan itu saya tidak bermaksud bahwa dalam bahasa fungsional total semuanya dapat ditentukan secara statis, karena beberapa hal hanya diketahui pada saat runtime, tetapi maksud saya bahwa dalam teori, program yang ditulis dalam bahasa pemrograman fungsional total yang ideal, dapat dianalisis sehingga semua yang secara teori bisa ditentukan secara statis dapat ditentukan secara statis. Atau masih ada masalah yang tidak dapat dipastikan mewarisi dalam bahasa fungsional total yang membuat analisis statis tidak lengkap? Beberapa masalah akan selalu tidak dapat diputuskan, tidak peduli dalam bahasa apa mereka ditulis, tetapi saya tertarik dengan masalah yang mewarisi bahasa tersebut,

Itu tergantung pada bahasa fungsional total .

Jawaban ini terdengar seperti penghalang, tetapi tidak ada yang lebih spesifik yang dapat dikatakan. Setelah semua, pertimbangkan program penting apa pun yang Anda tertarik. Tulis program dalam bahasa lengkap Turing favorit Anda untuk menyelesaikannya. Karena masalah dapat diputuskan, program Anda akan berhenti pada semua input.

(Bisa dibilang, masalah yang tidak dapat diputuskan dapat memiliki program yang menarik, tetapi tidak sedemikian rupa sehingga orang dapat menggunakannya, karena mereka tidak akan pernah bisa menunggu cukup lama untuk mengetahui jawabannya.)

Sekarang, tentukan bahasa baru sehingga hanya memiliki satu program input yang valid: program yang baru saja Anda tulis, dengan semantik yang sama seperti sebelumnya. Ini tentu total, karena semua input ke semua program yang tertulis di dalamnya (yang hanya ada satu) selalu berakhir.

Trik murah ini sebenarnya berguna: bahasa Coq , misalnya, adalah bahasa fungsional total karena tidak ada tanda centang program kecuali ada bukti yang diakhiri. (Jika Anda mengesampingkan persyaratan itu, itu akan menjadi Turing-lengkap, jadi satu-satunya kendala adalah menemukan bukti penghentian.)

Saya tidak yakin apa yang Anda maksud dengan "segala sesuatu yang secara teori dapat ditentukan secara statis dapat ditentukan secara statis"; kedengarannya benar secara tautologis. Meskipun demikian, total bahasa pada dasarnya tidak mudah untuk dianalisis; Anda tahu bahwa tidak ada yang menyimpang, yang merupakan fakta berguna, tetapi hubungan antara input dan output masih kompleks. (Secara khusus, masih ada banyak kemungkinan input yang tak terhingga, sehingga Anda tidak dapat mencoba semuanya secara menyeluruh, bahkan secara teori.)

Apa keterbatasan pemrograman fungsional total? Ini bukan Turing-complete, tetapi masih mendukung sebagian besar dari program yang mungkin. Apakah ada konstruksi penting yang bisa Anda tulis dalam bahasa Turing-lengkap, tetapi tidak dalam bahasa fungsional total?

$L$$L$$L$

1. $L$$L$$L$$L$konsisten. Inilah yang dikesampingkan oleh teorema Goedel, dengan asumsi Anda dapat melakukan aritmatika. Jadi kita tahu bahwa kita tidak bisa menulis penerjemah mandiri dalam bahasa fungsional total.

2. Sisi lain dari ini adalah batas-batas pada daya ekspresif dari total bahasa pada dasarnya adalah batas-batas pada daya ekspresif matematika itu sendiri . Misalnya, fungsi yang dapat didefinisikan dalam Coq (asisten bukti) adalah fungsi yang dapat dibuktikan menggunakan ZFC, dengan banyak kardinal yang tidak dapat diakses. Jadi pada dasarnya setiap fungsi yang Anda dapat membuktikan total kepuasan seorang matematikawan yang bekerja dapat didefinisikan dalam Coq.

3. Sisi lain dari sisi lain adalah matematika itu sulit! Jadi tidak ada pengertian yang mudah di mana bahasa total "sepenuhnya dapat dianalisis" - bahkan jika Anda tahu bahwa suatu fungsi berakhir, Anda mungkin masih harus melakukan banyak pekerjaan kreatif untuk membuktikan bahwa ia memiliki properti yang Anda inginkan. Misalnya, hanya mengetahui bahwa fungsi dari daftar ke daftar adalah total, tidak membuat Anda terlalu jauh dalam membuktikan bahwa itu adalah fungsi penyortiran ....