Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Mathematical Structures in Computer Science

Quantum weakest preconditions

Ellie D’Hondt, Prakash Panangaden

Published Jun 1, 2006• 152 citations
Publisher

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 stabilisers.

DOI
10.1017/s0960129506005251

Related papers

Quantum Weakest Preconditions

Ellie D’Hondt, Prakash Panangaden

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.

arXiv:quant-ph/0501157•Jan 26, 2005•0 citations

Quantum weakest preconditions

Ellie D’Hondt, Prakash Panangaden

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 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.

Finds and Results from the Swedish Cyprus Expedition: A Gender Perspective at the Medelhavsmuseet•Jan 1, 2004•0 citations

Predicate Transformer Semantics of Quantum Programs

Mingsheng Ying, Runyao Duan, Yuan Feng +1 more

This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selinger's suggestion of representing quantum programs by superoperators and elucidates D'Hondt-Panangaden's theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoff-von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal conjunctivity and termination law of quantum programs are proved, and Hoare's induction rule is established in the quantum setting. 8.1 Introduction In the mid-1990s Shor and Grover discovered, respectively, the famous quantum factoring and searching algorithms. Their discoveries indicated that in principle quantum computers offer a way to accomplish certain computational tasks much more efficiently than classical computers, and thus stimulated an intensive investigation in quantum computation. Since then a substantial effort has been made to develop the theory of quantum computation, to find new quantum algorithms, and to exploit the physical techniques needed in building functional quantum computers, including in particular fault tolerance techniques. Currently, quantum algorithms are expressed mainly at the very low level of quantum circuits. In the history of classical computation, however, it was realized long time ago that programming languages provide a technique that allows us to think about a problem that we intend to solve in a high-level, conceptual way, rather than the details of implementation.

Cambridge University Press eBooks•Nov 30, 2009•35 citations

Natural Quantum Operational Semantics with Predicates

Marek Sawerwain, Roman Gielerak

Natural Quantum Operational Semantics with Predicates A general definition of a quantum predicate and quantum labelled transition systems for finite quantum computation systems is presented. The notion of a quantum predicate as a positive operator-valued measure is developed. The main results of this paper are a theorem about the existence of generalised predicates for quantum programs defined as completely positive maps and a theorem about the existence of a GSOS format for quantum labelled transition systems. The first theorem is a slight generalisation of D'Hondt and Panagaden's theorem about the quantum weakest precondition in terms of discrete support positive operator-valued measures.

International Journal of Applied Mathematics and Computer Science•Sep 1, 2008•10 citations

Predicatet transformers for nondeterministic quantum programs

Xi Wang

Nondeterminism has been introduced into quantum programming languages to model, for example, unspecified behavior. Weakest precondition transformers provide a formal framework for reasoning about program correctness with respect to a given postcondition. This thesis combines these ideas by introducing demonic and angelic interpretations of nondeterminism for quantum programs, together with corresponding weakest liberal precondition transformers. To capture angelic nondeterminism in a qualitative setting, we introduce predicates represented by sets of subspaces, where each subspace is represented by a projection. Such a predicate is satisfied whenever the quantum state belongs to one of the represented subspaces. We show, however, that natural definitions of the weakest liberal precondition transformer based on these predicates do not behave as desired for measurements and loops in the demonic setting. For this reason, the demonic weakest liberal precondition transformer is restricted to singleton postconditions. We further investigate the corresponding non-liberal weakest precondition transformers using termination spaces. This yields transformer rules for all language constructs except loops, for which deriving a transformer rule remains an open problem. Finally, we show that the resulting weakest precondition variants have the same relations as in the classical case.

•Jan 1, 2026•0 citations

Quantum Weakest Preconditions Revisited: Pre-expectations for Expected Runtime Analysis

Christina Gehnen, Dominique Unruh, Joost-Pieter Katoen

Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest preconditions from the perspective of expected runtime analysis of quantum programs and introduce a novel pre-expectation framework that enables to reason about the preconditions of quantum programs without the need of an upper bound. This is particularly interesting for quantum programs involving reward statements. The overall goal is to analyze runtime behavior even in the case of programs with potentially infinite expected runtime. This paper presents several ways to do so, e.g., a program transformation such that the expected runtime of a quantum program can be expressed using the weakest pre-expectation calculus with rewards.

cs.LOCross-listedarXiv:2607.12532•Jul 15, 2026•0 citations
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 stabilisers.
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.
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 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.
This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selinger's suggestion of representing quantum programs by superoperators and elucidates D'Hondt-Panangaden's theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoff-von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal conjunctivity and termination law of quantum programs are proved, and Hoare's induction rule is established in the quantum setting. 8.1 Introduction In the mid-1990s Shor and Grover discovered, respectively, the famous quantum factoring and searching algorithms. Their discoveries indicated that in principle quantum computers offer a way to accomplish certain computational tasks much more efficiently than classical computers, and thus stimulated an intensive investigation in quantum computation. Since then a substantial effort has been made to develop the theory of quantum computation, to find new quantum algorithms, and to exploit the physical techniques needed in building functional quantum computers, including in particular fault tolerance techniques. Currently, quantum algorithms are expressed mainly at the very low level of quantum circuits. In the history of classical computation, however, it was realized long time ago that programming languages provide a technique that allows us to think about a problem that we intend to solve in a high-level, conceptual way, rather than the details of implementation.
Natural Quantum Operational Semantics with Predicates A general definition of a quantum predicate and quantum labelled transition systems for finite quantum computation systems is presented. The notion of a quantum predicate as a positive operator-valued measure is developed. The main results of this paper are a theorem about the existence of generalised predicates for quantum programs defined as completely positive maps and a theorem about the existence of a GSOS format for quantum labelled transition systems. The first theorem is a slight generalisation of D'Hondt and Panagaden's theorem about the quantum weakest precondition in terms of discrete support positive operator-valued measures.
Nondeterminism has been introduced into quantum programming languages to model, for example, unspecified behavior. Weakest precondition transformers provide a formal framework for reasoning about program correctness with respect to a given postcondition. This thesis combines these ideas by introducing demonic and angelic interpretations of nondeterminism for quantum programs, together with corresponding weakest liberal precondition transformers. To capture angelic nondeterminism in a qualitative setting, we introduce predicates represented by sets of subspaces, where each subspace is represented by a projection. Such a predicate is satisfied whenever the quantum state belongs to one of the represented subspaces. We show, however, that natural definitions of the weakest liberal precondition transformer based on these predicates do not behave as desired for measurements and loops in the demonic setting. For this reason, the demonic weakest liberal precondition transformer is restricted to singleton postconditions. We further investigate the corresponding non-liberal weakest precondition transformers using termination spaces. This yields transformer rules for all language constructs except loops, for which deriving a transformer rule remains an open problem. Finally, we show that the resulting weakest precondition variants have the same relations as in the classical case.
Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest preconditions from the perspective of expected runtime analysis of quantum programs and introduce a novel pre-expectation framework that enables to reason about the preconditions of quantum programs without the need of an upper bound. This is particularly interesting for quantum programs involving reward statements. The overall goal is to analyze runtime behavior even in the case of programs with potentially infinite expected runtime. This paper presents several ways to do so, e.g., a program transformation such that the expected runtime of a quantum program can be expressed using the weakest pre-expectation calculus with rewards.