Quantum Weakest Preconditions Revisited: Pre-expectations for Expected Runtime Analysis

Problema
La verificación de programas cuánticos depende en gran medida de las precondiciones débiles (wp) para razonar sobre el comportamiento de los programas. Los marcos existentes, como los de D'Hondt y Panangaden [11] y las extensiones para el análisis del tiempo de ejecución esperado de Liu et al. [25], requieren fundamentalmente que los predicados o las expectativas utilizados en el cálculo estén acotados (específicamente, acotados por el operador identidad $I$). Esta restricción limita el análisis de los programas cuánticos a espacios de Hilbert de dimensión finita y programas casi seguramente terminantes (AST).

Existe una brecha crítica en el análisis de programas que son AST pero que poseen un tiempo de ejecución esperado infinito. En entornos de dimensión infinita (por ejemplo, enteros cuánticos), un programa puede terminar con probabilidad 1 mientras que su tiempo de ejecución esperado diverge hacia el infinito. El cálculo wp estándar falla aquí porque la precondición débil de un bucle no terminante es 0, lo cual no puede capturar el costo infinito acumulado antes de la terminación. Además, los cálculos de tiempo de ejecución esperado existentes (ERT) están restringidos a dimensiones finitas y programas AST, lo que impide el análisis de operadores no acotados y comportamientos no AST donde la probabilidad de terminación es menor que 1.

Metodología
Los autores proponen un nuevo marco basado en pre-expectativas que elimina el requisito de acotación. La metodología involucra:

1. Redefinición de las Expectativas: El artículo introduce una nueva clase de operadores llamados "expectativas" ($E(H)$) definidos como operadores positivos, $\infty$-autoadjuntos en un espacio de Hilbert separable. A diferencia de los operadores autoadjuntos estándar, estos permiten dominios no densos y valores no acotados. Los autores definen un orden específico ($\sqsubseteq$) basado en las raíces cuadradas de estos operadores y sus dominios, demostrando que el conjunto de expectativas forma un orden parcial $\omega$-completo ($\omega$-cpo). Esta estructura es esencial para definir la semántica de los bucles while mediante supremos de orden inferior.
2. Definiciones Semánticas y Sintácticas: Los autores definen un lenguaje de programación cuántica concreto, qrWhile, que incluye sentencias de recompensa (reward(c)). Proporcionan una semántica denotacional que separa la evolución del estado cuántico (operadores de densidad) de la acumulación de recompensas esperadas.
3. Cálculo de Precondición Débil de Expectativa (wp): Se define un transformador sintáctico de precondición débil de expectativa para programas qrWhile. Este transformador mapea una post-expectativa a una pre-expectativa. Crucialmente, el cálculo maneja operadores no acotados y recompensas, permitiendo la expresión de tiempos de ejecución esperados incluso cuando estos son infinitos.
4. Análisis de Tiempo de Ejecución mediante Transformación: Para analizar el tiempo de ejecución esperado, los autores proponen una transformación sintáctica $T(S)$ que inserta sentencias reward(1) en un programa libre de recompensas $S$. El tiempo de ejecución esperado de $S$ es equivalente a la recompensa esperada de $T(S)$.
5. Transformadores de Avance y Retroceso: El artículo define tanto un transformador de tiempo de ejecución esperado hacia adelante (forward) como uno hacia atrás (backward). Demuestran que el transformador de retroceso $ert$ es equivalente a la precondición débil de expectativa del programa transformado $T(S)$.
6. Reglas de Inducción: Los autores adaptan la inducción de Park para proporcionar reglas de prueba para establecer límites superiores en los tiempos de ejecución esperados y las probabilidades de terminación sin calcular los supremos de orden inferior exactos.

Contribuciones Clave

• Expectativas No Acotadas: La definición de una nueva clase de expectativas ($E(H)$) que soporta operadores no acotados y valores infinitos, formando un $\omega$-cpo bajo un nuevo orden. Esto permite el razonamiento sobre programas en espacios de Hilbert de dimensión infinita (por ejemplo, enteros cuánticos).
• Precondición Débil de Expectativa Generalizada: Un cálculo de precondición débil de expectativa sintáctico y semántico para programas qrWhile con recompensas. Este marco elimina la condición de acotación requerida en trabajos previos [11, 38], siendo estrictamente más expresivo.
• Análisis de Tiempo de Ejecución para Programas No-AST y de Dimensión Infinita: La capacidad de analizar tiempos de ejecución esperados para programas que no son casi seguramente terminantes y para aquellos que tienen tiempos de ejecución esperados infinitos. El artículo demuestra que AST no implica un tiempo de ejecución esperado finito en dimensiones infinitas.
• Equivalencia de Enfoques: Una prueba de que el transformador de tiempo de ejecución esperado hacia adelante, el transformador $ert$ hacia atrás y la precondición débil de expectativa del programa transformado coinciden.
• Reglas de Prueba: La introducción de reglas de inducción de Park para acotar las precondiciones débiles y los tiempos de ejecución esperados en el caso no acotado.

Resultados
El artículo valida el marco a través de dos programas de ejemplo:

1. Composición Secuencial de Bucles: Se analiza un programa compuesto por dos bucles. El primer bucle tiene un tiempo de ejecución esperado finito, mientras que el segundo tiene un tiempo de ejecución esperado infinito para ciertas superposiciones, a pesar de ser AST para todos los estados base. El marco identifica correctamente que el programa total tiene un tiempo de ejecución esperado infinito, un resultado que no es derivable utilizando los cálculos acotados existentes.
2. Caminata Cuántica Unilateral: Una variante de una caminata cuántica donde el caminante se mueve a la izquierda o se queda en su lugar. El análisis revela un comportamiento de terminación matizado:
   • Para estados con posición negativa ($n < 0$), el programa no es AST.
   • Para estados con posición no negativa ($n \ge 0$), el programa es AST.
   • Sin embargo, para superposiciones de estados no negativos, el programa es AST pero no es Positivamente Casi Seguramente Terminante (PAST), lo que significa que tiene un tiempo de ejecución esperado infinito.
     El marco caracteriza con éxito estas distintas propiedades de terminación y tiempo de ejecución, mostrando que el espacio de estados AST es cerrado, mientras que el espacio de estados PAST no es necesariamente cerrado.

Significancia
El artículo afirma que su principal significancia radica en proporcionar un marco exhaustivo y expresivo para analizar el tiempo de ejecución esperado de programas cuánticos sin restringirse a espacios de dimensión finita o programas casi seguramente terminantes. Al introducir pre-expectativas no acotadas, los autores permiten la verificación de programas que anteriormente eran intratables, particularmente aquellos que involucran enteros cuánticos y tiempos de ejecución esperados infinitos. El trabajo aborda un desafío específico señalado en la literatura previa [25] respecto al caso de dimensión infinita y extiende el paradigma de verificación deductiva para manejar costos y recompensas no acotados de forma natural. Los autores enfatizan que su enfoque mantiene el estilo de las precondiciones débiles del caso de dimensión finita mientras generaliza los objetos matemáticos subyacentes para soportar la no acotación.