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

Problem
Quantum program verification relies heavily on weakest preconditions (wp) to reason about program behavior. Existing frameworks, such as those by D'Hondt and Panangaden [11] and extensions for expected runtime analysis like Liu et al. [25], fundamentally require that the predicates or expectations used in the calculus be bounded (specifically, bounded by the identity operator $I$). This restriction limits the analysis of quantum programs to finite-dimensional Hilbert spaces and almost surely terminating (AST) programs.

A critical gap exists in analyzing programs that are AST but possess an infinite expected runtime. In infinite-dimensional settings (e.g., quantum integers), a program may terminate with probability 1 while its expected runtime diverges to infinity. Standard wp-calculus fails here because the weakest precondition of a non-terminating loop is 0, which cannot capture the infinite cost accumulated before termination. Furthermore, existing expected runtime calculi (ERT) are restricted to finite dimensions and AST programs, preventing the analysis of unbounded operators and non-AST behaviors where termination probability is less than 1.

Methodology
The authors propose a novel framework based on pre-expectations that removes the boundedness requirement. The methodology involves:

1. Redefining Expectations: The paper introduces a new class of operators called "expectations" ($E(H)$) defined as positive, $\infty$-self-adjoint operators on a separable Hilbert space. Unlike standard self-adjoint operators, these allow for non-dense domains and unbounded values. The authors define a specific order ($\sqsubseteq$) based on the square roots of these operators and their domains, proving that the set of expectations forms an $\omega$-complete partial order ($\omega$-cpo). This structure is essential for defining the semantics of while-loops via least upper bounds.
2. Semantic and Syntactic Definitions: The authors define a concrete quantum programming language, qrWhile, which includes reward statements (reward(c)). They provide a denotational semantics that separates the evolution of the quantum state (density operators) from the accumulation of expected rewards.
3. Weakest Pre-Expectation (wp) Calculus: A syntactic weakest pre-expectation transformer is defined for qrWhile programs. This transformer maps a post-expectation to a pre-expectation. Crucially, the calculus handles unbounded operators and rewards, allowing the expression of expected runtimes even when they are infinite.
4. Runtime Analysis via Transformation: To analyze expected runtime, the authors propose a syntactic transformation $T(S)$ that inserts reward(1) statements into a reward-free program $S$. The expected runtime of $S$ is then equivalent to the expected reward of $T(S)$.
5. Forward and Backward Transformers: The paper defines both a forward expected runtime transformer ($ERT$) and a backward transformer ($ert$). It proves that the backward $ert$ transformer is equivalent to the weakest pre-expectation of the transformed program $T(S)$.
6. Induction Rules: The authors adapt Park induction to provide proof rules for establishing upper bounds on expected runtimes and termination probabilities without computing exact least upper bounds.

Key Contributions

• Unbounded Expectations: The definition of a new class of expectations ($E(H)$) that supports unbounded operators and infinite values, forming an $\omega$-cpo under a novel order. This allows reasoning about programs in infinite-dimensional Hilbert spaces (e.g., quantum integers).
• Generalized Weakest Pre-Expectation: A syntactic and semantic weakest pre-expectation calculus for qrWhile programs with rewards. This framework drops the boundedness condition required in previous work [11, 38], making it strictly more expressive.
• Runtime Analysis for Non-AST and Infinite-Dimensional Programs: The ability to analyze expected runtimes for programs that are not almost surely terminating and for those with infinite expected runtimes. The paper demonstrates that AST does not imply finite expected runtime in infinite dimensions.
• Equivalence of Approaches: A proof that the forward expected runtime transformer, the backward $ert$ transformer, and the weakest pre-expectation of the transformed program all coincide.
• Proof Rules: The introduction of Park induction rules for bounding weakest preconditions and expected runtimes in the unbounded case.

Results
The paper validates the framework through two example programs:

1. Sequential Composition of Loops: A program composed of two loops is analyzed. The first loop has a finite expected runtime, while the second has an infinite expected runtime for certain superpositions, despite being AST for all basis states. The framework correctly identifies the total program as having infinite expected runtime, a result not derivable using existing bounded calculi.
2. One-Sided Quantum Walk: A variant of a quantum walk where the walker moves left or stays. The analysis reveals a nuanced termination behavior:
   • For states with negative position ($n < 0$), the program is not AST.
   • For states with non-negative position ($n \ge 0$), the program is AST.
   • However, for superpositions of non-negative states, the program is AST but not Positive Almost Surely Terminating (PAST), meaning it has an infinite expected runtime.
     The framework successfully characterizes these distinct termination and runtime properties, showing that the space of AST states is closed, while the space of PAST states is not necessarily closed.

Significance
The paper claims that its primary significance lies in providing a comprehensive and expressive framework for analyzing the expected runtime of quantum programs without restricting to finite-dimensional spaces or almost surely terminating programs. By introducing unbounded pre-expectations, the authors enable the verification of programs that were previously intractable, particularly those involving quantum integers and infinite expected runtimes. The work addresses a specific challenge noted in prior literature [25] regarding the infinite-dimensional case and extends the deductive verification paradigm to handle unbounded costs and rewards naturally. The authors emphasize that their approach maintains the style of weakest preconditions from the finite-dimensional case while generalizing the underlying mathematical objects to support unboundedness.