Apakah ada gagasan yang masuk akal tentang algoritma aproksimasi untuk masalah yang tidak dapat ditentukan?

48

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.

Timothy Chow
sumber
3
..ingat saya tentang teori Interpretasi Abstrak.
Jagadish
1
[Bersamaan dengan komentar Jagadish]: Anda dapat melihat kursus MIT 16.399: Interpretasi Abstrak . Khususnya, Kuliah 3 mungkin berguna untuk kasus Anda.
MS Dousti
6
Ukuran yang jelas yang Anda mungkin tidak akan Anda sukai adalah dengan hanya memesan berbagai solusi parsial sesuai dengan domain mereka (yaitu, set input tempat mereka bekerja). Untuk apa Anda ingin menggunakan ukuran?
Andrej Bauer
3
@Andrej: Biarkan saya menjawab pertanyaan Anda secara tidak langsung. Dalam bidang masalah NP-hard, kami kadang-kadang memiliki hasil yang sangat bagus dari bentuk, "rasio perkiraan ini-dan-itu dapat dicapai, dan perbaikan lebih lanjut tidak mungkin kecuali P = NP." Mampu membuktikan hasil analog untuk masalah menarik yang tidak dapat ditentukan akan lebih baik. Ini akan memberi kita beberapa pengertian apakah ada beberapa penghalang intrinsik untuk kemajuan lebih lanjut.
Timothy Chow
mengusulkan konsep "quasialgorithms" dengan beberapa penelitian di daerah tersebut
vzn

Jawaban:

30

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.

Neel Krishnaswami
sumber
6

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".

Sariel Har-Peled
sumber
2

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.

Mn<nϵϵp>0

ρnρn<n

Ted
sumber