Seberapa baik detektor penghenti itu?

Apakah ada Mesin Turing yang dapat memutuskan apakah hampir semua Mesin Turing lainnya berhenti?

Misalkan kita memiliki beberapa enumerasi $\mathbb{N} \rightarrow \{M_i\}$ dari mesin Turing, dan beberapa gagasan "ukuran" dari satu set bilangan alami $\| \cdot \|$ , dan kami mendefinisikan:

Karakterisasi apa dari nilai minimum $f$ ada untuk berbeda $\| \cdot \|$? Misalnya, misalkan $\| S \|$adalah limsup dari proporsi angka hingga $k$ yang berada di $S$ . Apakah ada $i$ yang $f(i) = 0$ ?

Ini bukan properti "baik", karena apakah itu benar atau salah bergantung pada penyandian.

Lihat karya David dkk secara asimtotik hampir semua $\lambda$ -terms sangat normal , yang membuktikan apa yang tertulis dalam judul. Namun, makalah ini juga menunjukkan bahwa kebalikannya berlaku untuk SKI-combinators (di mana istilah lambda dapat dimasukkan secara komposisi).

Dalam kalkulus lambda, pengurangan adalah setara dengan langkah mesin Turing, dan normalisasi yang kuat adalah properti yang setiap urutan reduksi akhirnya mencapai bentuk normal - yaitu, tidak ada pengurangan lebih lanjut yang dimungkinkan. (Karena istilah lambda yang diberikan mungkin memiliki banyak reduksi yang valid, normalisasi yang kuat agak seperti mengatakan mesin Turing nondeterministik yang diberikan selalu terhenti.) Jadi fakta bahwa secara asimptotik hampir semua -term sangat normal artinya bahwa dengan probabilitas mendekati 1, mengurangi istilah lambda besar akan selalu mencapai bentuk normal.$\lambda$

Namun, istilah lambda dapat diterjemahkan dengan cara mempertahankan makna menjadi kalkulus kombinasi seperti kombinator SKI (dan sebaliknya), dan dalam kalkulus kombinator asimtotik semua istilah loop.