Bagaimana cara menunjukkan dua model komputasi yang setara?

Saya mencari penjelasan tentang bagaimana seseorang dapat membuktikan bahwa dua model perhitungan adalah setara. Saya telah membaca buku-buku tentang masalah ini kecuali bahwa bukti kesetaraan dihilangkan. Saya punya ide dasar tentang apa artinya dua model perhitungan menjadi setara (tampilan automata: jika mereka menerima bahasa yang sama). Apakah ada cara lain untuk berpikir tentang kesetaraan? Jika Anda dapat membantu saya memahami bagaimana membuktikan bahwa model mesin Turing setara dengan kalkulus lambda, itu sudah cukup.

Anda menunjukkan bahwa model mana pun dapat mensimulasikan yang lain, yaitu diberi mesin dalam model A, menunjukkan bahwa ada mesin dalam model B yang menghitung fungsi yang sama. Perhatikan bahwa simulasi ini tidak harus dapat dihitung (tetapi biasanya demikian).

Pertimbangkan, misalnya, pushdown automata dengan dua tumpukan (2-PDA). Dalam pertanyaan lain , simulasi di kedua arah diuraikan. Jika Anda melakukan ini secara formal, Anda akan menggunakan mesin Turing umum (tuple) dan secara eksplisit membuat seperti apa 2-PDA yang sesuai, dan sebaliknya.

Secara formal, simulasi seperti itu mungkin terlihat seperti ini. Membiarkan

$\qquad \displaystyle M = (Q,\Sigma_I,\Sigma_O,\delta,q_0,Q_F)$

menjadi mesin Turing (dengan satu pita). Kemudian,

$\qquad \displaystyle A_M = (Q \cup \{q^*_1,q^*_2\},\Sigma_I,\Sigma_O', \delta', q^*_1, Q_F)$

dengan $\Sigma_O' = \Sigma_O \overset{.}{\cup} \{\$\}$ dan $\delta'$ diberikan oleh

$\quad \displaystyle (q^*_1,a,h_l,h_r) \to_{\delta'} (q^*_1,ah_l,h_r)$ untuk semua$a \in \Sigma_I$ dan$h_r,h_l \in \Sigma_O$ ,
$\quad \displaystyle (q^*_1,\varepsilon,h_l,h_r) \to_{\delta'} (q^*_2,h_l,h_r)$ untuk semua$h_r,h_l \in \Sigma_O$ ,
$\quad \displaystyle (q^*_2,\varepsilon,h_l,h_r) \to_{\delta'} (q^*_2,\varepsilon,h_lh_r)$ untuk semua$h_r,h_l \in \Sigma_O$ dengan$h_l \neq \$$ ,
$\quad \displaystyle (q^*_2,\varepsilon,\$,h_r) \to_{\delta'} (q_0,\$,h_r)$ untuk semua$h_r \in \Sigma_O$ ,
$\quad \displaystyle (q,\varepsilon,h_l,h_r) \to_{\delta'} (q',\varepsilon,h_la) \iff (q,h_r) \to_\delta (q',a,L)$ untuk semua$q \in Q$ dan$h_l \in \Sigma_O$ ,
$\quad \displaystyle (q,\varepsilon,\$,h_r) \to_{\delta'} (q',\$,\square a) \iff (q,h_r) \to_\delta (q',a,L)$ untuk semua$q \in Q$ ,
$\quad \displaystyle (q,\varepsilon,h_l,h_r) \to_{\delta'} (q',ah_l,\varepsilon) \iff (q,h_r) \to_\delta (q',a,R)$ untuk semua$q \in Q, h_l \in \Sigma_O'$ ,
$\quad \displaystyle (q,\varepsilon,h_l,\$) \to_{\delta'} (q,h_l,\square\$)$ untuk semua$q \in Q$ dan$h_l \in \Sigma_O'$ , dan
$\quad \displaystyle (q,\varepsilon,h_l,h_r) \to_{\delta'} (q',h_l,a) \iff (q,h_r) \to_\delta (q',a,N)$ untuk semua$q \in Q,h_l\in\Sigma_O'$

adalah 2-PDA setara. Di sini, kita mengasumsikan bahwa mesin Turing menggunakan $\square \in \Sigma_O$ sebagai simbol kosong, kedua tumpukan dimulai dengan marker $\$\notin \Sigma_O$ (yang tidak pernah dihapus) dan $(q,a,h_l,h_r) \to_{\delta'} (q',l_1\dots l_i,r_1\dots r_j)$ berarti bahwa $A_M$ mengkonsumsi masukan $a$ , switch negara dari$q$ to$q'$ dan memperbarui tumpukan seperti:

^{[ sumber ]}

Tetap untuk menunjukkan bahwa $A_M$ memasuki keadaan akhir pada $x \in \Sigma_I^*$ jika dan hanya jika $M$ melakukannya. Ini cukup jelas dengan konstruksi; secara formal, Anda harus menerjemahkan penerimaan yang berjalan pada $M$ ke dalam penerimaan yang berjalan pada $A_M$ dan sebaliknya.

Pada awal Sistem Komunikasi dan Seluler: Pi-Calculus oleh Robin Milner, ada pengantar tentang automata dan bagaimana mereka dapat mensimulasikan satu sama lain sehingga mereka tidak dapat dibedakan: Bisimulasi . (bdk Bisimulasi di wikipedia)

Saya tidak ingat dengan baik, saya harus membaca ulang bab ini, tetapi ada masalah dengan simulasi dan bisimulasi yang membuat mereka tidak cukup untuk persamaan komputasi.

Dengan demikian Robin Milner memperkenalkan Pi-Calculus-nya dan memaparkannya untuk sisa buku ini.

Pada akhirnya, dalam buku terakhirnya The Space and Motion of Communicating Agents , Anda dapat melihat Robin Milner's Bigraphs. Mereka dapat memodelkan Automata, Petri nets, Pi-Calculus dan metodologi komputasi lainnya.

Sejauh yang saya tahu, satu-satunya (atau paling tidak paling umum) cara untuk melakukan ini adalah membandingkan bahasa yang diterima mesin / model. Itulah inti teori Automata: ia mengambil konsep yang tidak jelas dari suatu masalah atau algoritma dan mengubahnya menjadi himpunan matematis konkret (yaitu bahasa) yang dapat kita pikirkan.

Cara termudah untuk melakukan ini adalah, diberi mesin / fungsi sewenang-wenang dari satu model, untuk membangun mesin dari model kedua yang menghitung bahasa yang sama. Kemungkinannya adalah Anda akan menggunakan induksi dalam panjang ekspresi, status dalam mesin, aturan dalam tata bahasa, dll.

Saya belum pernah melihat ini dilakukan dengan Lambda dan TM (walaupun saya 99% yakin itu mungkin), tapi saya pasti melihat hal semacam ini untuk membuktikan kesetaraan NFA dan ekspresi Reguler. Pertama Anda menunjukkan NFA yang dapat menerima atom apa pun, kemudian menggunakan induksi, Anda membuat NFA yang menerima penyatuan / penggabungan / Kleene-bintang dari setiap NFA yang lebih kecil.

Kemudian Anda melakukan yang sebaliknya, untuk menemukan RE untuk NFA apa pun.