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

Christina Gehnen; Dominique Unruh; Joost-Pieter Katoen

A pre-expectation framework reasons about quantum program preconditions without upper bounds, so expected runtime can be analyzed even when it may be infinite.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-15 05:21 UTC pith:RMR3RILC

load-bearing objection Abstract-only claim of a bound-free quantum pre-expectation calculus for expected runtime (incl. infinite); useful if the preservation theorems hold, but we cannot check them yet. the 2 major comments →

arxiv 2607.12532 v1 pith:RMR3RILC submitted 2026-07-14 cs.LO cs.PLquant-ph

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

Christina Gehnen , Dominique Unruh , Joost-Pieter Katoen This is my paper

classification cs.LO cs.PLquant-ph

keywords quantum weakest preconditionspre-expectationsexpected runtimequantum programsreward statementsprogram transformationruntime analysis

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper revisits quantum weakest preconditions with the goal of analyzing the expected runtime of quantum programs, including cases where that expectation may be infinite. Standard approaches often require an a priori upper bound on the quantities being reasoned about; the authors introduce a novel pre-expectation framework that removes that requirement. The framework is especially useful for programs that contain reward statements, which can encode runtime cost. One concrete route they develop is a program transformation that rewrites a quantum program so that its expected runtime becomes expressible as a weakest pre-expectation with rewards. The result is a calculus that can certify runtime behavior without presupposing that the expectation is finite.

Core claim

Quantum weakest preconditions can be recast as a pre-expectation calculus that does not demand an upper bound on the quantities of interest, thereby supporting expected-runtime analysis of quantum programs (including those with rewards and those whose expected runtime may be infinite) via transformations that reduce runtime questions to weakest pre-expectation calculations.

What carries the argument

The novel pre-expectation framework for quantum programs (together with a program transformation that encodes expected runtime via reward statements so that weakest pre-expectation calculus applies directly).

Load-bearing premise

The program transformation and reward encoding must preserve the true expected runtime of the original quantum program, including when that expectation is infinite.

What would settle it

Exhibit a concrete quantum program whose true expected runtime (computed by other means) differs from the weakest pre-expectation obtained after the proposed reward transformation, especially on an instance with infinite expected runtime.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

Expected runtime of quantum programs can be stated and reasoned about inside a weakest pre-expectation calculus without first proving finiteness.
Reward statements become a systematic device for turning runtime questions into pre-expectation questions.
Programs whose expected runtime diverges can still be analyzed rather than excluded by an upper-bound hypothesis.
Several alternative routes to the same analysis become available once the pre-expectation framework is in place.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same bound-free pre-expectation style may transfer to other quantitative properties of quantum programs (energy, entanglement cost) that can be encoded as rewards.
Classical expected-runtime calculi that already use rewards may serve as a template for verifying soundness of the quantum transformation.
Tool builders could implement the transformation as a front-end that reuses existing quantum weakest-precondition engines for runtime queries.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

Abstract-only claim of a bound-free quantum pre-expectation calculus for expected runtime (incl. infinite); useful if the preservation theorems hold, but we cannot check them yet.

read the letter

The one thing you need to know: this paper claims a novel pre-expectation framework for quantum programs that drops the usual upper-bound requirement, so you can reason about expected runtime—including cases where it may be infinite—especially with reward statements. The main technical vehicle is a program transformation that encodes runtime via rewards and then reuses weakest pre-expectation calculus.

What looks new and useful is exactly that removal of the bound. Existing quantum wp variants often force you to supply an a-priori upper bound; for loops or reward-carrying programs that may not terminate almost-surely, that is a real obstacle. Framing expected runtime as a special case of wp-with-rewards via a transformation is a clean idea if it works. The authors (Katoen et al.) know the classical and quantum wp literature well, so the survey/revisit part is likely careful.

Soft spots are almost entirely information gaps, not visible flaws. We have only the abstract: no definitions of the pre-expectation operators, no statement of the transformation, no theorems. The load-bearing claim is that the transformed program’s weakest pre-expectation equals the true expected runtime of the original even when that expectation is infinite. That preservation has to be proved carefully (domains, measures, continuity at infinity). Nothing in the abstract contradicts itself or smells like circularity; it is simply unverifiable from what we have. “Several ways” to do the analysis is also left vague.

This is for people already working on quantum program logics or probabilistic resource analysis. A reader who cares about quantum wp or expected runtime of quantum loops will get value from the full development. It is coherent enough and important enough inside the subfield to deserve a serious referee rather than a desk reject. I would not cite or bring it to reading group on the abstract alone, but I would send it out for review and then decide.

Referee Report

2 major / 1 minor

Summary. The manuscript (available only as an abstract) revisits quantum weakest preconditions for expected-runtime analysis of quantum programs. It claims a novel pre-expectation framework that reasons about preconditions without requiring an upper bound, motivated by programs with reward statements and by the need to handle potentially infinite expected runtime. Several approaches are announced, including a program transformation that encodes expected runtime so that it can be recovered from a weakest pre-expectation calculus with rewards.

Significance. If the framework is sound and the announced transformation correctly preserves expected runtime (including the infinite case), the work would extend classical pre-expectation techniques to quantum programs without artificial upper bounds and would give a usable tool for runtime analysis of non-terminating or infinite-expectation quantum programs. That would be a solid contribution to quantum program verification. The abstract alone, however, supplies no definitions, theorems, or examples with which to assess whether those claims hold.

major comments (2)

Only the abstract is available for review. The central load-bearing claim—that a program transformation encodes expected runtime into rewards so that the weakest pre-expectation of the transformed program equals the true expected runtime even when that expectation is infinite—cannot be checked: there are no definitions of the pre-expectation operators, no statement of the transformation, and no soundness or preservation theorems. Assessment of correctness is therefore impossible on the supplied material.
The abstract asserts that the framework works “without the need of an upper bound” and handles “potentially infinite expected runtime.” Without the body it is impossible to verify whether the operators are well-defined on unbounded or infinite expectations, whether the fixed-point characterizations remain valid, or whether the reward encoding is faithful in the infinite case. These points are essential to the paper’s main contribution and must be established formally before acceptance can be considered.

minor comments (1)

The abstract is clear on motivation but does not name the concrete quantum programming language, the precise form of reward statements, or the relationship to existing quantum weakest-precondition calculi; those details should appear early in the full manuscript for positioning.

Circularity Check

0 steps flagged

No circularity can be established from the abstract alone; this is a definitional formal-methods paper with no exhibited self-definitional reductions or fitted predictions.

full rationale

Only the abstract is available. It claims a novel pre-expectation framework for quantum programs that avoids upper bounds, enabling expected-runtime analysis (including infinite cases) via a program transformation that encodes runtime with rewards so that weakest pre-expectation yields the expected runtime. No equations, definitions of the operators, statements of the transformation, soundness theorems, or citations appear in the provided material. Consequently no step can be shown to reduce by construction to its inputs (self-definitional, fitted-input-as-prediction, load-bearing self-citation, uniqueness import, ansatz smuggling, or renaming). The work is a formal-methods contribution rather than an empirical fitting exercise; residual risk that the preservation claim is definitional rather than proved cannot be checked without the body and does not constitute exhibited circularity under the rules. Score 0 with empty steps is the correct honest finding.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 2 invented entities

Abstract-only review: free parameters are not introduced (this is not a fitting paper). Axioms are the usual background of quantum programming semantics and weakest-precondition reasoning that the abstract relies on without stating them. No new physical entities are invented; the 'invented' objects are formal constructs (pre-expectation, reward encoding, program transformation) whose independent evidence cannot be assessed from the abstract.

axioms (3)

domain assumption Quantum programs have a well-defined denotational or operational semantics in which expected runtime (possibly infinite) is meaningful.
The abstract's goal of analyzing expected runtime, including infinite cases, presupposes a semantic model of quantum programs and expectation; not proved in the abstract.
domain assumption Weakest preconditions / pre-expectations can be extended with reward statements so that accumulated cost equals expected runtime.
Central technique in the abstract; standard in probabilistic wp calculi but must hold for the quantum setting they use.
ad hoc to paper A program transformation exists that preserves expected runtime when encoding it into rewards for the pre-expectation calculus.
The abstract presents this as one of the ways to analyze runtime; the preservation property is load-bearing and paper-specific.

invented entities (2)

Quantum pre-expectation framework without upper bound no independent evidence
purpose: Reason about preconditions and expected runtime of quantum programs when expected runtime may be infinite.
Named as the novel contribution; independent evidence would be soundness/completeness theorems and examples in the full paper, not available here.
Program transformation encoding expected runtime via rewards no independent evidence
purpose: Express expected runtime of a quantum program as a weakest pre-expectation of a transformed program with reward statements.
Presented as a concrete method in the abstract; falsifiable only via formal proof that the transformation preserves expectation.

pith-pipeline@v1.1.0-grok45 · 6015 in / 2567 out tokens · 24919 ms · 2026-07-15T05:21:20.722061+00:00 · methodology

0 comments

read the original abstract

Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest preconditions from the perspective of expected runtime analysis of quantum programs and introduce a novel pre-expectation framework that enables to reason about the preconditions of quantum programs without the need of an upper bound. This is particularly interesting for quantum programs involving reward statements. The overall goal is to analyze runtime behavior even in the case of programs with potentially infinite expected runtime. This paper presents several ways to do so, e.g., a program transformation such that the expected runtime of a quantum program can be expressed using the weakest pre-expectation calculus with rewards.

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

Core claim

What carries the argument

Load-bearing premise

What would settle it

If this is right

Where Pith is reading between the lines

discussion (0)