¿Podría usarse una computadora cuántica para escribir una prueba lógica de que una aplicación de software no tiene errores, equivalente a probar todas las combinaciones posibles de entrada y salida?

En adelante, una prueba debe considerarse como un proceso, el cálculo en sí mismo, ya que debemos aceptar que en el futuro, las computadoras cuánticas probarán teoremas mediante métodos que ni un cerebro humano ni ningún otro árbitro podrán verificar paso a paso- paso, ya que si la ‘secuencia de proposiciones’ correspondiente a dicha prueba se imprimiera, el papel llenaría el universo observable muchas veces ”. David Deutsch en su artículo: Máquinas, lógica y física cuántica escrito hace 28 años con Artur Ekert y Rossella Lupacchini.

Si bien Deutsch fue pionero en el campo de la computación cuántica al formular una descripción para una máquina cuántica de Turing, las expectativas que fomentó para la computación cuántica en el caso de probar que los programas superan la realidad, incluso con las extensiones más optimistas del arte actual.

Omitiendo la idea de que probar el software requiere asegurar su terminación; La complejidad de expresar un programa que es lo suficientemente complejo como para requerir inspección de la máquina, aunque en realidad no es muy complejo, supera con creces los tamaños de registro de qubit y los tiempos de decoherencia que parecen probables para las próximas décadas. (Digo esto mientras recuerdo que mi primera computadora, una Kim 1, tenía una memoria de 512 bytes.) Los registros Qubit y el tiempo de decoherencia, en el futuro previsible, limitarán los programas cuánticos.

Una base axiomática para la programación de computadoras por CAR HOARE proporciona la base para estimar la complejidad.

Los axiomas permiten al diseñador de lenguaje expresar sus intenciones generales de manera simple y directa, sin la masa de detalles que generalmente acompaña a las descripciones algorítmicas. Finalmente, los axiomas pueden formularse de una manera en gran medida independiente entre sí, de modo que el diseñador pueda trabajar libremente en un axioma o grupo de axiomas sin temor a efectos inesperados de interacción con otras partes del lenguaje.

Incluso en el formato compacto ofrecido por Hoare, las entradas necesarias no serían digeribles por las computadoras cuánticas sin una mejora de dos o tres órdenes de magnitud.

Puedo retomar la respuesta de Marc Weber a ¿Se podría usar una computadora cuántica para escribir una prueba lógica de que una aplicación de software no tiene errores, lo que equivale a probar todas las combinaciones posibles de entrada y salida? Termina

La respuesta es “depende”. Para hacer una prueba o no hacer una prueba, primero debe abordar el problema de detención. El problema de detención nos enseña que algunos problemas no pueden resolverse. Uno de esos problemas es decidir si algún algoritmo arbitrario se detiene (alguna vez se completa).

¿Por qué? Bueno, supongamos que la entrada a ese algoritmo es en sí misma, pero en cualquier lugar donde dejaría de decir que la entrada se detendría, en su lugar se repite para siempre. Entonces, la entrada a ese programa es otra copia del programa original … y así sucesivamente con una cantidad infinita de entrada, volteándose de un lado a otro entre los dos programas. En la clase de informática, aprende que esto significa que la computadora tendrá que profundizar en los algoritmos infinitamente profundo para llegar a una respuesta. Las máquinas de Turing por su definición no pueden tener estados infinitos. Entonces, el programa que podría determinar si otro programa está libre de errores … se puede hacer que se repita para siempre. Esto crea una clase de algoritmos que se denominan “no calificables”.

Entonces, esencialmente, no. Puede jugar con la verificación de la ausencia de errores de muchas maneras diferentes, pero no hay forma de verificar que esté completamente libre de errores, salvo demostrar que el algoritmo no se puede asignar al problema de detención. ‘Buscar bucles infinitos’ simplemente no se puede calcular en todos los casos.

Como ejemplo más práctico, suponga que está escribiendo un programa que desea verificar si hay pérdidas de memoria, pero una de las entradas al programa borró toda la memoria. Puede tener una secuencia de entrada que se quede sin memoria sin borrarla nunca, pero ¿es realmente una pérdida de memoria si la entrada esperada era borrar memoria ocasionalmente? ¿Qué pasaría si la excepción de falta de memoria borrara toda la memoria? ¿Seguiría teniendo pérdidas desde un punto de vista práctico?

Una computadora cuántica no puede resolver fundamentalmente ningún problema que no pueda ser resuelto por una máquina de Turing determinista (lea “computadora normal”). Esto incluye el problema de determinar si un programa tiene un bucle infinito. La posibilidad de un bucle infinito en alguna entrada se consideraría un error grave en algunos programas, y no hay una forma general de resolver este problema, Quantum o no.

Las ganancias de una Computadora Cuántica estarían en la eficiencia de la solución, no en la capacidad de solución.

Para darle una idea de cuán difícil es el problema del “bucle infinito”, intente determinar si el siguiente programa trivialmente simple tiene un bucle infinito en alguna entrada.

Entrada x
Deje y = 1
Mientras x> 1 Do
Deje y = y + 1
Si x es par
Deje x = x / 2
Más
Deje x = x * 3 + 1
Terminara si
Fin mientras
Salida y

¿Están completas las computadoras cuánticas? Para que puedan verificarlo. Entonces, ¿qué estrategia utilizar para encontrar la prueba? Hay un gran espacio de solución, prueba y error. Entonces, tal vez la respuesta sea ‘en algunos casos por accidente’. No conozco la teoría perfectamente detrás de encontrar pruebas. Solo sepa que pueden verificarse fácilmente una vez que existen.