Quantum weakest preconditions

DOI10.1017/S0960129506005251zbMATH Open1122.68058arXivquant-ph/0501157OpenAlexW2121087903MaRDI QIDQ5482269FDOQ5482269

Ellie D'Hondt, Prakash Panangaden

Publication date: 28 August 2006

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Abstract: We develop a notion of predicate transformer and, in particular, the weakest precondition, appropriate for quantum computation. We show that there is a Stone-type duality between the usual state-transformer semantics and the weakest precondition semantics. Rather than trying to reduce quantum computation to probabilistic programming we develop a notion that is directly taken from concepts used in quantum computation. The proof that weakest preconditions exist for completely positive maps follows immediately from the Kraus representation theorem. As an example we give the semantics of Selinger's language in terms of our weakest preconditions. We also cover some specific situations and exhibit an interesting link with stabilizers.

Full work available at URL: https://arxiv.org/abs/quant-ph/0501157

Recommendations

• Generalised quantum weakest preconditions
• Commutativity of quantum weakest preconditions
• Commutativity of quantum weakest liberal precondition and its properties
• Weakly intuitionistic quantum logic
• Weak sufficiency of quantum statistics
• Contextuality under weak assumptions
• Kochen-Specker theorem as a precondition for quantum computing
• scientific article; zbMATH DE number 764483
• Quantum lower bounds by quantum arguments
• Quantum lower bounds by quantum arguments

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Quantum computation (81P68)

Cited In (25)

• Healthiness conditions for predicate transformers
• A proof system for disjoint parallel quantum programs
• Natural Quantum Operational Semantics with Predicates
• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
• The monoidal structure of Turing machines
• Distributed measurement-based quantum computation
• Deriving the correctness of quantum protocols in the probabilistic logic for quantum programs
• Reachability analysis of quantum Markov decision processes
• A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
• Commutativity of quantum weakest preconditions
• Generalised quantum weakest preconditions
• Termination of nondeterministic quantum programs
• Complete positivity and natural representation of quantum computations
• Infinite-Dimensionality in Quantum Foundations: W*-algebras as Presheaves over Matrix Algebras
• The expectation monad in quantum foundations
• Quantum temporal logic and reachability problems of matrix semigroups
• Dijkstra and Hoare monads in monadic computation
• Semantics for a quantum programming language by operator algebras
• Title not available (Why is that?)
• Dagger compact closed categories and completely positive maps (extended abstract)
• Quantum Hoare type theory: extended abstract
• Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
• Eigenlogic in the spirit of George Boole
• Toward automatic verification of quantum programs
• Quantum loop programs

This page was built for publication: Quantum weakest preconditions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5482269)