Quantum Hoare Rules and Loop Proofs

This page follows Quantum While Programs: Syntax and Execution and uses the notation of Quantum Hoare Logic and Weakest Preconditions. We use finite-dimensional registers, unnormalized execution branches, and denotational semantics that collects terminating paths. Let $E=\llbracket S\rrbracket$ . Assertions are effects $0\preceq P\preceq I$ , and $A\preceq B$ means that $B-A$ is positive semidefinite.

Assertions and two notions of correctness

For every partial density operator $\rho$ , total and partial correctness require respectively

\models_{tot}\{P\}S\{Q\}\Longleftrightarrow \operatorname{tr}(P\rho)\le\operatorname{tr}(QE(\rho)),

\models_{par}\{P\}S\{Q\}\Longleftrightarrow \operatorname{tr}(P\rho)\le\operatorname{tr}(QE(\rho)) +\operatorname{tr}(\rho)-\operatorname{tr}(E(\rho)).

Subscripts $t$ and $p$ below denote total and partial correctness. Total correctness imposes a termination obligation only over the effect promised by the precondition. An arbitrary total triple does not imply global termination on every input: $P=I$ forces termination on normalized inputs, while $P=0$ gives a trivial triple. A derivation must keep one correctness convention throughout.

Basic axioms

\{P\}\ \mathbf{skip}\ \{P\}_*,\qquad \{U^\dagger P U\}\ \bar q:=U[\bar q]\ \{P\}_*.

Initialization is defined by $\mathcal R_q(\rho)=\sum_iA_i\rho A_i^\dagger$ , where $A_i=|0\rangle\langle i|_q\otimes I$ . Its rule is

\left\{\sum_i A_i^\dagger P A_i\right\}\ q:=0\ \{P\}_*.

The precondition therefore cannot be obtained by mechanically substituting 0 for $q$ in a matrix assertion. For the single-qubit postcondition $P=|0\rangle\langle0|$ , the calculated precondition is $I$ .

Sequencing and consequence

\frac{\{P\}S_1\{R\}_*\quad\{R\}S_2\{Q\}_*} {\{P\}S_1;S_2\{Q\}_*}.

\frac{P\preceq P'\quad\{P'\}S\{Q'\}_*\quad Q'\preceq Q} {\{P\}S\{Q\}_*}.

The directions follow from the trace inequalities: decreasing the precondition effect or increasing the postcondition effect preserves validity. Classical set implication cannot simply replace the Löwner order.

Measurement case rule

If $\{P_m\}S_m\{Q\}_*$ holds for every outcome $m$ and $\sum_mM_m^\dagger M_m=I$ , then

\left\{\sum_mM_m^\dagger P_mM_m\right\} \mathbf{if}\ (\square_m M=m\to S_m)\ \mathbf{fi}\ \{Q\}_*.

These are branches of one measurement, not successive tests of independent Boolean conditions. Measurement disturbance is represented by $M_m$ on both sides. An input entangled with untouched registers must still be interpreted on a common Hilbert space.

qPD: the partial-correctness loop rule

Let $W=\mathbf{while}\ M=1\ \mathbf{do}\ S\ \mathbf{od}$ with measurement $\{M_0,M_1\}$ . Choose $P$ as the assertion before the body on the continuing branch and $Q$ as the postcondition after exit, and set

R=M_0^\dagger QM_0+M_1^\dagger PM_1.

The qPD loop rule is

\frac{\{P\}S\{R\}_p}{\{R\}W\{Q\}_p}.

$R$ is the assertion before the measurement, $P$ constrains only states entering the body on the continuing branch, and $Q$ constrains exit states. They are generally different. The rule permits a divergent body or loop; the partial-correctness compensation term accounts for remaining mass. It is the same rule as (R.LP) on the main Quantum Hoare Logic page.

qPD also contains skip, initialization, unitary, sequencing, case, and Löwner consequence rules. Theorem 6.1 (printed p. 117) proves qPD sound, and Theorem 6.2 (printed p. 120) proves relative completeness, assuming facts about the complex field and an assertion language expressive enough for the required wlp. Relative completeness does not mean that a tool will synthesize an invariant automatically.

qTD: total correctness and ranking functions

Simply replacing $p$ by $t$ in the qPD loop rule is unsound: a nonterminating loop may still satisfy the body-preservation premise. Definition 6.10 (printed p. 121) calls

t_\epsilon:\mathcal D(\mathcal H_{all})\to\mathbb N

an $(A,\epsilon)$ -ranking function, for an effect $A$ and $\epsilon>0$ , exactly when, for every partial density operator $\rho$ ,

T(\rho)=\llbracket S\rrbracket(M_1\rho M_1^\dagger),\qquad t_\epsilon(T(\rho))\le t_\epsilon(\rho),

and

\operatorname{tr}(A\rho)\ge\epsilon \Longrightarrow t_\epsilon(T(\rho))<t_\epsilon(\rho).

The measured continuing branch must be part of $T$ ; the classical comparison $t(\llbracket S\rrbracket(\rho))<t(\rho)$ is not the quantum obligation. Well-foundedness of $\mathbb N$ rules out an infinite strictly descending chain.

With this page's notation $R=M_0^\dagger QM_0+M_1^\dagger PM_1$ , the textbook (R.LT) rule (Figure 6.5, printed p. 123) is

\frac{ \{P\}S\{R\}_t\quad \forall\epsilon>0,\ t_\epsilon\text{ is a }(M_1^\dagger PM_1,\epsilon)\text{-ranking function} }{ \{R\}W\{Q\}_t}.

The textbook figure uses $P$ for the final assertion and $Q$ for the body assertion, exactly the opposite letter convention from this page; the rule has the same meaning. The ranking function concerns mass relevant to the precondition and does not require global termination for every input. Neither the body's total-correctness premise nor the condition for every positive threshold $\epsilon$ may be dropped.

Lemma 6.6 (printed p. 122) gives the equivalent residual-limit criterion. For any ranking-related effect $A$ , an $(A,\epsilon)$ -ranking function exists for every $\epsilon>0$ exactly when

\lim_{n\to\infty}\operatorname{tr}\left(A(\llbracket S\rrbracket\circ E_1)^n(\rho)\right)=0, \qquad E_1(\rho)=M_1\rho M_1^\dagger,

for every $\rho$ . In this page's (R.LT), substitute $A=M_1^\dagger PM_1$ , where $P$ is the body precondition. This is the vanishing of residual mass during continuing iterations as observed by $A$ , not a claim that a global termination mass automatically vanishes for an arbitrary precondition. Theorem 6.3 (printed p. 124) and Theorem 6.4 (printed p. 126) establish qTD soundness and relative completeness.

Weakest preconditions and fixed points

For the trace adjoint $E^*$ ,

\operatorname{wp}_S(Q)=E^*(Q),\qquad \operatorname{wlp}_S(Q)=E^*(Q)+I-E^*(I),

and total and partial triples are equivalent to $P\preceq\operatorname{wp}_S(Q)$ and $P\preceq\operatorname{wlp}_S(Q)$ respectively. A loop wp is obtained as the least fixed point by iterating

F_Q(X)=M_0^\dagger QM_0+M_1^\dagger\operatorname{wp}_S(X)M_1

from the zero effect. Replacing the body wp by wlp and approximating downward from $I$ gives the greatest fixed point. See Weakest Preconditions for the transformer equations.

Example: a measurement loop that resets a qubit

For computational-basis measurement and body $X$ , choose exit postcondition $Q=|0\rangle\langle0|$ and continuing-branch body precondition $P=|1\rangle\langle1|$ . Then $R=I$ and $\{P\}X\{I\}_p$ holds, so qPD yields $\{I\}W\{Q\}_p$ . After $X$ , the continuing branch exits at the next measurement, so this particular loop terminates almost surely and the same triple is totally correct. That termination fact belongs to the example; it is not a consequence of the qPD loop rule alone.

References and audit page index

This page is aligned with the main Quantum Hoare Logic page and checked against Chapter 6 of Foundations of Quantum Programming: qPD Figure 6.3 is PDF p. 25 / printed p. 115; qPD soundness and completeness are PDF pp. 27 and 30 / printed pp. 117 and 120; Definition 6.10 is PDF p. 31 / printed p. 121; Lemma 6.6 is PDF p. 32 / printed p. 122; qTD Figure 6.5 and (R.LT) are PDF p. 33 / printed p. 123; qTD soundness and completeness are PDF pp. 34 and 36 / printed pp. 124 and 126. Definitions, structural wp/wlp equations, and auxiliary rules are summarized on the main page.

Mingsheng Ying, Foundations of Quantum Programming, Chapter 6, 2024, DOI.
Mingsheng Ying, Floyd–Hoare Logic for Quantum Programs, 2011, DOI.