Como você verifica se dois algoritmos retornam o mesmo resultado para alguma entrada?

17

Como você verifica se dois algoritmos (por exemplo, classificação de mesclagem e classificação Naïve) retornam o mesmo resultado para qualquer entrada, quando o conjunto de todas as entradas é infinito?

Atualização: Obrigado Ben por descrever como isso é impossível de ser feito algoritmicamente no caso geral. A resposta de Dave é um ótimo resumo de métodos algorítmicos e manuais (sujeitos à inteligência e metáfora humanas) que nem sempre funcionam, mas são bastante eficazes.

computability formal-methods software-engineering software-verification Andres Riofrio
fonte
5
como disse o yuval, não existe procedimento que possa determinar isso para dois programas. mas em um caso especial como o seu exemplo, você pode provar: por exemplo, se você provar que seus algoritmos retornam uma sequência classificada e são estáveis, você estará pronto.
Sasho Nikolov 25/05
1
Deseja uma técnica / algoritmo automático ou um conjunto de técnicas manuais?
Dave Clarke
@SashoNikolov, se o desempenho for considerado parte da saída, você também precisará mostrar que ambos operam na mesma complexidade de tempo / espaço.
EdA-qa mort-ora-y
1
Você quer dizer "verificar" ou provar? Significa "qualquer entrada" ou todas as entradas? Qual é a motivação e o contexto da pergunta?
Kaveh
2
@AndresRiorio: As técnicas de prova são diferentes dos algoritmos que resolvem o problema geral. Por exemplo, o problema da parada é indecidível, mas certamente é possível provar a finalização de muitos programas (manualmente ou heurística automatizada).
Raphael

Respostas:

16

Em contraste com o que dizem os negativistas, existem muitas técnicas eficazes para fazer isso.

  • A bisimulação é uma abordagem. Veja, por exemplo, o artigo de Gordon sobre Coindução e Programação Funcional .

  • Outra abordagem é usar teorias operacionais de equivalência de programas, como o trabalho de Pitts .

  • Uma terceira abordagem é verificar se os dois programas atendem à mesma especificação funcional. Existem milhares de artigos sobre essa abordagem.

  • Uma quarta abordagem é mostrar que um programa pode ser reescrito no outro usando transformações de programas de som .

Obviamente, nenhum desses métodos está completo devido à indecidibilidade, mas volumes e volumes de trabalho foram produzidos para solucionar o problema.

Dave Clarke
fonte
heurística . [Gr. εὑρίσκω "descobrir"] n. 1. Uma técnica projetada para resolver um problema que ignora se é possível provar que a solução está correta, mas que geralmente produz uma boa solução ou resolve um problema mais simples que contém ou cruza com a solução do problema mais complexo. 2. ( Teor. ) Um algoritmo que não funciona.
25412 JeffE
1
Bart Simpson: "Não posso vencer. Não tente".
Dave Clarke
9
@ Jeff: Se você quiser verificar se dois algoritmos retornam o mesmo resultado, faça uma prova. Existem muitas boas técnicas para fazer isso. Claro, todos os métodos estão incompletos, mas quem se importa? O teorema da incompletude de Goedel não é uma razão para desistir da matemática!
Neel Krishnaswami
3
@JeffE Só porque não há função computável para determinar se dois algoritmos arbitrários retornam o mesmo resultado, não significa que você não possa responder à pergunta de dois algoritmos específicos , especialmente porque o processo de busca por uma prova não é computável função . Da mesma forma, existem muitos documentos que comprovam o término garantido para algoritmos específicos, independentemente do fato de que não é possível determinar mecanicamente se um algoritmo arbitrário sempre terminará.
Ben
2
Na prática, dois algoritmos que supostamente calculam a mesma função quase nunca permitem uma prova de equivalência baseada em bisimulação. (No caso dos algoritmos de classificação mencionados acima, os estágios intermediários dos loops / recursão são diferentes.) Eu diria que usando a boa e velha lógica Hoare para mostrar que ambos implementam a mesma especificação de comportamento de E / S é o caminho ir.
Kai
10

Para elaborar um pouco as declarações "é impossível", aqui está um esboço de prova simples.

Podemos modelar algoritmos com saída da Turing Machines que param com sua saída em sua fita. Se você deseja ter máquinas que podem parar, aceitando com saída na fita ou rejeitando (nesse caso, não há saída), você pode facilmente criar uma codificação que permita modelar essas máquinas com a opção "parar ou parar", não há máquinas "rejeitadas".

Agora, suponha que eu tenha um algoritmo P para determinar se duas dessas TMs têm a mesma saída para cada entrada. Então, dado uma TM A e uma entrada X , posso construir uma nova TM B que opera da seguinte maneira:

  1. Verifique se a entrada é exatamente X
  2. Se sim, insira um loop infinito
  3. Se não, execute A na entrada

Agora eu posso correr P em A e B . B não para em X , mas tem a mesma saída que A para todas as outras entradas, portanto, se e somente se A não para em X , esses dois algoritmos têm a mesma saída para cada entrada. Mas P foi assumida para ser capaz de dizer se dois algoritmos têm a mesma saída para cada entrada, de modo que se tivéssemos P poderíamos dizer se uma máquina pára arbitrárias sobre uma entrada arbitrária, que é o Deter problema. Como o problema da parada é conhecido como indecidível, P não pode existir.

Isso significa que não há uma abordagem geral (computável) para determinar se dois algoritmos têm a mesma saída que sempre funciona; portanto, você deve aplicar um raciocínio específico ao par de algoritmos que você está analisando. No entanto, na prática, pode haver abordagens computáveis ​​que funcionem para grandes classes de algoritmos, e certamente existem técnicas que você pode usar para tentar elaborar uma prova para qualquer caso específico. A resposta de Dave Clarke fornece algumas coisas relevantes para você analisar aqui. O resultado da "impossibilidade" se aplica apenas à criação de um método genérico que resolva o problema de uma vez por todas, para todos os pares de algoritmos.

Ben
fonte
P
@Raphael Sim, o argumento que esbocei não diz nada sobre um P tão restrito , apenas que um totalmente geral não pode existir. Meu instinto é que o problema de parada ainda é indecidível, mesmo quando você o restringe a "algoritmos de classificação" em vez de algoritmos gerais, nesse caso a prova de impossibilidade ainda é válida, embora eu nunca tenha ouvido uma afirmação desse tipo.
Ben
2
De maneira mais geral, o teorema de Rice afirma que não há maneira computável de provar algo sobre um algoritmo, assim que houver pelo menos um algoritmo que tenha a propriedade que você está tentando provar e pelo menos um que não tenha. Por exemplo, dado um algoritmo A, não há função computável que tome um algoritmo B como entrada e teste se B é equivalente a A.
Gilles 'SO- stop be evil'
É importante notar que o teorema de Rice se aplica apenas a propriedades de linguagens , não de Turing Machines (quando você as usa como modelo de "algoritmo"). Se for possível existir duas Máquinas de Turing que reconhecem o mesmo idioma, mas uma possui a propriedade e a outra não, o teorema de Rice não se aplica e pode haver um método computável geral para testar a propriedade. Mas o teorema de Rice se aplica claramente a este caso, sim.
Ben
2

É impossível em geral, mas muitas restrições podem tornar isso possível. Por exemplo, você pode verificar a equivalência de dois programas de código linear usando BDDs. A execução simbólica pode lidar com muitos outros casos.

James Koppel
fonte
1

É impossível conceber um algoritmo que prove essa igualdade em geral. Dica: redução do problema de parada.

Yuval Filmus
fonte
Existem muitas técnicas, embora nenhuma seja totalmente automática.
Dave Clarke
Não sei se é possível ou não, por sua resposta é apenas um comentário. não é uma resposta.
@SaeedAmiri: Aprofundei um pouco o contexto da resposta; Eu acho que está completo o suficiente, se não particularmente bom.
Raphael
@ Rafael, a redução que está na mente de Yuval é óbvia, e não acho que o OP não esteja ciente disso, mas o difícil problema da IMO é encontrar um caminho para casos especiais. Portanto, essa redução óbvia pode ser um comentário apenas para lembrar o OP para caso geral.
2
@SaeedAmiri: Isso é para o OP e os eleitores decidirem então, não nós.
Raphael