¿Cómo verifica si dos algoritmos devuelven el mismo resultado para cualquier entrada?

18

¿Cómo se verifica si dos algoritmos (por ejemplo, ordenar por combinación y ordenar por ingenuo) devuelven el mismo resultado para cualquier entrada, cuando el conjunto de todas las entradas es infinito?

Actualización: Gracias Ben por describir cómo esto es imposible de hacer algorítmicamente en el caso general. La respuesta de Dave es un gran resumen de métodos algorítmicos y manuales (sujetos a ingenio y metáfora humana) que no siempre funcionan, pero son bastante efectivos.

computability formal-methods software-engineering software-verification Andres Riofrio
fuente
55
Como dijo Yuval, no hay ningún procedimiento que pueda determinar eso para dos programas. pero en un caso especial como su ejemplo, puede probarlo: por ejemplo, si prueba que ambos algoritmos devuelven una secuencia ordenada y son estables, habrá terminado.
Sasho Nikolov
1
¿Quieres una técnica / algoritmo automático o un conjunto de técnicas manuales?
Dave Clarke
@SashoNikolov, si el rendimiento se considera parte del resultado, también debería mostrar que ambos operan en la misma complejidad de tiempo / espacio.
edA-qa mort-ora-y
1
¿Quieres decir "comprobar" o probar? ¿Significa "cualquier entrada" o todas las entradas? ¿Cuál es la motivación y el contexto para la pregunta?
Kaveh
2
@AndresRiorio: las técnicas de prueba son diferentes de los algoritmos que resuelven el problema general. Por ejemplo, el problema de detención es indecidible, pero ciertamente es posible probar la finalización de muchos programas (a mano o heurística automatizada).
Raphael

Respuestas:

16

En contraste con lo que dicen los que no dicen, hay muchas técnicas efectivas para hacer esto.

  • La bisimulación es un enfoque. Véase, por ejemplo, el artículo de Gordon sobre Coinducción y Programación Funcional .

  • Otro enfoque es utilizar teorías operacionales de equivalencia de programas, como el trabajo de Pitts .

  • Un tercer enfoque es verificar que ambos programas satisfagan la misma especificación funcional. Hay miles de documentos sobre este enfoque.

  • Un cuarto enfoque es mostrar que un programa puede reescribirse en el otro mediante transformaciones de programas de sonido .

Por supuesto, ninguno de estos métodos está completo debido a la indecidibilidad, pero se han producido volúmenes y volúmenes de trabajo para abordar el problema.

Dave Clarke
fuente
heu · ris · tic . [Gramo. εὑρίσκω "descubrir"] n. 1. Una técnica diseñada para resolver un problema que ignora si se puede demostrar que la solución es correcta, pero que generalmente produce una buena solución o resuelve un problema más simple que contiene o se cruza con la solución del problema más complejo. 2. ( Theor. ) Un algoritmo que no funciona.
JeffE
1
Bart Simpson: "No puedo ganar. No lo intentes".
Dave Clarke
9
@JeffE: si desea verificar si dos algoritmos devuelven el mismo resultado, debe hacer una prueba. Hay muchas buenas técnicas para hacer esto. Claro, todos los métodos están incompletos, pero ¿a quién le importa? ¡El teorema de incompletitud de Goedel no es una razón para renunciar a las matemáticas!
Neel Krishnaswami
3
@JeffE El hecho de que no haya una función computable para determinar si dos algoritmos arbitrarios devuelven el mismo resultado no significa que no pueda responder la pregunta para dos algoritmos particulares , especialmente porque el proceso de búsqueda de una prueba no es computable la función . Del mismo modo, hay un montón de documentos que prueban la terminación garantizada de algoritmos particulares, independientemente del hecho de que no es posible determinar mecánicamente si un algoritmo arbitrario siempre terminará.
Ben
2
En la práctica, dos algoritmos que se supone que calculan la misma función casi nunca permiten una prueba de equivalencia basada en bisimulación. (En el caso de los algoritmos de clasificación mencionados anteriormente, las etapas intermedias de los bucles / recursión son diferentes). Diría que usar la buena lógica de Hoare para mostrar que ambos implementan la misma especificación del comportamiento de E / S es la forma ir.
Kai
10

Para elaborar un poco sobre las declaraciones de "es imposible", aquí hay un bosquejo de prueba simple.

Podemos modelar algoritmos con salida por Turing Machines que se detienen con su salida en su cinta. Si desea tener máquinas que puedan detenerse, ya sea aceptando con salida en su cinta o rechazando (en cuyo caso no hay salida), puede encontrar fácilmente una codificación que le permita modelar estas máquinas con el "alto o alto no". no hay máquinas de rechazo ".

Ahora, suponga que tengo un algoritmo P para determinar si dos de estas TM tienen la misma salida para cada entrada. Luego, dada una TM A y una entrada X , puedo construir una nueva TM B que funcione de la siguiente manera:

  1. Compruebe si la entrada es exactamente X
  2. En caso afirmativo, ingrese un bucle infinito
  3. Si no, entonces ejecute A en la entrada

Ahora puedo correr P en A y B . B no se detiene en X , pero tiene la misma salida que A para todas las demás entradas, por lo que si y solo si A no se detiene en X , estos dos algoritmos tienen la misma salida para cada entrada. Pero se suponía que P podía determinar si dos algoritmos tienen la misma salida para cada entrada, por lo que si tuviéramos P podríamos saber si una máquina arbitraria se detiene en una entrada arbitraria, que es el problema de detención. Como se sabe que el problema de detención es indecidible, P no puede existir.

Esto significa que no existe un enfoque general (computable) para determinar si dos algoritmos tienen el mismo resultado que siempre funciona, por lo que debe aplicar un razonamiento particular al par de algoritmos que está analizando. Sin embargo, en la práctica puede haber enfoques computables que funcionen para grandes clases de algoritmos, y ciertamente existen técnicas que puede usar para tratar de encontrar una prueba para un caso particular. La respuesta de Dave Clarke le da algunas cosas relevantes para ver aquí. El resultado de "imposibilidad" solo se aplica al diseño de un método genérico que resuelva el problema de una vez por todas, para todos los pares de algoritmos.

Ben
fuente
PAG
@Raphael Sí, el argumento que bosquejé no dice nada sobre una P tan restringida , solo que no puede existir una totalmente general. Mi instinto es que el problema de detención aún es indecidible incluso cuando lo restringe a "algoritmos de clasificación" en lugar de algoritmos generales, en cuyo caso la prueba de imposibilidad aún se mantiene, aunque nunca he escuchado tal afirmación.
Ben
2
En términos más generales, el teorema de Rice establece que no hay una forma computable de probar algo sobre un algoritmo, tan pronto como haya al menos un algoritmo que tenga la propiedad que está tratando de probar y al menos una que no. Por ejemplo, dado un algoritmo A, no existe una función computable que tome un algoritmo B como entrada y pruebe si B es equivalente a A.
Gilles 'SO- deja de ser malo'
Es importante tener en cuenta que el teorema de Rice se aplica solo a las propiedades de los lenguajes , no a las máquinas de Turing (cuando las usa como modelo de "algoritmo"). Si es posible que existan dos máquinas de Turing que reconocen el mismo lenguaje pero una tiene la propiedad y la otra no, entonces el teorema de Rice no se aplica, y puede haber un método computable general para probar la propiedad. Pero el teorema de Rice se aplica claramente a este caso, sí.
Ben
2

Es imposible en general, pero muchas limitaciones pueden hacerlo posible. Por ejemplo, puede verificar la equivalencia de dos programas de código de línea recta utilizando BDD. La ejecución simbólica puede manejar muchos otros casos.

James Koppel
fuente
1

Es imposible diseñar un algoritmo que pruebe esta igualdad en general. Sugerencia: reducción del problema de detención.

Yuval Filmus
fuente
Existen muchas técnicas, aunque ninguna es completamente automática.
Dave Clarke
No sé si es posible o no, por su respuesta es solo un comentario. No es una respuesta.
@SaeedAmiri: Desarrollé un poco el contexto de la respuesta; Creo que es lo suficientemente completo, si tal vez no es particularmente bueno.
Raphael
@Raphael, la reducción que está en la mente de Yuval es obvia, y no creo que OP no sea consciente de eso, pero el problema difícil de la OMI es encontrar alguna forma para casos especiales, por lo que esta reducción obvia podría ser un comentario para recordarle a OP para caso general.
2
@SaeedAmiri: Eso es para que el OP y los votantes decidan entonces, no nosotros.
Raphael