Bahasa pemrograman untuk perhitungan yang efisien

Tidak mungkin menulis bahasa pemrograman yang memungkinkan semua mesin berhenti pada semua input dan tidak ada yang lain. Namun, sepertinya mudah untuk mendefinisikan bahasa pemrograman seperti itu untuk kelas kompleksitas standar apa pun. Secara khusus, kita dapat mendefinisikan bahasa di mana kita dapat mengekspresikan semua perhitungan yang efisien dan hanya perhitungan yang efisien.

Misalnya, untuk sesuatu seperti : ambil bahasa pemrograman favorit Anda, dan setelah Anda menulis program Anda (sesuai dengan Turing Machine ), tambahkan tiga nilai ke header: integer , dan integer , dan output default . Ketika program dikompilasi, output mesin Turing yang diberikan input ukuran menjalankan on untuk langkah . Jika tidak berhenti sebelum langkah naik, output output default$P$$M'$$c$$k$$d$$M$$x$$n$$M'$$x$$c n^k$$M'$$c n^k$$d$. Kecuali saya salah, bahasa pemrograman ini akan memungkinkan kami untuk mengekspresikan semua perhitungan dalam dan tidak lebih. Namun, bahasa yang diusulkan ini secara inheren tidak menarik.$P$

Pertanyaan saya: apakah ada bahasa pemrograman yang menangkap himpunan bagian dari fungsi yang dapat dihitung (seperti semua fungsi yang dapat dihitung secara efisien) dengan cara yang tidak sepele? Jika tidak, apakah ada alasan untuk ini?

Satu bahasa yang hanya mencoba untuk mengekspresikan perhitungan waktu polinomial adalah kalkulus lambda lunak . Jenis sistem itu berakar pada logika linier. Tesis baru-baru ini membahas kalkulus waktu polinomial, dan memberikan ringkasan yang bagus tentang perkembangan terkini berdasarkan pendekatan ini. Martin Hofmann telah mengerjakan topik ini selama beberapa waktu. Daftar yang lebih tua dari makalah yang relevan dapat ditemukan di sini ; Banyak dari makalahnya berlanjut ke arah ini.

Pekerjaan lain mengambil pendekatan untuk memverifikasi bahwa program tersebut menggunakan sejumlah sumber daya tertentu, menggunakan Jenis Ketergantungan atau Bahasa Majelis yang Diketik .

Namun pendekatan lain didasarkan pada kalkulus formal terbatas sumber daya , seperti varian kalkulus ambien.

Pendekatan ini memiliki properti yang diketik dengan baik oleh program memenuhi beberapa batasan sumber daya yang ditentukan sebelumnya. Batas sumber daya dapat berupa waktu atau ruang, dan umumnya dapat bergantung pada ukuran input.

Pekerjaan awal di bidang ini adalah pada batu yang sangat normal, yang berarti bahwa semua program yang diketik dengan baik berhenti. Sistem F , alias kalkulus lambda polimorfik, sangat normal. Ia tidak memiliki operator titik tetap, namun tetap cukup ekspresif, meskipun saya tidak berpikir kelas kompleksitas yang terkait dengannya. Menurut definisi, setiap kalkulus yang sangat normal mengungkapkan beberapa kelas penghentian perhitungan.

Bahasa pemrograman Charity adalah bahasa fungsional yang cukup ekspresif yang berhenti pada semua input. Saya tidak tahu kelas kompleksitas apa yang bisa diekspresikan, tetapi fungsi Ackermann dapat ditulis dalam Charity.

Lihatlah makalah Guillaume Bonfante yang mengusulkan dua penokohan untuk Logspace dan waktu polinomial menggunakan bahasa pemrograman.

Guillaume Bonfante, Beberapa bahasa pemrograman untuk Logspace dan Ptime, AMAST 2006, LNCS 4019, hlm. 66-80, 2006

Saya juga ingin menyebutkan Teori Kompleksitas Tersirat sebagai pendekatan untuk ini, karena saya telah melihatnya muncul dalam beberapa pertanyaan yang agak terkait. Mengutip jawaban ini oleh Neel Krishnaswami :

Teknik dasarnya adalah mengaitkan kelas kompleksitas dengan subsistem logika linier (yang disebut "logika linier cahaya"), dengan gagasan bahwa cut-elimination untuk sistem logis harus lengkap untuk kelas kompleksitas yang diberikan (seperti LOGSPACE, PTIME, dll). Kemudian melalui Curry-Howard Anda mengeluarkan bahasa pemrograman di mana tepatnya program-program di kelas yang diberikan dapat diekspresikan.

Saya terkejut tidak ada yang menyebutkan rekursi primitif. Dengan membatasi loop terikat (yaitu jumlah iterasi untuk setiap loop harus dihitung sebelum loop dimulai) program yang dihasilkan adalah primitif rekursif, dan karenanya total. Douglas Hofstadter mengusulkan bahasa pemrograman, BLOOP, yang memungkinkan semua dan hanya fungsi rekursif primitif.

Lihat juga Pola bahasa untuk pemrograman PTIME dan karya-karya Japaridze pada aritmatika PTIME misalnya http://arxiv.org/abs/0902.2969