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

Problema
A verificação de programas quânticos depende fortemente de pré-condições mais fracas (wp) para raciocinar sobre o comportamento do programa. Estruturas existentes, como as de D'Hondt e Panangaden [11] e extensões para análise de tempo de execução esperado como a de Liu et al. [25], exigem fundamentalmente que os predicados ou as expectativas usados no cálculo sejam limitados (especificamente, limitados pelo operador identidade $I$). Essa restrição limita a análise de programas quânticos a espaços de Hilbert de dimensão finita e programas quase certamente terminantes (AST).

Existe uma lacuna crítica na análise de programas que são AST, mas possuem um tempo de execução esperado infinito. Em configurações de dimensão infinita (ex: inteiros quânticos), um programa pode terminar com probabilidade 1 enquanto seu tempo de execução esperado diverge para o infinito. O cálculo wp padrão falha aqui porque a pré-condição mais fraca de um loop não terminante é 0, o que não consegue capturar o custo infinito acumulado antes da terminação. Além disso, os cálculos de tempo de execução esperado (ERT) existentes são restritos a dimensões finitas e programas AST, impedindo a análise de operadores não limitados e comportamentos não-AST onde a probabilidade de terminação é menor que 1.

Metodologia
Os autores propõem uma nova estrutura baseada em pré-expectativas que remove o requisito de limitação. A metodologia envolve:

1. Redefinição de Expectativas: O artigo introduz uma nova classe de operadores chamados "expectativas" ($E(H)$) definidos como operadores positivos, $\infty$-autoadjuntos em um espaço de Hilbert separável. Diferente dos operadores autoadjuntos padrão, estes permitem domínios não densos e valores não limitados. Os autores definem uma ordem específica ($\sqsubseteq$) baseada nas raízes quadradas desses operadores e seus domínios, provando que o conjunto de expectativas forma um $\omega$-cpo (ordem parcialmente completa de $\omega$). Esta estrutura é essencial para definir a semântica de loops while via supremos de ordem inferior.
2. Definições Semânticas e Sintáticas: Os autores definem uma linguagem de programação quântica concreta, qrWhile, que inclui declarações de recompensa (reward(c)). Eles fornecem uma semântica denotacional que separa a evolução do estado quântico (operadores de densidade) da acumulação de recompensas esperadas.
3. Cálculo de Pré-expectativa Mais Fraca (wp): Um transformador sintático de pré-expectativa mais fraca é definido para programas qrWhile. Este transformador mapeia uma pós-expectativa para uma pré-expectativa. Crucialmente, o cálculo lida com operadores e recompensas não limitados, permitindo a expressão de tempos de execução esperados mesmo quando estes são infinitos.
4. Análise de Tempo de Execução via Transformação: Para analisar o tempo de execução esperado, os autores propõem uma transformação sintática $T(S)$ que insere declarações reward(1) em um programa $S$ livre de recompensas. O tempo de execução esperado de $S$ é então equivalente à recompensa esperada de $T(S)$.
5. Transformadores de Direção Avançada e Reversa: O artigo define tanto um transformador de tempo de execução esperado direto ($ERT$) quanto um transformador reverso ($ert$). Eles provam que o transformador $ert$ reverso é equivalente à pré-expectativa mais fraca do programa transformado $T(S)$.
6. Regras de Indução: Os autores adaptam a indução de Park para fornecer regras de prova para estabelecer limites superiores em tempos de execução esperados e probabilidades de terminação sem calcular os supremos de ordem inferior exatos.

Principais Contribuições

• Expectativas Não Limitadas: A definição de uma nova classe de expectativas ($E(H)$) que suporta operadores não limitados e valores infinitos, formando um $\omega$-cpo sob uma nova ordem. Isso permite o raciocínio sobre programas em espaços de Hilbert de dimensão infinita (ex: inteiros quânticos).
• Pré-expectativa Mais Fraca Generalizada: Um cálculo de pré-expectativa mais fraca sintático e semântico para programas qrWhile com recompensas. Esta estrutura elimina a condição de limitação exigida em trabalhos anteriores [11, 38], tornando-a estritamente mais expressiva.
• Análise de Tempo de Execução para Programas Não-AST e de Dimensão Infinita: A capacidade de analisar tempos de execução esperados para programas que não são quase certamente terminantes e para aqueles que possuem tempos de execução esperados infinitos. O artigo demonstra que AST não implica tempo de execução esperado finito em dimensões infinitas.
• Equivalência de Abordagens: Uma prova de que o transformador de tempo de execução esperado direto, o transformador $ert$ reverso e a pré-expectativa mais fraca do programa transformado coincidem.
• Regras de Prova: A introdução de regras de indução de Park para limitar pré-expectativas e tempos de execução esperados no caso não limitado.

Resultados
O artigo valida a estrutura através de dois programas de exemplo:

1. Composição Sequencial de Loops: Um programa composto por dois loops é analisado. O primeiro loop possui um tempo de execução esperado finito, enquanto o segundo possui um tempo de execução esperado infinito para certas superposições, apesar de ser AST para todos os estados de base. O framework identifica corretamente o programa total como tendo tempo de execução esperado infinito, um resultado não derivável usando cálculos limitados existentes.
2. Caminhada Quântica Unilateral: Uma variante de uma caminhada quântica onde o caminhante move-se para a esquerda ou permanece parado. A análise revela um comportamento de terminação matizado:
   • Para estados com posição negativa ($n < 0$), o programa não é AST.
   • Para estados com posição não negativa ($n \ge 0$), o programa é AST.
   • No entanto, para superposições de estados não negativos, o programa é AST, mas não é POSITIVAMENTE Quase Certamente Terminante (PAST), o que significa que possui um tempo de execução esperado infinito.
     O framework caracteriza com sucesso essas propriedades distintas de terminação e tempo de execução, mostrando que o espaço de estados AST é fechado, enquanto o espaço de estados PAST não é necessariamente fechado.

Significância
O artigo afirma que sua principal significância reside em fornecer uma estrutura abrangente e expressiva para analisar o tempo de execução esperado de programas quânticos sem restringir a espaços de dimensão finita ou programas quase certamente terminantes. Ao introduzir pré-expectativas não limitadas, os autores permitem a verificação de programas que eram anteriormente intratáveis, particularmente aqueles envolvendo inteiros quânticos e tempos de execução esperados infinitos. O trabalho aborda um desafio específico observado na literatura anterior [25] em relação ao caso de dimensão infinita e estende o paradigma de verificação dedutiva para lidar naturalmente com custos e recompensas não limitados. Os autores enfatizam que sua abordagem mantém o estilo de pré-condições mais fracas do caso de dimensão finita, enquanto generaliza os objetos matemáticos subjacentes para suportar a não limitação.