Quantum Programming Logic

Origin. D'Hondt and Panangaden (2006), Ying (2012). 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	Löwner order	State comparison
†	U+2020	Dagger	Adjoint
\|0⟩	—	Zero state	Initial qubit
wp	—	Weakest precondition	Precondition

Metatheory. Soundness: valid triples preserve quantum semantics. Completeness: for finite-dimensional. Quantum wp well-defined. No cloning: classical rules don't apply directly. Entanglement complicates local reasoning.

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

Limitations. Infinite-dimensional harder. Continuous parameters. Error/noise modeling separate. Tool support emerging. Scalability challenges. Entanglement across qubits.