Auxiliary Rules of Quantum Hoare Logic

This entry follows Chapter 6 §6.7. Figures 6.9–6.10 and Lemma 6.8 were checked against printed pages 131–133 (PDF pages 41–43). See Hoare rules for triple semantics. All assertions are effects, $0\preceq A\preceq I$. Local operators are implicitly extended by identities.

Locality and invariant assertions

A command uses variables $\operatorname{var}(S)$. For an effect $C$ on a disjoint set $V$, its cylindric extension is $C\otimes I_{\operatorname{var}(S)}$. Axiom (Ax.Inv) gives $\{C\}S\{C\}_p$. This is a partial-correctness axiom: the command may still diverge.

Rule (R.TI) derives $\{A\}S\{B\}$ from $\{A\otimes I_W\}S\{B\otimes I_W\}$ when $V\cap W=\varnothing$, $A,B$ act on $V$, and $\operatorname{var}(S)\subseteq V$. It holds for partial and total correctness. Removing an unused auxiliary space does not license ignoring entanglement.

Convex combinations and independent invariants

If every $\{A_i\}S\{B_i\}_*$ holds, $p_i\geq0$ and $\sum_i p_i\leq1$, rule (R.CC) yields

The same correctness convention must be used throughout. Convex combinations preserve effect bounds; multiplying noncommuting effects is not a replacement for conjunction.

Rule (R.Inv) adds the same independent assertion $C$ to both sides of a triple:

The variables of $C$ must be disjoint from those of the command.

Adjoint operations and scaling

Rule (R.SO) transforms a triple into $\{\mathcal E^*(A)\}S\{\mathcal E^*(B)\}$ when the quantum operation $\mathcal E$ acts on variables unused by $S$. It holds for total correctness. Partial correctness additionally requires trace preservation of $\mathcal E$. It cannot be applied indiscriminately to noise on the registers the command modifies.

Rule (R.Lin) gives $\{\lambda A\}S\{\lambda B\}$ for $\lambda\geq0$, provided both scaled operators remain effects. Total correctness permits this scaling; partial correctness additionally requires $\lambda\leq1$, since its nontermination compensation cannot be scaled arbitrarily.

Weak operator limits

Suppose $A_n\to A$ and $B_n\to B$ in the weak operator topology: for all vectors $\psi,\phi$, $\langle\psi|A_n|\phi\rangle\to\langle\psi|A|\phi\rangle$. If all $\{A_n\}S\{B_n\}_*$ hold, (R.Lim) gives $\{A\}S\{B\}_*$. The assertions remain uniformly bounded effects; arbitrary divergent matrix series do not qualify.

Strengthening combination with nontermination bounds

For normalized input define $d_S(\rho)=1-\mathrm{tr}(\llbracket S\rrbracket(\rho))$. The book's $\operatorname{Term}(C)$ means $d_S(\rho)\leq\mathrm{tr}(C\rho)$, an upper bound on nontermination. Its $\operatorname{Abort}(C)$ means $\mathrm{tr}(C\rho)\leq d_S(\rho)$, a lower bound. The name Term does not assert unconditional termination.

Given partial triples $\{A_i\}S\{B_i\}_p$:

• (R.CC1): if $p_i\geq0$, $s=\sum_i p_i\leq1$ and $\operatorname{Abort}(C)$ holds, the precondition is $\sum_i p_iA_i+(1-s)C$ and the postcondition is $\sum_i p_iB_i$.
• (R.CC2): if $\lambda_i\geq0$, $s=\sum_i\lambda_i\geq1$ and $\operatorname{Term}(C)$ holds, the precondition is $\sum_i\lambda_iA_i-(s-1)C$ and the postcondition is $\sum_i\lambda_iB_i$. Both must remain effects.

For example, a never-terminating command has $d_S=1$, so $\operatorname{Abort}(I)$ holds. Its partial correctness does not establish that any output is produced.

Source

Mingsheng Ying, Foundations of Quantum Programming, second edition, §6.7, printed pages 131–133, Figures 6.9–6.10 and Lemmas 6.8–6.9. Chapter 6 DOI. This entry verifies the auxiliary rules; it does not certify completion of the remaining chapter audit.