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

21

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.

saadtaame
fonte
Eu acho que você escolheu os livros errados.
Raphael
@Raphael O que é um bom livro sobre o assunto?
Saadtaame
Eu gostaria de dizer "qualquer livro sobre autômatos", mas aparentemente isso agora é verdade. Infelizmente, não tenho nenhum livro de inglês adequado em mãos, desculpe.
Raphael
1
Um livro sobre autômatos não será suficiente.
Reinierpost
Que livros você está usando?
Saadtaame

Respostas:

20

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

M=(Q,ΣI,ΣO,δ,q0,QF)

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

AM=(Q{q1,q2},ΣI,ΣO,δ,q1,QF)

com e fornecido porΣO=ΣO.{$}δ

(q1,a,hl,hr)δ(q1,ahl,hr) para todos os e , para todos os , para todos os com , para todos os ,aΣIhr,hlΣO
(q1,ε,hl,hr)δ(q2,hl,hr)hr,hlΣO
(q2,ε,hl,hr)δ(q2,ε,hlhr)hr,hlΣOhl$
(q2,ε,$,hr)δ(q0,$,hr)hrΣO
(q,ε,hl,hr)δ(q,ε,hla)(q,hr)δ(q,a,L)para todos e , para todos , para todos , para todos e e para todos osqQhlΣO
(q,ε,$,hr)δ(q,$,a)(q,hr)δ(q,a,L)qQ
(q,ε,hl,hr)δ(q,ahl,ε)(q,hr)δ(q,a,R)qQ,hlΣO
(q,ε,hl,$)δ(q,hl,$)qQhlΣO
(q,ε,hl,hr)δ(q,hl,a)(q,hr)δ(q,a,N)qQ,hlΣ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:ΣO$ΣO(q,a,hl,hr)δ(q,l1li,r1rj)AMaqq

atualização da pilha
[ 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.AMxΣIMMAM

Rafael
fonte
@frabala Você estava certo, eu tive os estados iniciais da maneira errada. Corrigido agora, obrigado!
Raphael
4

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.

Stephane Rolland
fonte
2

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.

jmite
fonte