Jak wykazać, że dwa modele obliczeń są równoważne?

Szukam wyjaśnienia, w jaki sposób można udowodnić, że dwa modele obliczeń są równoważne. Czytałem książki na ten temat, z tym wyjątkiem, że pominięto dowody równoważności. Mam podstawowe pojęcie o tym, co to znaczy, że dwa modele obliczeń są równoważne (widok automatów: jeśli akceptują te same języki). Czy istnieją inne sposoby myślenia o równoważności? Jeśli pomożesz mi zrozumieć, jak udowodnić, że model maszyny Turinga jest równoważny rachunkowi lambda, byłoby to wystarczające.

Pokazujesz, że każdy model może symulować drugi, którym jest maszyna w modelu A, pokazujesz, że istnieje maszyna w modelu B, która oblicza tę samą funkcję. Zauważ, że ta symulacja nie musi być obliczalna (ale zwykle jest).

Rozważmy na przykład automaty wypychające z dwoma stosami (2-PDA). W innym pytaniu przedstawiono symulacje w obu kierunkach. Jeśli zrobiłbyś to formalnie, wziąłbyś ogólną maszynę Turinga (krotkę) i wyraźnie skonstruowałbyś, co odpowiadałby 2-PDA, i odwrotnie.

Formalnie taka symulacja może wyglądać następująco. Pozwolić

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

być maszyną Turinga (z jedną taśmą). Następnie,

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

z i podane przez$\Sigma_O' = \Sigma_O \overset{.}{\cup} \{\$\}$$\delta'$

$\quad \displaystyle (q^*_1,a,h_l,h_r) \to_{\delta'} (q^*_1,ah_l,h_r)$ dla wszystkich i , dla wszystkich , dla wszystkich z , dla wszystkich , ∈ Ď I$a \in \Sigma_I$$h_r,h_l \in \Sigma_O$
$\quad \displaystyle (q^*_1,\varepsilon,h_l,h_r) \to_{\delta'} (q^*_2,h_l,h_r)$$h_r,h_l \in \Sigma_O$
$\quad \displaystyle (q^*_2,\varepsilon,h_l,h_r) \to_{\delta'} (q^*_2,\varepsilon,h_lh_r)$$h_r,h_l \in \Sigma_O$$h_l \neq \$$
$\quad \displaystyle (q^*_2,\varepsilon,\$,h_r) \to_{\delta'} (q_0,\$,h_r)$$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)$ q ∈ Q h l ∈ Σ Odla wszystkich i , dla wszystkich , dla wszystkich , dla wszystkich i oraz dla wszystkich$q \in Q$$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)$$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)$$q \in Q, h_l \in \Sigma_O'$
$\quad \displaystyle (q,\varepsilon,h_l,\$) \to_{\delta'} (q,h_l,\square\$)$$q \in Q$$h_l \in \Sigma_O'$
$\quad \displaystyle (q,\varepsilon,h_l,h_r) \to_{\delta'} (q',h_l,a) \iff (q,h_r) \to_\delta (q',a,N)$$q \in Q,h_l\in\Sigma_O'$

jest równoważnym 2-PDA. Zakładamy, że maszyna Turinga używa jako pusty symbol, oba stosy zaczynają się od znacznika (który nigdy nie jest usuwany) i oznacza, że zużywa wejście , przełącza stany z na i aktualizuje stosy w następujący sposób:$\square \in \Sigma_O$$\$\notin \Sigma_O$$(q,a,h_l,h_r) \to_{\delta'} (q',l_1\dots l_i,r_1\dots r_j)$$A_M$$a$$q$$q'$

^{[ źródło ]}

Pozostaje pokazać, że wchodzi w stan końcowy na tylko i tylko wtedy, gdy zrobi. Jest to całkiem jasne z konstrukcji; formalnie musisz przełożyć akceptowanie przebiegów na na akceptowanie przebiegów na i odwrotnie.$A_M$$x \in \Sigma_I^*$$M$$M$$A_M$

Na początku systemów komunikacyjnych i mobilnych: Pi-Calculus autorstwa Robina Milnera znajduje się wprowadzenie do automatów i sposobów ich wzajemnej symulacji, aby nie można było ich rozróżnić: bisimulacja . (por. Bisimulation na wikipedii)

Nie pamiętam dobrze, powinienem ponownie przeczytać ten rozdział, ale wystąpiły problemy z symulacją i bisimulacją, które sprawiły, że nie były wystarczające do równoważności obliczeniowych.

W ten sposób Robin Milner przedstawia swoje Pi-Calculus i ujawnia je do końca książki.

Ostatecznie w jego ostatniej książce The Space and Motion of Communicating Agents można było obejrzeć Bigraphs Robina Milnera. Mogą modelować Automaty, sieci Petriego, Pi-Calculus i inne metodologie obliczeniowe.

O ile mi wiadomo, jedynym (lub przynajmniej najczęstszym) sposobem na to jest porównanie języków akceptowanych przez maszyny / modele. Taki jest sens teorii automatów: przyjmuje niejasną koncepcję problemu lub algorytmu i zamienia ją w konkretny zestaw matematyczny (tj. Język), o którym możemy myśleć.

Najłatwiej to zrobić, biorąc pod uwagę dowolną maszynę / funkcję z jednego modelu, aby zbudować maszynę z drugiego modelu, który oblicza ten sam język. Szanse są takie, że użyjesz indukcji długości wyrażenia, stanów w maszynie, reguł gramatyki itp.

Nie widziałem tego zrobionego z Lambda i TM (chociaż jestem w 99% pewien, że to możliwe), ale zdecydowanie widziałem tego rodzaju rzeczy, aby udowodnić równoważność NFA i wyrażeń regularnych. Najpierw pokazujesz NFA, który może zaakceptować dowolny atom, a następnie za pomocą indukcji tworzysz NFA, które akceptują zjednoczenie / konkatenację / gwiazdę Kleene wszelkich mniejszych NFA.

Następnie postępujesz odwrotnie, aby znaleźć RE dla dowolnego NFA.