Apakah masalah penghentian dapat diputuskan untuk program murni pada komputer yang ideal?

Cukup sederhana untuk memahami mengapa masalah penghentian tidak dapat diputuskan untuk program tidak murni (yaitu, yang memiliki I / O dan / atau negara bagian bergantung pada negara mesin-global); tetapi secara intuitif, tampaknya program murni berhenti pada komputer yang ideal akan dapat ditentukan melalui misalnya analisis statis.

Apakah ini yang sebenarnya terjadi? Jika tidak, apa sajakah contoh tandingan atau makalah yang menyangkal klaim ini?

Berikut ini adalah bukti ketidakpastian dengan pengurangan dari masalah Putus.

Reduksi: Diberikan mesin dan input x , buat Mesin Turing H baru yang tidak membaca input apa pun, tetapi tuliskan M dan x pada kaset dan simulasikan M pada x hingga M berhenti.$M$$x$$H$$M$$x$$M$$x$$M$

Perilaku mesin baru ini tidak tergantung pada pita input, sehingga merupakan mesin Turing murni yang hanya dapat digunakan analisis statis. Jika analisis statis cukup, maka itu dapat menunjukkan apakah H berhenti, yang akan menunjukkan apakah M berhenti pada x , yang akan memecahkan masalah penghentian untuk mesin yang tidak murni, yang kami tahu tidak dapat diputuskan, dan karena itu masalah Anda juga tidak dapat diputuskan.$H$$H$$M$$x$

Tidak bukan, dan terlebih lagi itu tidak bergantung pada I / O.

Contoh tandingan sederhana: tulis sebuah program untuk menemukan angka ganjil yang sempurna (ini adalah masalah terbuka: kita belum tahu apakah ada) - tidak mengambil input apa pun dan tidak melakukan tugas yang tidak murni ; mungkin berhenti ketika menemukan satu, atau dapat bekerja tanpa batas (dalam kasus nomor seperti itu tidak ada). Sekarang jika analisis statis cukup kuat untuk menentukan kasus penghentian itu akan digunakan untuk menjawab ini (dan banyak lagi pertanyaan) di mana penghentian akan berarti keberadaan positif dari nomor tersebut dan tidak berhenti akan berarti tidak ada nomor tersebut, tetapi sayangnya analisis statis tidak begitu kuat.

Bukti klasik dengan diagonalisasi adalah mesin murni , tidak hanya itu adalah Mesin Turing murni, tetapi tidak bergantung pada "Masalah Terbuka".

Sebagai contoh, sebuah mesin Turing yang mengeksekusi dugaan Collatz memiliki status penghentian yang tidak diketahui, tetapi itu bergantung pada ketidaktahuan kita tentang dugaan Collatz, suatu hari kita dapat membuktikan bahwa Collatz benar dan kemudian kita akan dapat memutuskan status penghentian dugaan tersebut. (Entah untuk beberapa input tidak berhenti, atau Selalu berhenti).

Jadi dugaan Collatz sudah bisa menjawab pertanyaan Anda (setidaknya untuk sementara), tetapi itu bergantung pada sesuatu yang kita tidak tahu . Alih-alih, bukti klasik adalah masalah yang sudah dipecahkan: kita sudah tahu itu tidak dapat dipastikan .

Sebagai catatan, bukti standar dari keraguan tentang masalah penghentian bergantung pada gagasan yang sama dengan quines: bahwa mungkin untuk menulis sebuah program yang sub-termnya dievaluasi ke kode sumber untuk keseluruhan program. Kemudian, jika ada fungsi haltsyang, diberikan kode sumber untuk suatu program, dikembalikan Benar jika program itu berhenti pada semua input dan Salah sebaliknya, ini akan menjadi program hukum:

prog() = if halts "prog" then prog() else ()

di mana "prog"akan ada ekspresi yang dievaluasi ke kode sumber untuk prog; Namun, Anda dapat dengan cepat melihatnyaprog berhenti (untuk semua input) jika tidak berhenti, yang merupakan kontradiksi. Tidak ada dalam bukti ini bergantung pada I / O dengan cara apa pun (apakah Anda memerlukan I / O untuk menulis quine?).

Omong-omong, Anda mungkin ingin melihat ke "I / O berbasis dialog" untuk bukti lebih lanjut bahwa I / O sepenuhnya tidak relevan dengan masalah Anda (pada dasarnya, program yang I / O dapat dikurangi menjadi program yang menerima input sebagai (eksplisit) argumen fungsional dan mengembalikan output sebagai hasil tambahan (eksplisit) dalam bahasa malas). Sayangnya, saya tidak dapat menemukan halaman yang masuk akal, tidak bias (atau pro-dialog) di web saat ini.