A formal language for expressing quantum predicates

Umut Yiğit Dural

Published Jan 1, 2025• 0 citations

Abstract

We develop a formal language, a syntax, for specifying quantum predicates, which are yes/no properties of quantum systems. Specifically we study classical-quantum predicates using projector-based Birkhoff-von Neumann quantum logic. We give an extensional definition of a weakest precondition calculus that preserves projector-based predicates fora simple loop-free classical-quantum programming language. We prove that our weakest precondition calculus is relatively complete in the sense of Cook for the classical-quantum programming language we specify. To achieve this, we show that for any post condition expressible in our formal language, the corresponding weakest precondition with respect to any program is also expressible in our formal language. This result establishes a foundation for reasoning about classical-quantum programs using an intensional approach.

DOI: 10.18154/rwth-2026-06832

Related papers

An Expressive Assertion Language for Quantum Programs

Bonan Su, Yuan Feng, Mingsheng Ying +1 more

In this paper, we define an assertion language designed for expectation-based reasoning about quantum programs. The key design idea is a representation of quantum predicates by quasi-probability distributions of generalized Pauli operators. Then we extend classical techniques such as Gödelization to prove that this language is expressive with respect to the quantum programs with loops–specifically, for any program S and any postcondition ψ formulated in the assertion language, the weakest precondition of S with respect to ψ can also be expressed as a formula in the assertion language. As an application, we present a sound and relatively complete quantum Hoare logic upon our expressive assertion language.

Proceedings of the ACM on Programming LanguagesJan 8, 20261 citation

Proof rules for purely quantum programs

Yuan Feng, Runyao Duan, Zhengfeng Ji +1 more

We apply the notion of quantum predicate proposed by D'Hondt and Panangaden to analyze a purely quantum language fragment which describes the quantum part of a future quantum computer in Knill's architecture. The denotational semantics, weakest precondition semantics, and weakest liberal precondition semantics of this language fragment are introduced. To help reasoning about quantum programs involving quantum loops, we extend proof rules for classical probabilistic programs to our purely quantum programs.

arXiv:cs/0507043Jul 18, 20054 citations

Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs

Mingsheng Ying

A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties (e.g. correctness) of quantum programs. Surprisingly, such a logic is missing in the literature, and the existing first-order Birkhoff-von Neumann quantum logic deals with only classical variables and quantifications over them. In this paper, we fill in this gap by introducing a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables. Examples are presented to show our logic is particularly suitable for specifying some important properties studied in quantum computation and quantum information. We further incorporate this logic into quantum Hoare logic as an assertion logic so that it can play a role similar to that of first-order logic for classical Hoare logic and BI-logic for separation logic. In particular, we show how it can be used to define and derive quantum generalisations of some adaptation rules that have been applied to significantly simplify verification of classical programs. It is expected that the assertion logic defined in this paper - first-order quantum logic with quantum variables - can be combined with various quantum program logics to serve as a solid logical foundation upon which verification tools can be built using proof assistants such as Coq and Isabelle/HOL.

arXiv:2205.01959May 4, 20221 citation

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 eBooksNov 30, 200935 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, 20260 citations

Birkhoff style proof systems for hybrid-dynamic quantum logic

Daniel Găină

We explore a simple approach to quantum logic based on hybrid and dynamic modal logic, where the set of states is given by some Hilbert space. In this setting, a notion of quantum clause is proposed in a similar way the notion of Horn clause is advanced in first-order logic, that is, to give logical properties for use in logic programming and formal specification. We propose proof rules for reasoning about quantum clauses and we investigate soundness and compactness properties that correspond to this proof calculus. Then we prove a Birkhoff completeness result for the fragment of hybrid-dynamic quantum logic determined by quantum clauses.

arXiv:2406.13360Jun 19, 20240 citations