¿Cómo mostrar dos modelos de cálculo equivalentes?

Estoy buscando una explicación sobre cómo se podría probar que dos modelos de cálculo son equivalentes. He estado leyendo libros sobre el tema, excepto que se omiten las pruebas de equivalencia. Tengo una idea básica sobre lo que significa que dos modelos de computación sean equivalentes (la vista de autómatas: si aceptan los mismos idiomas). ¿Hay otras formas de pensar acerca de la equivalencia? Si pudiera ayudarme a comprender cómo demostrar que el modelo de máquina de Turing es equivalente al cálculo lambda, eso sería suficiente.

Muestras que cualquiera de los modelos puede simular al otro, que tiene una máquina en el modelo A, muestra que hay una máquina en el modelo B que calcula la misma función. Tenga en cuenta que esta simulación no tiene que ser computable (pero generalmente lo es).

Considere, por ejemplo, autómatas pushdown con dos pilas (2-PDA). En otra pregunta , se resumen las simulaciones en ambas direcciones. Si hiciera esto formalmente, tomaría una máquina de Turing general (una tupla) y construiría explícitamente cuál sería el 2-PDA correspondiente, y viceversa.

Formalmente, tal simulación puede verse así. Dejar

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

ser una máquina de Turing (con una cinta). Luego,

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

$\Sigma_O' = \Sigma_O \overset{.}{\cup} \{\$\}$$\delta'$

$\quad \displaystyle (q^*_1,a,h_l,h_r) \to_{\delta'} (q^*_1,ah_l,h_r)$$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 \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'$

$\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$ a $q'$ y actualiza las pilas así:

^{[ fuente ]}

Queda por demostrar que $A_M$ entra en un estado final en $x \in \Sigma_I^*$ si y solo si $M$lo hace Esto es bastante claro por construcción; formalmente, tienes que traducir aceptando carreras en$M$ en aceptar carreras en $A_M$ y viceversa.

Al comienzo de los sistemas de comunicación y móviles: el cálculo Pi de Robin Milner, hay una introducción sobre los autómatas y cómo pueden simularse entre sí para que no puedan distinguirse: Bisimulación . (cf Bisimulación en wikipedia)

No recuerdo bien, debería volver a leer el capítulo, pero hubo un problema con la simulación y la bisimulación que los hizo insuficientes para las equivalencias computacionales.

Así, Robin Milner presenta su Pi-Calculus y lo expone para el resto del libro.

En última instancia, en su último libro The Space and Motion of Communicating Agents , podría echar un vistazo a Bigraphs de Robin Milner. Pueden modelar autómatas, redes de Petri, cálculo de Pi y otras metodologías computacionales.

Hasta donde yo sé, la única (o al menos más común) forma de hacerlo es comparar los idiomas que aceptan las máquinas / modelos. Ese es el objetivo de la teoría de Autómatas: toma el concepto vago de un problema o algoritmo y lo convierte en un conjunto matemático concreto (es decir, un lenguaje) sobre el que podemos razonar.

La manera más fácil de hacer esto es, dada una máquina / función arbitraria de un modelo, construir una máquina a partir del segundo modelo que calcule el mismo lenguaje. Lo más probable es que use inducción en la longitud de la expresión, estados en la máquina, reglas en la gramática, etc.

No he visto esto hecho con Lambda y TM (aunque estoy 99% seguro de que es posible), pero definitivamente he visto este tipo de cosas para probar la equivalencia de NFA y expresiones regulares. Primero muestra un NFA que puede aceptar cualquier átomo, luego, usando la inducción, crea NFA que acepta la unión / concatenación / estrella de Kleene de cualquier NFA más pequeño.

Luego haces lo contrario, para encontrar un RE para cualquier NFA.