Quantum Weakest Preconditions
Quantum Weakest Preconditions
D'Hondt and Panangaden develop predicate transformers and weakest-precondition semantics for quantum computation.
Paper information (2006, Mathematical Structures in Computer Science 16(3):429–451) — Ellie D’Hondt and Prakash Panangaden. DOI; author archive PDF; earlier arXiv version
Work
The paper develops predicate transformers for quantum computation, especially the weakest precondition (wp). Given a program's state transformation and a postcondition, wp describes which input states are sufficient to ensure that postcondition. The authors establish a Stone-type duality between state-transformer and weakest-precondition semantics, use the Kraus representation theorem to obtain weakest preconditions for completely positive maps, and apply the account to Selinger's language and stabilizer situations.
Contributions
- A weakest-precondition notion based directly on quantum computation rather than a reduction to probabilistic programs.
- A state-transformer and predicate-transformer correspondence with a Stone-type duality.
- An existence result for weakest preconditions of completely positive maps, grounded in the Kraus representation theorem.
- Examples involving Selinger's quantum language and stabilizer reasoning.
Limits
The framework primarily treats quantum programs represented by operators and completely positive maps; loops, recursion, classical stores, nontermination, and numerical approximation require additional fixed-point or other extensions. A wp formula is a semantic reasoning tool, not an automatic generator of invariants, a machine-checked proof, or a hardware-noise guarantee. The chosen predicate order also determines what “weakest” means in a particular model.
Connections
The paper directly underlies the wiki's Weakest Preconditions entry and turns the superoperator semantics of QPL into backward predicate transformation. It shares a program-logic goal with Reasoning About Imperative Quantum Programs, but emphasizes transformer duality and backward postcondition reasoning, whereas the latter focuses on a logic for imperative programs. Later quantum Hoare logic and expected-runtime work extend this line.
Original paper
Ellie D’Hondt and Prakash Panangaden, Quantum Weakest Preconditions, Mathematical Structures in Computer Science 16(3), 429–451 (2006), DOI: 10.1017/S0960129506005251. Author archive PDF; earlier arXiv version