Quantum Programming Logic

Origin. D'Hondt and Panangaden (2006), Ying (2011). Hoare-style logic for quantum programs. Quantum weakest precondition. Verification of quantum algorithms. Foundation for quantum program correctness.

Models. Program logic for quantum. Classical Hoare: {P} C {Q} with P, Q sets of states. Quantum Hoare: {P} C {Q} with P, Q positive operators below the identity, so that assertions are graded rather than yes-or-no and tr(Pρ) reads off the degree to which state ρ satisfies P. Quantum operations as commands, and their adjoints as predicate transformers.

Formalism.

States and predicates: ρ: density matrix (positive, trace ≤ 1) — the state. P: quantum predicate, a positive operator with 0 ⊑ P ⊑ I — the assertion. These are not the same kind of object. They are paired by tr(Pρ), the probability that ρ satisfies P; writing a triple as {ρ} C {σ} with density matrices in the assertion slots conflates them. ⊑: Löwner order (Q − P positive semidefinite). Partial correctness: {P} C {Q} means tr(Pρ) ≤ tr(Q · ⟦C⟧(ρ)) for every ρ.

Quantum commands:

q := |0⟩ (initialization)
q := U[q] (unitary transformation)
measure q (measurement)
if □m=i → Pᵢ fi (measurement-based conditional)

Quantum Hoare rules: Initialization: {I} q := |0⟩ {|0⟩⟨0|}

Unitary: {U†PU} q := U[q] {P}

Measurement: {Σᵢ Mᵢ†PMᵢ} measure q {P}

The daggers stand to the left, matching U†PU: predicates are pulled backwards through the operation. Forward conjugation Σᵢ MᵢPMᵢ† is the evolution of states, and is the wrong direction here.

Sequential: {P} C₁ {Q} {Q} C₂ {R} ───────────────────────── {P} C₁; C₂ {R}

Quantum weakest precondition: wp⟦C⟧(P) = ⟦C⟧†(P), the adjoint of the program's superoperator — the Heisenberg picture to ⟦C⟧'s Schrödinger picture. It is characterized exactly, not merely bounded: tr(wp⟦C⟧(P) · ρ) = tr(P · ⟦C⟧(ρ)) for every ρ. Then {Q} C {P} holds iff Q ⊑ wp⟦C⟧(P), so wp⟦C⟧(P) is the ⊑-largest precondition. Logically weakest is order-theoretically largest, since a larger positive operator is satisfied with at least as high a probability by every state.

Total correctness: Loops: require termination proof. Quantum while: fixed-point semantics.

Symbols.

Symbol	Unicode	Name	Meaning
ρ, σ	U+03C1, U+03C3	Density matrix	Quantum state
P, Q	—	Quantum predicate	Positive operator, 0 ⊑ P ⊑ I
U	—	Unitary	Quantum gate
M	—	Measurement	Observable
⊑	U+2291	Square image of or equal / Löwner order	P ⊑ Q iff Q − P is positive semidefinite
×	U+00D7	Multiplication sign	Matrix dimensions, as in 2^n × 2^n
†	U+2020	Dagger	Adjoint
\|0⟩	—	Zero state	Initial qubit
wp	—	Weakest precondition	Precondition
⟦C⟧	—	Denotation brackets	Superoperator denoted by command C
Σ	U+03A3	Sigma / Summation	Sum over measurement outcomes
⟨	U+27E8	Mathematical left angle bracket	Opens a bra
⟩	U+27E9	Mathematical right angle bracket	Closes a ket
□	U+25A1	White square / Guarded choice	Branch marker in the measurement conditional
≤	U+2264	Less-than or equal	Numerical comparison of traces
⊓	U+2293	Square cap / Meet	Greatest lower bound in the Löwner order, which need not exist
I	—	Identity operator	The weakest predicate
tr	—	Trace	tr(Pρ) is the probability that ρ satisfies P
0	—	Zero operator	Least element of the Löwner CPO

Metatheory. D'Hondt and Panangaden (2006) established the duality the calculus rests on: quantum predicates are the effects, positive operators below I, and the weakest precondition of a command is the adjoint of its superoperator, characterized exactly by tr(wp⟦C⟧(P)ρ) = tr(P⟦C⟧(ρ)) for every ρ. This is the Heisenberg picture to the denotation's Schrödinger picture, and it makes {Q} C {P} equivalent to Q ⊑ wp⟦C⟧(P), so the weakest precondition is the ⊑-greatest solution. Selinger (2004) supplied the domain theory: partial density operators under the Löwner order form a CPO with least element 0, and superoperators are Scott-continuous on it, so while-loops denote least fixed points and the predicate transformer inherits continuity. Ying (2011) proved soundness and completeness of the resulting Floyd–Hoare system for quantum while-programs under partial correctness, with total correctness requiring a separate termination argument. Because wp is the adjoint, it is completely positive, and it is unital exactly when the command is trace-preserving, which is the operator form of guaranteed termination.

Applies to. Quantum algorithm verification. Quantum error correction. Quantum cryptography. Quantum compilers. Formal methods for quantum.

Limitations. The predicate space is not a lattice. By Kadison's antilattice theorem self-adjoint operators are lattice-ordered only in the commutative case, so P ⊓ Q generally fails to exist, there is no conjunction rule, and a postcondition cannot be assembled from independently established parts. Assertions are graded: tr(Pρ) is a probability, so a triple bounds probabilities rather than asserting truth, and a state satisfies P outright only when P is a projection containing the support of ρ. There is no frame rule — entanglement means a subsystem has no independent state, so separation-logic variants must impose separability side conditions. Completeness requires that the assertion language contain arbitrary effects, 2^n × 2^n operators with no finite syntax, so proof obligations grow exponentially with register size and need not be decidable. The calculus supplies no termination argument, and noise must be an explicit channel; approximate correctness is not expressible by exact triples.