Como mostrar dois modelos de computação são equivalentes?

Estou procurando uma explicação sobre como alguém poderia provar que dois modelos de computação são equivalentes. Eu tenho lido livros sobre o assunto, exceto que as provas de equivalência são omitidas. Eu tenho uma idéia básica sobre o que significa dois modelos de computação serem equivalentes (a visão de autômatos: se eles aceitam as mesmas linguagens). Existem outras maneiras de pensar sobre equivalência? Se você pudesse me ajudar a entender como provar que o modelo da máquina de Turing é equivalente ao cálculo lambda, isso seria suficiente.

Você mostra que um dos modelos pode simular o outro, que recebe uma máquina no modelo A, mostra que existe uma máquina no modelo B que calcula a mesma função. Observe que esta simulação não precisa ser computável (mas geralmente é).

Considere, por exemplo, autômatos de empilhamento com duas pilhas (2-PDA). Em outra pergunta , as simulações em ambas as direções são descritas. Se você fizesse isso formalmente, usaria uma máquina de Turing geral (uma tupla) e construiria explicitamente qual seria o 2-PDA correspondente e vice-versa.

Formalmente, essa simulação pode ser assim. Deixei

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

seja uma máquina de Turing (com uma fita). Então,

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

com e fornecido por$\Sigma_O' = \Sigma_O \overset{.}{\cup} \{\$\}$$\delta'$

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

é um 2-PDA equivalente. Aqui, assumimos que a máquina de Turing usa como símbolo em branco, ambas as pilhas começam com um marcador (que nunca é removido) e significa que consome a entrada , alterna os estados de para e atualiza as pilhas da seguinte forma:$\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'$

^{[ fonte ]}

Resta mostrar que entra em um estado final em se e somente se faz isso. Isto é bastante claro pela construção; formalmente, você deve traduzir aceitando execuções em em aceitando execuções em e vice-versa.$A_M$$x \in \Sigma_I^*$$M$$M$$A_M$

No início de sistemas móveis e de comunicação: o Pi-Calculus, de Robin Milner, há uma introdução aos autômatos e como eles podem simular um ao outro para que não possam ser distinguidos: bisimulação . (cf Bisimulação na wikipedia)

Não me lembro bem, deveria reler o capítulo, mas houve um problema com a simulação e a bimimulação que os tornou insuficientes para equivalências computacionais.

Assim, Robin Milner apresenta seu Pi-Calculus e o expõe pelo resto do livro.

Por fim, em seu último livro The Space and Motion of Communicating Agents , você pode dar uma olhada nos Bigraphs de Robin Milner. Eles podem modelar Automata, redes de Petri, Pi-Calculus e outras metodologias computacionais.

Até onde eu sei, a única (ou pelo menos mais comum) maneira de fazer isso é comparar os idiomas aceitos pelas máquinas / modelos. Esse é o ponto principal da teoria de Autômatos: ele pega o conceito vago de um problema ou algoritmo e o transforma em um conjunto matemático concreto (isto é, uma linguagem) com o qual podemos raciocinar.

A maneira mais fácil de fazer isso é, dada uma máquina / função arbitrária de um modelo, construir uma máquina a partir do segundo modelo que calcula a mesma linguagem. É provável que você use indução no comprimento da expressão, estados na máquina, regras na gramática etc.

Não vi isso com Lambda e TMs (embora tenha 99% de certeza que é possível), mas definitivamente vi esse tipo de coisa para provar a equivalência de NFAs e expressões regulares. Primeiro, você mostra um NFA que pode aceitar qualquer átomo e, em seguida, usando indução, cria NFAs que aceitam a estrela de união / concatenação / Kleene de qualquer NFA menor.

Então você faz o oposto, para encontrar um ER para qualquer NFA.