Masalah-masalah tertentu diketahui tidak dapat diputuskan, tetapi masih mungkin untuk membuat beberapa kemajuan dalam memecahkannya. Misalnya, masalah penghentian tidak dapat diputuskan, tetapi kemajuan praktis dapat dibuat pada pembuatan alat untuk mendeteksi potensi loop tak terbatas dalam kode Anda. Masalah ubin sering kali tidak dapat dipastikan (mis., Apakah ubin polyomino ini berbentuk persegi panjang?) Tetapi sekali lagi dimungkinkan untuk meningkatkan keadaan seni di bidang ini.
Yang saya bertanya-tanya adalah apakah ada metode teoretis yang layak untuk mengukur kemajuan dalam memecahkan masalah yang tidak dapat ditentukan, yang menyerupai alat teoritis yang telah dikembangkan untuk mengukur kemajuan pada masalah NP-hard. Atau sepertinya kita terjebak dengan penilaian ad hoc, aku-tahu-kemajuan-kapan-aku-lihat-berapa banyak terobosan tertentu memajukan pemahaman kita tentang masalah yang tidak dapat diputuskan?
Sunting : Ketika saya memikirkan pertanyaan ini, saya sadar bahwa mungkin kompleksitas parameter mungkin relevan di sini. Masalah yang tidak dapat diputuskan dapat menjadi dapat ditentukan jika kita memperkenalkan parameter dan memperbaiki nilai parameter. Saya tidak yakin apakah pengamatan ini ada gunanya.
Jawaban:
Dalam hal masalah penghentian, jawabannya adalah "belum". Alasannya adalah bahwa metode logis standar untuk mengkarakterisasi seberapa keras bukti terminasi suatu program (misalnya, analisis ordinal) cenderung kehilangan terlalu banyak struktur kombinatorial dan / atau teori angka.
Ini berarti bahwa tidak ada hubungan yang rapi antara kekuatan teoritik-bukti dari metalogik tempat Anda menunjukkan penghentian (misalnya, ini sangat penting dalam penulisan ulang teori) dan fungsi-fungsi yang teknik seperti sintesis fungsi-peringkat dapat menunjukkan penghentian untuk .
Untuk kalkulus lambda, kami memiliki karakterisasi yang tepat tentang terminasi dalam hal kemampuan mengetik: istilah lambda sangat normal jika dan hanya jika itu dapat diketik di bawah disiplin jenis persimpangan. Tentu saja, ini berarti bahwa inferensi tipe penuh untuk tipe persimpangan tidak mungkin dilakukan, tetapi ini juga dapat memberikan cara untuk membandingkan algoritma inferensi parsial.
sumber
Dari pembicaraan yang mengesankan dari seseorang yang menerapkan algoritma yang memecahkan masalah yang tidak dapat diputuskan: "Dibutuhkan 2-3 detik untuk semua input yang saya coba".
sumber
Ini menjawab judul pertanyaan lebih dari isinya, tetapi Anda juga dapat mempertimbangkan "perkiraan" dari masalah penghentian sebagai algoritma yang akan memberi Anda jawaban yang benar pada program "hampir semua".
Gagasan tentang "hampir semua" program hanya masuk akal jika model perhitungan Anda optimal (dalam arti yang sama untuk kompleksitas Kolmogorov ), untuk menghindari situasi di mana sebagian besar program Anda sepele.
sumber