Teori yang mencirikan kelas kompleksitas komputasi

Saat membaca makalah " Sebuah teori aplikatif untuk FPH " Anda dapat menemukan bagian berikut:

Mempertimbangkan teori yang mengkarakterisasi kelas kompleksitas komputasi, ada tiga pendekatan berbeda:

• dalam satu, fungsi yang dapat didefinisikan dalam teori adalah "otomatis" dalam kelas kompleksitas tertentu. Dalam akun seperti itu, sintaksis harus dibatasi untuk menjamin bahwa seseorang tetap berada di kelas yang sesuai. Ini menghasilkan, secara umum, dalam masalah bahwa definisi fungsi tertentu tidak berfungsi lagi, bahkan jika fungsi tersebut berada dalam kelas kompleksitas yang sedang dipertimbangkan.
• Dalam akun kedua, logika yang mendasarinya dibatasi.
• Dalam akun ketiga, seseorang tidak membatasi sintaksis, secara umum, memungkinkan untuk menuliskan "istilah fungsi" untuk fungsi sewenang-wenang (rekursif parsial), atau logika, tetapi hanya untuk istilah fungsi yang termasuk dalam kelas kompleksitas yang dipertimbangkan. , seseorang dapat membuktikan bahwa mereka memiliki properti karakteristik tertentu, biasanya, properti yang “terbukti total”. Sementara istilah fungsi, menurut kerangka sintaksis yang mendasari, mungkin memiliki karakter komputasi langsung, yaitu, sebagai istilah , logika yang digunakan untuk membuktikan properti karakteristik mungkin klasik.$\lambda$

Pertanyaan saya menyangkut referensi yang dapat sebagai pengantar tiga pendekatan yang disebutkan di atas. Dalam bagian ini kita melihat karakterisasi hanya untuk pendekatan, tetapi apakah ini memiliki nama yang diterima secara umum?

Saya pikir pendekatan pertama, pendekatan aritmatika terbatas , adalah pendekatan yang paling populer dan dipelajari dengan baik. Nama dibatasi aritmatika menunjukkan penggunaan subsistem lemah arano kosmetik Peano, di mana induksi dibatasi untuk formula dengan kuantifier terbatas. Saya sudah merangkum ide utama di balik pendekatan ini dalam posting ini . Referensi terbaru yang sangat baik tentang aritmatika terbatas adalah buku karya Cook dan Nguyen, yang konsepnya tersedia secara gratis.

Pendekatan kedua menggunakan logika linier dan subsistemnya seperti yang disebutkan oleh Kaveh, yang saya tidak tahu banyak tentangnya.

Saya belum pernah mendengar tentang pendekatan ketiga meskipun saya sedang mengerjakan aritmatika terbatas. Tetapi kedengarannya agak aneh bagi saya karena tanpa beberapa bentuk pembatasan sintaksis atau logis, bagaimana kemudian teori mencirikan kelas kompleksitas?

Pendekatan ketiga yang disebutkan dalam makalah terkait mengacu pada kerangka teori aplikatif terikat, yang merupakan subsistem dari teori Feferman tentang Matematika Eksplisit seperti halnya teori Aritmatika Terikat adalah subsistem Aritmatika Peano (atau ekstensi dengan urutan lebih tinggi). Teori-teori ini mengandung kalkulus lambda penuh (atau lebih tepatnya logika kombinatorik) dan karenanya memiliki istilah yang menunjukkan semua fungsi yang dapat dihitung. Mereka juga memiliki predikat$W$menunjukkan set kata-kata biner. Kekuatan teori terutama ditentukan oleh aksioma tentang apa$W$itu mengandung. Cara mengkarakterisasi kelas kompleksitas$C$ oleh teori $T$ adalah sebagai berikut:

• Untuk suatu fungsi $f$ ada sebuah istilah $t_f$ seperti yang $T$ terbukti $\forall x. W(x) \to W(t_f(x))$ jika dan hanya jika $f$ ada di $C$.

Mereka berasal dari karya Thomas Strahm, khususnya makalah-makalah berikut:

Thomas Strahm. Teori dengan penerapan sendiri dan kompleksitas komputasi, Informasi dan Komputasi 185, 2003, hlm. 263-297. http://dx.doi.org/10.1016/S0890-5401(03)00086-5

Thomas Strahm. Karakterisasi bukti-teoretis dari fungsional yang layak dasar, Theoretical Computer Science 329, 2004, hlm. 159-176. http://dx.doi.org/10.1016/j.tcs.2004.08.009

Saya tidak benar-benar tahu apakah itu mewakili wilayah tersebut (karena ketidakbiasaan saya secara umum tentang hal itu), tetapi karya Giorgi Japaridze tentang logika komputabilitas merupakan pendekatan kedua.