Bayesian Inference in Quantum Programs

Gehnen, Christina; Unruh, Dominique; Katoen, Joost-Pieter

doi:10.4230/LIPIcs.ICALP.2025.157

Bayesian Inference in Quantum Programs

Christina Gehnen

RWTH Aachen University, Germany Dominique Unruh

RWTH Aachen University, Germany
University of Tartu, Estonia Joost-Pieter Katoen

RWTH Aachen University, Germany

Abstract

Conditioning is a key feature in probabilistic programming to enable modeling the influence of data (also known as observations) to the probability distribution described by such programs. Determining the posterior distribution is also known as Bayesian inference. This paper equips a quantum while-language with conditioning, defines its denotational and operational semantics over infinite-dimensional Hilbert spaces, and shows their equivalence. We provide sufficient conditions for the existence of weakest (liberal) precondition-transformers and derive inductive characterizations of these transformers. It is shown how w(l)p-transformers can be used to assess the effect of Bayesian inference on (possibly diverging) quantum programs.

Keywords and phrases:

Quantum Program Logics, Weakest Preconditions, Bayesian Inference, Program Semantics

Category:

Track B: Automata, Logic, Semantics, and Theory of Programming

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Quantum information theory ; Theory of computation

\rightarrow

Logic and verification ; Theory of computation

\rightarrow

Program semantics

Related Version:

Full Version: https://arxiv.org/abs/2504.20732 [14]

Funding:

This work is supported by the ERC Grant 819317 CerQuS and the Interdisciplinary Doctoral Program in Quantum Systems Integration funded by the BMW group.

DOI:

10.4230/LIPIcs.ICALP.2025.157

Event:

52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Editors:

Keren Censor-Hillel, Fabrizio Grandoni, Joël Ouaknine, and Gabriele Puppis

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Quantum verification is a important part of the rapidly evolving field of quantum computing and information. The importance comes from several factors. Firstly, quantum computers operate in a completely different way than classical computers do. Principles of quantum mechanics are important to algorithm designers but in general unintuitive to most people. This leads to a higher risk of introducing logical errors. Secondly, quantum algorithms are often used in safely critical areas such as cryptography and optimization where those mistakes can lead to serious issues. Classical testing and debugging methods do not directly apply to quantum computing. Testing on quantum computers is challenging due to high execution costs, probabilistic outcomes, and noise from environmental interactions. While simulators help, they have limitations such as scalability. Debugging is also difficult, as measuring quantum variables alters their state, preventing traditional inspection methods.

Testing only verifies specific inputs without guaranteeing overall correctness, whereas formal verification ensures correctness for all inputs. Weakest preconditions define input states that ensure a given postcondition holds after execution. Inspired by the importance of conditioning and Bayesian inference in probabilistic programs, we extend the calculus from [7, 27] to incorporate “observations”. Combining weakest preconditions for total correctness and weakest liberal preconditions for partial correctness, we determine whether a predicate holds assuming all observations hold, i.e, compute a conditional probability.

This new statement could be used to aid in debugging to locate logical mistakes. Assume having a theoretical algorithm and a wrong implementation. To figure out which parts are wrong, fixing variable values by observations can help identify errors by comparing implementation samples with the expected distribution. Similarly, given a complex (possibly wrong) algorithm, adding observations can help understanding parts of the algorithm by comparing it to its intuitive understanding. For instance, in a random walk algorithm with a random starting point, analyzing success probability from a “good” starting point can help to understand the algorithm. Unlike traditional assertions, observations can be useful even when they don’t always hold. Another possible application is error correction, where outputs are often analysed assuming no more than $t$ qubit errors occurred per step to ensure successful error correction.

Related Work

The general idea of weakest preconditions was first developed by Dijkstra for classical programs [10, 9], then for probabilistic programs [16, 20] and later for quantum programs [7]. D’Hondt and Panangaden [7] defined predicates as positive operators as we do and focused on total correctness and finite-dimensional Hilbert spaces. [27] extended this approach to partial correctness and gave an explicit representation of the predicate transformer for the quantum while-language. An alternative to define predicates is to use projections [29]. There have been several extensions like adding classical variables [6, 13] or non-determinism [12].

A runtime assertion scheme using projective predicates for testing and debugging has been introduced in [18]. In contrast, our approach enables debugging, but in addition provides formal guarantees on the correctness based on the satisfaction of assertions and allows infinite-dimensional Hilbert spaces. A survey about studies and approaches of debugging of quantum programs is given in [8]. Another idea to locate bugs is to use incorrectness logic with projective predicates [26]. The idea of conditional weakest preconditions has been introduced in [22, 23] for probabilistic programs.

The concept of choosing specific measurement outcomes is also known as postselection. [1] shows that the class of problems solvable by quantum programs with postselection in polynomial time, called Postselected Bounded-Error Quantum Polynomial-Time (PostBQP), is the same as the ones in the complexity class Probabilistic Polynomial-Time (PP). This equivalence is shown by solving a representative PP-complete problem, MAJ-SAT, using a quantum program with postselection. We confirm the correctness of this program in Section 5 by using conditional weakest preconditions.

Main Contributions

$\blacksquare$

Conditional weakest-precondition transformers: We define a weakest precondition calculus for reasoning about programs with an “observe” statement. The conditional weakest precondition, defined in terms of weakest (liberal) preconditions transformers, reveals the probability of a postcondition given all observations succeed.

The definition of the transformers is semantic, i.e., formulated in a generic way based on the denotational semantics and not tied to a specific syntax of programs (but we also give explicit rules for our syntax by recursion over the structure of a program).
$\blacksquare$

Semantics: We develop both denotational and operational semantics of a simple quantum while-language with “observe” statements and show their equivalence.
$\blacksquare$

Our definition of weakest (liberal) preconditions is a conservative extension of [27], supporting “observe” statements. Further differences include: Our definition is semantic and we support infinite-dimensional quantum systems (e.g., to support quantum integers)¹¹1Notice that [27] also defines a language with quantum integers. However, they do not explicitly specify the various notions of convergence of operators (e.g., operator topologies, convergence of infinite sums, existence of suprema), making it difficult to verify whether their rules are sound in the infinite-dimensional case..

Structure

We first recall important definitions in Section 2. The main contributions are in Section 3 and Section 4: Section 3 introduces the “observe” statement and its semantics whereas Section 4 defines weakest (liberal) preconditions and finally conditional weakest (liberal) preconditions. Two examples in Section 5 illustrate our approach, followed by conclusions in Section 6.

2 Preliminaries

2.1 Hilbert Spaces

Let $\langle\cdot\mid\cdot\rangle$ denote the inner product over a vector space $\mathcal{V}$ . The norm (or length) of a vector $u$ , denoted $\|u\|$ , is defined as $\sqrt{\langle u\mid u\rangle}$ . The vector $u$ is called a unit vector if $\|u\|=1$ . Vectors $u, v$ are orthogonal ( $u\bot v$ ) if $\langle u\mid v\rangle=0$ . The sequence $\{u_{i}\}_{i\in\mathbb{N}}$ of vectors $u_{i}\in\mathcal{V}$ is a Cauchy sequence, if for any $\epsilon>0$ , there exists a positive integer $N$ such that $\|u_{n}-u_{m}\|<\epsilon$ for all $n,m\geq N$ . If for any $\epsilon>0$ , there exists a positive integer $N$ such that $\|u_{n}-u\|<\epsilon$ for all $n\geq N$ , then $u$ is the limit of $\{u_{i}\}_{i\in\mathbb{N}}$ , denoted $u=\lim_{i\to\infty}u_{i}$ .

A family $\{u_{i}\}_{i\in I}$ of vectors in $\mathcal{V}$ is summable with the sum $v=\sum_{i\in I}u_{i}$ if for every $\epsilon>0$ there exists a finite $J\subseteq I$ such that $\|v-\sum_{i\in K}u_{i}\|<\epsilon$ for every finite $K\subseteq I$ and $J\subseteq K$ .

A Hilbert space $\mathcal{H}$ is a complete inner product space, i.e, every Cauchy sequence of vectors in $\mathcal{H}$ has a limit [27]. An orthonormal basis of a Hilbert space $\mathcal{H}$ is a (possibly infinite) family $\{u_{i}\}_{i\in I}$ of unit vectors if they are pairwise orthogonal (i.e., $u_{i}\bot u_{j}$ for $i\neq j,i,j\in I$ ) and every $v\in\mathcal{H}$ can be written as $v=\sum_{i\in I}\langle u_{i}\mid v\rangle\cdot u_{i}$ (in the sense above). The cardinality of $I$ , denoted $\absolutevalue{I}$ , is the dimension of $\mathcal{H}$ . Hilbert spaces and its elements can be combined using the tensor product $\otimes$ [24, Def. IV.1.2].

We use Dirac notation $\ket{\phi}$ to denote vectors of a vector space where $\bra{\phi}$ is the dual vector of $\ket{\phi}$ [11], i.e., $\bra{\phi}=\ket{\phi}^{\dagger}$ .

Example 1.

A typical Hilbert space over the set $X$ is

\displaystyle l^{2}(X)=\{\sum_{n\in X}\alpha_{n}\ket{n}\mid\alpha_{n}\in% \mathbb{C}\text{ for all }n\in X\text{ and }\sum_{n\in X}\absolutevalue{\alpha% _{n}}^{2}<\infty\}

where the inner product is defined as $(\sum_{n\in X}\alpha_{n}\ket{n},\sum_{n\in X}\alpha^{\prime}_{n}\ket{n})=\sum_% {n\in X}\overline{\alpha_{n}}\alpha^{\prime}_{n}$ . By $\overline{x+yi}=x-yi$ we denote the complex conjugate of $x+yi\in\mathbb{C}$ . An orthonormal basis, also called computational basis, is $\{\ket{n}\mid n\in X\}$ . For (countably) infinite sets $X$ , the basis is (countably) infinite and thus $l^{2}(X)$ is a (countably) infinite Hilbert space. $l^{2}(\mathbb{Z})$ can be used for quantum integers and is also denoted by $\mathcal{H}_{\infty}$ . For qubits, we use $l^{2}(\{0,1\})$ and denote it as $\mathcal{H}_{2}$ .

2.2 Operators

In the following, all vector spaces will be over $\mathbb{C}$ . For vector spaces $\mathcal{V},\mathcal{W}$ , a function $f:\mathcal{V}\to\mathcal{W}$ is called linear if $f(ax+y)=af(x)+f(y)$ for $x,y\in\mathcal{V}$ and $a\in\mathbb{C}$ . If $\mathcal{V},\mathcal{W}$ are normed vector spaces then $f$ is called bounded linear if $f$ is linear and $\norm{f(x)}\leq c\cdot\norm{x}$ for some constant $c\geq 0$ for all $x\in\mathcal{V}$ . If $\mathcal{H}$ is a Hilbert space, we call bounded linear functions on $\mathcal{H}\to\mathcal{H}$ operators. Let $B(\mathcal{H})$ denote the space of all operators on $\mathcal{H}$ and $A\ket{\phi}$ the result of applying operator $A$ to $\ket{\phi}\in\mathcal{H}$ . For this work, we additionally generalize the notion of linearity to functions that are defined on subsets of the vector space: For (normed) vector spaces $S\subseteq\mathcal{V},T\subseteq\mathcal{W}$ with $\mathit{span}(S)=\mathcal{V}$ and $\mathit{span}(T)=\mathcal{W}$ , we call $f:S\to T$ (bounded) linear iff there exists a (bounded) linear function $\bar{f}:\mathcal{V}\to\mathcal{W}$ such that $\bar{f}(s)=f(s)$ for $s\in S$ . $\mathit{span}(S)$ includes all finite linear combinations of $S$ .

Let $A$ and $B$ be operators on $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$ with $\ket{\phi}\in\mathcal{H}_{1},\ket{\psi}\in\mathcal{H}_{2}$ . By [24, Def. IV.1.3], the tensor product $A\otimes B$ is the unique operator that satisfies $(A\otimes B)(\ket{\phi}\otimes\ket{\psi})=A\ket{\phi}\otimes B\ket{\psi}$ For matrices, the tensor product is also called the Kronecker product.

For every operator $A$ on $\mathcal{H}$ , there exists an operator $A^{\dagger}$ on $\mathcal{H}$ with $\langle\ket{\phi},A\ket{\psi}\rangle=\langle A^{\dagger}\ket{\phi},\ket{\psi}\rangle$ for all $\ket{\phi},\ket{\psi}\in\mathcal{H}$ . An operator $A$ on $\mathcal{H}$ is called positive if $\bra{\psi}A\ket{\psi}\geq 0$ for all states $\ket{\psi}\in\mathcal{H}$ [21]. The identity operator $\textbf{I}_{\mathcal{H}}$ on $\mathcal{H}$ is defined by $\textbf{I}_{\mathcal{H}}\ket{\phi}=\ket{\phi}$ . The zero operator on $\mathcal{H}$ , denoted by $\mathbf{0}_{\mathcal{H}}$ , maps every vector to the zero vector. We omit $\mathcal{H}$ if it is clear from the context. An unitary operator $U$ is an operator such that its inverse is its adjoint $U^{-1}=U^{\dagger}$ , i.e., $U^{\dagger}U=\textbf{I}$ and $UU^{\dagger}=\textbf{I}$ [17]. An (ortho)projector is an operator $P:\mathcal{H}\to\mathcal{H}$ such that $P^{2}=P=P^{\dagger}$ . For every closed subspace $S$ , there exists a projector $P_{S}$ with image $S$ [5, Prop. II.3.2 (b)].

An operator $A$ is a trace class operator if there exists an orthonormal basis $\{\ket{\psi_{i}}\}_{i\in I}$ such that $\{\bra{\psi_{i}}\cdot\absolutevalue{A}\cdot\ket{\psi_{i}}\}_{i\in I}$ is summable where $\absolutevalue{A}$ is the unique positive operator $B$ with $B^{\dagger}B=A^{\dagger}A$ . Then the trace of $A$ is defined as $tr(A)=\sum_{i\in I}\bra{\psi_{i}}\cdot A\cdot\ket{\psi_{i}}$ where $\{\ket{\psi_{i}}\}_{i\in I}$ is an orthonormal basis. For a trace class operator $A$ , it can be shown that $tr(A)$ is independent of the chosen base [27]. The trace is cyclic, i.e., $tr(AB)=tr(BA)$ [25], linear, i.e., $tr(A+B)=tr(A)+tr(B)$ , scalar, i.e., $tr(cA)=c\cdot tr(A)$ for a constant $c$ [4] and multiplicative, i.e., $tr(A\otimes B)=tr(A)tr(B)$ holds [25] for trace class operators $A, B$ . We use $T(\mathcal{H})$ to denote the space of trace class operators on $\mathcal{H}$ . Positive trace class operators with $tr(\rho)\leq 1$ are called partial density operators. The set of partial density operators is denoted $\mathcal{D}^{-}(\mathcal{H})$ with $\mathit{span}(\mathcal{D}^{-}(\mathcal{H}))=T(\mathcal{H})$ . Density operators are partial density operators with $tr(\rho)=1$ . They are denoted as $\mathcal{D}(\mathcal{H})$ . The support of a partial density operator $\rho$ is the smallest closed subspace $S$ such that $P_{S}\rho P_{S}=\rho$ .

Let us consider some properties of functions that map operators to operators. $f:T_{1}\to T_{2}$ with $T_{1}\subseteq T(\mathcal{H}_{1}),T_{2}\subseteq T(\mathcal{H}_{2})$ is trace-reducing if $tr(f(\rho))\leq tr(\rho)$ for all positive $\rho\in T_{1}$ . $f:B_{1}\subseteq B(\mathcal{H}_{1})\to B_{2}\subseteq B(\mathcal{H}_{2})$ is positive if $f(a)$ is positive for positive $a\in B_{1}$ and subunital if $f(\textbf{I}_{\mathcal{H}_{1}})\sqsubseteq\textbf{I}_{\mathcal{H}_{2}}$ and $\textbf{I}_{\mathcal{H}_{1}}\in B_{1}$ , where $\sqsubseteq$ is defined just below.

2.2.1 The Loewner Partial Order

To order operators, the Loewner partial order is used. For any operators $A, B$ , it is defined by $A\sqsubseteq B$ iff $B-A$ is a positive operator. This is equivalent to $tr(A\rho)\leq tr(B\rho)$ for all partial density operators $\rho\in\mathcal{D}^{-}(\mathcal{H})$ [27]. The Loewner order is compatible w.r.t. addition (also known as monotonic), i.e., $A\sqsubseteq B$ implies $A+C\sqsubseteq B+C$ for any $C$ , and w.r.t. multiplication of non-negative scalars, i.e., $A\sqsubseteq B$ implies $cA\sqsubseteq cB$ for $c\geq 0$ [3].

Using this order, we can define predicates [7]. A quantum predicate on a Hilbert space $\mathcal{H}$ is defined as an operator $P$ on $\mathcal{H}$ with $\mathbf{0}_{\mathcal{H}}\sqsubseteq P\sqsubseteq\textbf{I}_{\mathcal{H}}$ . The set of quantum predicates on $\mathcal{H}$ is denoted by $\mathcal{P}(\mathcal{H})$ and $\mathit{span}(\mathcal{P}(\mathcal{H}))=B(\mathcal{H})$ .

The Loewner partial order is an $\omega$ -complete partial order ( $\omega$ -cpo) on the set of partial density operators [28]. Thus each increasing sequence of partial density operators has a least upper bound. This also holds for the set of predicates [7].

An important property that we need is continuity of the trace operator. First of all, we note that the trace-operator is order-continuous on partial density operators with respect to $\sqsubseteq$ , i.e., $\bigvee_{i\in\mathbb{N}}tr(\rho_{i})=tr(\bigvee_{i\in\mathbb{N}}\rho_{i})$ for any increasing sequence of partial density operators $\{\rho_{i}\}_{i\in\mathbb{N}}$ . Without going further into details, this holds because for an increasing sequence of real numbers, the least upper bound and the limit coincide, the same also holds for partial density operators [25] and because the trace is linear and bounded, it is also trace-norm continuous. Continuity w.r.t. predicates means $\bigvee_{i\in\mathbb{N}}tr(P_{i}\rho)=tr((\bigvee_{i\in\mathbb{N}}P_{i})\rho)$ for every $\rho\in\mathcal{D}^{-}(\mathcal{H})$ and increasing sequence of predicates $\{P_{i}\}_{i\in\mathbb{N}}$ . Without going into further detail, we can show that a function $f:\mathcal{B}(\mathcal{H})\to\mathbb{C}$ defined by $f(A)=tr(A\rho)$ for a fixed $\rho\in\mathcal{D}^{-}(\mathcal{H})$ is weak^∗-continuous and convergence of positive bounded operators in the weak^∗-topology coincides with the supremum [25]. Similar, the same property holds for decreasing sequences of predicates $\{P_{i}\}_{i\in\mathbb{N}}$ and the greatest lower bound $\bigwedge_{i\in\mathbb{N}}P_{i}$ .

2.3 Quantum-specific Preliminaries

Due to a postulate of quantum mechanics, the state space of an isolated quantum system can be described as a Hilbert space where states correspond to unit vectors (up to a phase shift) in its state space [27]. A quantum state is called pure if it can be described by a vector in the Hilbert space; otherwise mixed, i.e., it is a probabilistic distribution over pure states. We use partial density operators to describe mixed states, in particular to capture the current state of a program. If a quantum system is in a pure state $\ket{\psi_{i}}$ with probability $p_{i}$ (with $\sum_{i}p_{i}\leq 1$ ), then this is represented by the partial density operator $\rho=\sum_{i}p_{i}\ket{\psi_{i}}\bra{\psi_{i}}$ .

To obtain the current value of e.g. a quantum variable, we cannot simply look at it. In quantum mechanics, each measurement can impact the current state of a qubit.

A measurement is a (possible infinite) family of operators $\{M_{m}\}_{m\in I}$ where $m$ is the measurement outcome and $\sum_{m\in I}M_{m}^{\dagger}M_{m}=\textbf{I}$ ¹¹1As in [25], we mean convergence of sums with respect to SOT (strong operator topology) which is the topology where $\lim_{i\to\infty}a_{i}=a$ holds iff for all $\phi$ : $\lim_{i\to\infty}a_{i}\phi=a\phi$ [5, Prop. IX.1.3(c)].. If the quantum system is in state $\rho\in\mathcal{D}^{-}(\mathcal{H})$ before the measurement $\{M_{m}\}$ , then the probability for result $m$ is $p(m)=tr(M_{m}\rho M^{\dagger}_{m})$ and the post-measurement state is $\rho_{m}=\frac{M_{m}\rho M^{\dagger}_{m}}{p(m)}$ . An important kind of measurement is the projective measurement. It is a set of projections $\{P_{m}\}$ over $\mathcal{H}$ with $\sum_{m}P_{m}=\textbf{I}$ . An important property of projective measurements is that if a state $\rho$ is measured by a projective measurement $\{P,I-P\}$ and $supp(\rho)\subseteq P$ holds, then $\rho$ is not changed.

2.4 Markov Chains

A Markov chain (MC) is a tuple $\mathcal{M}=(\Sigma,\textbf{P},s_{init})$ where

$\blacksquare$

$\Sigma$ is a nonempty (possibly uncountable) set of states,
$\blacksquare$

$\textbf{P}:\Sigma\times\Sigma\rightarrow[0,1]$ with $\sum_{s^{\prime}\in\Sigma}\textbf{P}(s,s^{\prime})=1$ is the transition probability function. Let $s\overset{p}{\rightarrow}s^{\prime}$ denote $\textbf{P}(s,s^{\prime})=p$ .
$\blacksquare$

$s_{init}\in\Sigma$ is the initial state.

Note that in comparison to [2, 23], $\Sigma$ can be uncountable. However, in our setting the reachable set of states will be countable as every state $s$ can only have a countable number of successor states $s^{\prime}$ with $\textbf{P}(s,s^{\prime})>0$ . Therefore, even if $\Sigma$ is uncountable, the set of reachable states is countable and all results from [2, 23] still apply.

A path of a MC $\mathcal{M}$ is an infinite sequence $s_{0}s_{1}s_{2}\ldots\in\Sigma^{\omega}$ with $s_{0}=s_{init}$ and $\textbf{P}(s_{i},s_{i+1})>0$ for all $i$ . We use $\mathit{Paths}(\mathcal{M})$ to denote the set of paths in $\mathcal{M}$ and $\mathit{Paths}_{\mathit{fin}}(\mathcal{M})$ for the finite path prefixes. If it is clear from the context, we omit $\mathcal{M}$ . The probability distribution $Pr^{\mathcal{M}}$ on $\mathit{Paths}(\mathcal{M})$ is defined using cylinder sets as in [2]. In a slight abuse of notation, we write $Pr^{\mathcal{M}}(\hat{\pi})$ for $Pr^{\mathcal{M}}(Cyl(\hat{\pi}))$ for $\hat{\pi}\in\mathit{Paths}_{\mathit{fin}}(\mathcal{M})$ where $Cyl(\hat{\pi})$ denotes the cylinder set of $\hat{\pi}$ . We write $s_{0}\rightarrow_{p}^{*}s_{n}$ where $p=\sum_{s_{0}\ldots s_{n}\in\mathit{Paths}_{\mathit{fin}}(\mathcal{M})}\textbf% {P}(s_{0}\ldots s_{n})$ is the probability to reach $s_{n}$ from $s_{0}$ . Given a target set of reachable states $T\subseteq\Sigma$ , let $\lozenge T$ be the (measurable) set of infinite paths that reach the target set $T$ . The probability of reaching $T$ is $Pr^{\mathcal{M}}(\lozenge T)=\sum_{\hat{\pi}\in\mathit{Paths}_{\mathit{fin}}(% \mathcal{M})\cap(\Sigma\backslash T)^{*}T}Pr^{\mathcal{M}}(\hat{\pi})$ . Analogously, let $\neg\lozenge T$ be the set of paths that never reach $T$ ; $Pr^{\mathcal{M}}(\neg\lozenge T)=1-Pr^{\mathcal{M}}(\lozenge T)$ .

3 Quantum Programs with Observations

We assume $\mathit{Var}$ to be a finite set of quantum variables with two types: Boolean and integer. As in [27], the corresponding Hilbert spaces are

	$\displaystyle\mathcal{H}_{2}=\{\alpha\ket{0}+\beta\ket{1}\mid\alpha,\beta\in% \mathbb{C}\},$
	$\displaystyle\mathcal{H}_{\infty}=\Big{\{}\sum_{n\in\mathbb{Z}}\alpha_{n}\ket{% n}\mid\alpha_{n}\in\mathbb{C}\text{ for all }n\in\mathbb{Z}\text{ and }\sum_{n% \in\mathbb{Z}}\absolutevalue{\alpha_{n}}^{2}<\infty\Big{\}}.$

Each variable $q\in\mathit{Var}$ has a type $type(q)\in\{\mathit{Bool},\mathit{Int}\}$ . Its state space $\mathcal{H}_{q}$ is $\mathcal{H}_{2}$ if $type(q)=\mathit{Bool}$ and $\mathcal{H}_{\infty}$ otherwise. The state space of a quantum register $\bar{q}=q_{1},...,q_{n}$ is defined by the tensor product $\mathcal{H}_{\bar{q}}=\bigotimes_{i=1}^{n}\mathcal{H}_{q_{i}}$ of state spaces of $q_{1}$ through $q_{n}$ .

3.1 Syntax

A quantum while-program has the following syntax:

S::=\mathbf{skip}\mid q:=0\mid\overline{q}:=U\overline{q}\mid\mathbf{observe}% \text{ }(\bar{q},O)\mid S_{1};S_{2}\mid\mathbf{measure}\text{ }M[\bar{q}]:\bar% {S}\mid\mathbf{while}\text{ }M[\bar{q}]=1\text{ }\mathbf{do}\text{ }S

where

$\blacksquare$

$q$ is a quantum variable,
$\blacksquare$

$\bar{q}$ is a quantum register,
$\blacksquare$

$U$ from statement $\overline{q}:=U\overline{q}$ is a unitary operator on $\mathcal{H}_{\bar{q}}$ and $\bar{q}$ is the same on both sides,
$\blacksquare$

$O$ in $\mathbf{observe}\text{ }(\bar{q},O)$ is a projection on $\mathcal{H}_{\bar{q}}$
$\blacksquare$

the measurement $M=\{M_{m}\}_{m\in I}$ in $\mathbf{measure}\text{ }M[\bar{q}]:\bar{S}$ is on $\mathcal{H}_{\bar{q}}$ and $\bar{S}=\{S_{m}\}_{m\in I}$ is a family of quantum programs where each $S_{m}$ corresponds to an outcome $m\in I$ ,
$\blacksquare$

the measurement in $\mathbf{while}\text{ }M[\bar{q}]=1\text{ }\mathbf{do}\text{ }S$ on $\mathcal{H}_{\bar{q}}$ has the form $M=\{M_{0},M_{1}\}$ .

Our programs extend [27] with the new statement $\mathbf{observe}\text{ }(\bar{q},O)$ . We only allow projective predicates $O$ for observations. It is conceivable that it can also be based on more general predicates $O\in\mathcal{P}(\mathcal{H})$ but it is not clear what the intuitive operational meaning of such $O$ would be, so we choose to pursue the simpler case.

We use $\mathbf{if}\text{ }M[\bar{q}]=1\text{ }\mathbf{then}\text{ }S_{1}\text{ }% \mathbf{else}\text{ }S_{0}$ as syntactic sugar for a measurement statement with $M=\{M_{0},M_{1}\}$ and $\bar{S}=\{S_{0},S_{1}\}$ .

By $\equiv$ we denote syntactic equality of quantum programs. We use $\mathit{var}(S)$ to denote the set of variables occurring in program $S$ . The Hilbert space of $\mathit{var}(S)$ is denoted by $\mathcal{H}_{\mathit{all}}$ . If the set of variables is clear from the context, we just write $\mathcal{H}$ .

For $\bar{q}=q_{1},...,q_{n}$ and operator $A$ on $\mathcal{H}_{\bar{q}}$ , we define its cylinder extension by $A\otimes I_{Var\backslash\{\bar{q}\}}$ on $\mathcal{H}_{all}$ and abbreviate it by $A$ if it is clear from the context. Let $\ket{\phi}\bra{\psi}_{q}$ denote the value of quantum variable $q$ in the state $\ket{\phi}\bra{\psi}$ . We sometimes refer to it meaning its cylinder extension on $\mathcal{H}_{\mathit{all}}$ [27]. This notation is equivalent to $q(\ket{\phi}\bra{\psi})$ in [25].

3.2 Semantics

In this section, we define an operational and denotational semantics for quantum while-programs with observations and show their equivalence.

Figure 1: Transition probability function of MC

\mathfrak{R}_{\rho}\llbracket S\rrbracket

for all

\sigma\in\mathcal{D}(\mathcal{H})

where

\downarrow;S_{2}\equiv S_{2}

.

3.2.1 Operational Semantics

We start by defining the operational semantics of a program $S$ as a Markov chain inspired by [23] instead of non-deterministic relations in comparison to [27]. A quantum configuration is a tuple $\langle S,\rho\rangle$ with density operator $\rho\in\mathcal{D}(\mathcal{H})$ . Note that we consider normalized density operators $\mathcal{D}(\mathcal{H})$ instead of partial density operators $\mathcal{D}^{-}(\mathcal{H})$ . Intuitively, $S$ is the program that is left to evaluate and $\rho$ is the current state. We use $\downarrow$ to denote that there is no program left to evaluate. The set of all configurations over $\mathcal{H}$ is denoted as $\mathcal{C}(\mathcal{H})$ . The quantum configuration for violated observations is $\langle\lightning\rangle$ and for termination is $\langle sink\rangle$ .

Definition 2.

The operational semantics of a program $S$ with initial state $\rho\in\mathcal{D}(\mathcal{H})$ is defined as the Markov chain $\mathfrak{R}_{\rho}\llbracket S\rrbracket=(\Sigma,\textbf{P},s_{init})$ where:

$\blacksquare$

$\Sigma=\mathcal{C}(\mathcal{H})\cup\{\langle\lightning\rangle,\langle sink\rangle\}$ ,
$\blacksquare$

$s_{init}=\langle S,\rho\rangle$ ,
$\blacksquare$

P is the smallest function satisfying the inference rules in Figure 1 where $c\overset{p}{\rightarrow}c^{\prime}$ means $\textbf{P}(c,c^{\prime})=p>0$ . For all other pairs of states the transition probability is $0$ .

The meaning of a transition $\langle S,\sigma\rangle\overset{p}{\rightarrow}\langle S^{\prime},\sigma^{% \prime}\rangle$ is that after evaluating program $S$ on state $\sigma$ , with probability $p$ the new state is $\sigma^{\prime}$ and the program left to execute is $S^{\prime}$ . For the observe statement, there are two successors, $\langle\mathbf{observe}\text{ }(\bar{q},O),\sigma\rangle\overset{tr(O\sigma O^% {\dagger})}{\rightarrow}\langle\downarrow,\frac{O\sigma O^{\dagger}}{tr(O% \sigma O^{\dagger})}\rangle$ and $\langle\mathbf{observe}\text{ }(\bar{q},O),\sigma\rangle\overset{1-tr(O\sigma O% ^{\dagger})}{\rightarrow}\langle\lightning\rangle$ . The observation $O$ is satisfied by state $\sigma$ with probability $tr(O\sigma O^{\dagger})$ and then it terminates successfully. If the observation is violated (with probability $1-tr(O\sigma O^{\dagger})$ ), the successor state is $\langle\lightning\rangle$ , the state that captures paths with violated observations. For details of the other rules we refer to [27].

3.2.2 Denotational Semantics

We now provide a denotational semantics for quantum while-programs. To handle observations and distinguish between non-terminating runs and those that violate observations, we introduce denotational semantics in a slightly different way than [27]. To do so, we start with defining some basics:

For tuples $(\rho,p),(\sigma,q)\in\mathcal{D}^{-}(\mathcal{H})\times\mathbb{R}_{\geq 0}$ , we define multiplication with a constant $a\in\mathbb{R}_{\geq 0}$ and addition entrywise: $a(\rho,p):=(a\rho,ap)$ and $(\rho,p)+(\sigma,q):=(\rho+\sigma,p+q)$ .

The least upper bound (lub) of a set of tuples is defined as the entrywise lub provided it exists, i.e., $\bigvee_{n=0}^{\infty}(\rho_{n},p_{n}):=(\bigvee_{n=0}^{\infty}\rho_{n},% \bigvee_{n=0}^{\infty}p_{n})$ where $\bigvee_{n=0}^{\infty}\rho_{n}$ is the lub w.r.t. the Loewner partial order $\sqsubseteq$ and $\bigvee_{n=0}^{\infty}p_{n}$ is the lub w.r.t. to the classical ordering $\leq$ on $\mathbb{R}_{\geq 0}$ .

As the probability of violating observations depends on the density operator, we introduce

\mathcal{D}\mathcal{R}=\{(\rho,p)\in\mathcal{D}^{-}(\mathcal{H})\times\mathbb{% R}_{\geq 0}\mid tr(\rho)+p\leq 1\}\subseteq T(\mathcal{H})\times\mathbb{C}.

$T(\mathcal{H})\times\mathbb{C}$ is isomorphic to the set of operators of the form $\begin{pmatrix}\rho&\\ &p\end{pmatrix}\in T(\mathcal{H}\otimes\mathbb{C})$ . Thus the trace and the norm from $T(\mathcal{H}\otimes\mathbb{C})$ apply. Specifically, $\tilde{tr}(\rho,p):=tr(\rho)+p$ and $\norm*{(\rho,p)}:=\norm*{\rho}+\absolutevalue*{p}$ for $(\rho,p)\in T(\mathcal{H})\times\mathbb{C}$ .

Definition 3.

The denotational semantics of a quantum program $S$ is defined as a mapping $\llbracket S\rrbracket:\mathcal{D}\mathcal{R}\to\mathcal{D}\mathcal{R}$ . For $(\rho,p)\in\mathcal{D}\mathcal{R}$ , $\rho$ is used for density-transformer semantics as defined in [27] and $p$ for the probability of an observation violation.

The denotational semantics for $(\rho,p)\in\mathcal{D}\mathcal{R}$ is given by

$\blacksquare$

$\llbracket\mathbf{skip}\rrbracket(\rho,p)=(\rho,p)$ .
$\blacksquare$

$\llbracket q:=0\rrbracket(\rho,p)=\begin{cases}(\ket{0}\bra{0}_{q}\rho\ket{0}% \bra{0}_{q}+\ket{0}\bra{1}_{q}\rho\ket{1}\bra{0}_{q},p)&\text{, if }type(q)=% \mathit{Bool}\\ (\sum_{n\in\mathbb{Z}}\ket{0}\bra{n}_{q}\rho\ket{n}\bra{0}_{q},p)&\text{, if }% type(q)=\mathit{Int}.\end{cases}$
$\blacksquare$

$\llbracket\overline{q}:=U\overline{q}\rrbracket(\rho,p)=(U\rho U^{\dagger},p)$ .
$\blacksquare$

$\llbracket\mathbf{observe}\text{ }(\bar{q},O)\rrbracket(\rho,p)=(O\rho O^{% \dagger},p+tr(\rho)-tr(O\rho O^{\dagger}))$ .
$\blacksquare$

$\llbracket S_{1};S_{2}\rrbracket(\rho,p)=\llbracket S_{2}\rrbracket(\llbracket S% _{1}\rrbracket(\rho,p))$ .
$\blacksquare$

$\llbracket\mathbf{measure}\text{ }M[\bar{q}]:\bar{S}\rrbracket(\rho,p)=\sum_{m% }\llbracket S_{m}\rrbracket(M_{m}\rho M_{m}^{\dagger},0)+(\mathbf{0},p)$ with $M=\{M_{m}\}_{m\in I}$ and $\bar{S}=\{S_{m}\}_{m\in I}$ .

\blacksquare

$\llbracket\mathbf{while}\text{ }M[\bar{q}]=1\text{ }\mathbf{do}\text{ }S% \rrbracket(\rho,p)=\bigvee_{n=0}^{\infty}\llbracket(\mathbf{while}\text{ }M[% \bar{q}]=1\text{ }\mathbf{do}\text{ }S)^{n}\rrbracket(\rho,p)$ with $M=\{M_{0},M_{1}\}$ where loop unfoldings are defined inductively

	$\displaystyle(\mathbf{while}\text{ }M[\bar{q}]=1\text{ }\mathbf{do}\text{ }S)^% {0}$	$\displaystyle\equiv\Omega$
	$\displaystyle(\mathbf{while}\text{ }M[\bar{q}]=1\text{ }\mathbf{do}\text{ }S)^% {n+1}$	$\displaystyle\equiv\mathbf{if}\text{ }M[\bar{q}]=1\text{ }\mathbf{then}\text{ % }S;(\mathbf{while}\text{ }M[\bar{q}]=1\text{ }\mathbf{do}\text{ }S)^{n}\text{ % }\mathbf{else}\text{ }\mathbf{skip}$

where $\Omega$ is a syntactic quantum program with $\llbracket\Omega\rrbracket(\rho,p)=(\mathbf{0},p)$ as in [27].

We write $\llbracket S\rrbracket_{\rho}(\rho,p)$ and $\llbracket S\rrbracket_{\lightning}(\rho,p)$ to denote the first/second component of $\llbracket S\rrbracket(\rho,p)$ . It follows directly that our definition is a conservative extension of [27]:

Proposition 4.

For an observe-free program $S$ , input state $\rho\in\mathcal{D}^{-}(\mathcal{H})$ and $p\in\mathbb{R}_{\geq 0}$ , is $\llbracket S\rrbracket(\rho,p)=(\llbracket S\rrbracket_{og}(\rho),p)$ where $\llbracket S\rrbracket_{og}(\rho)$ is the denotational semantics as defined in [27].

Some intuition behind those tuples: If $\llbracket S\rrbracket(\rho,0)=(\rho^{\prime},p^{\prime})$ for a program $S$ with initial pair $(\rho,0)$ , then the probability of violating an observation while executing $S$ on $\rho\in\mathcal{D}(\mathcal{H})$ is $p^{\prime}$ . The probability of terminating normally (without violating an observation) is given by $tr(\rho^{\prime})$ and the probability for non-termination is $1-tr(\rho^{\prime})-p^{\prime}$ . As in the observe-free case, $\rho^{\prime}$ is the (non-normalized) state after $S$ has been executed (and terminated) on $\rho$ . It is easy to see that only the observation statement can change the value of the second entry.

Proposition 5.

For $(\rho,p),(\rho,q)\in\mathcal{D}\mathcal{R}$ and program $S$ :

1.

$\llbracket S\rrbracket_{\rho}(\rho,p)=\llbracket S\rrbracket_{\rho}(\rho,q)$
2.

$p\leq\llbracket S\rrbracket_{\lightning}(\rho,p)$
3.

if $(\rho,q+p)\in\mathcal{D}\mathcal{R}$ then $\llbracket S\rrbracket_{\lightning}(\rho,q+p)=\llbracket S\rrbracket_{% \lightning}(\rho,q)+p$
4.

$\tilde{tr}(\llbracket S\rrbracket(\rho,p))\leq\tilde{tr}(\rho,p)$
5.

$\llbracket S\rrbracket$ is well defined, i.e., $\llbracket S\rrbracket(\rho,p)\in\mathcal{D}\mathcal{R}$ and the least upper bound exists.
6.

$\llbracket S\rrbracket$ is linear

Proof.

All claims can be shown by doing an induction over $S$ , see [14]. $\hfill\blacktriangleleft$ As $\llbracket S\rrbracket_{\rho}(\rho,p)=\llbracket S\rrbracket_{\rho}(\rho,q)$ , we use $\llbracket S\rrbracket_{\rho}(\rho)$ instead. Three consequences of Proposition 5:

Lemma 6.

For $(\rho,p),(\sigma,q)\in\mathcal{D}\mathcal{R}$ with $(\rho+\sigma,p+q)\in\mathcal{D}\mathcal{R}$ and programs $S,S_{1},S_{2}$ :

1.

$tr(\llbracket S\rrbracket_{\rho}(\rho,p))\leq tr(\rho)$ , i.e., $\llbracket S\rrbracket_{\rho}$ is trace-reducing
2.

$\llbracket S_{1};S_{2}\rrbracket_{\lightning}(\rho,q+p)=\llbracket S_{2}% \rrbracket_{\lightning}(\llbracket S_{1}\rrbracket_{\rho}(\rho,0),q)+% \llbracket S_{1}\rrbracket_{\lightning}(\rho,p)$
3.

$\llbracket S\rrbracket_{\rho}$ is bounded linear

The proof can be found in [14].

3.2.3 Equivalence of Semantics

The following lemma asserts the equivalence of our operational and denotational semantics. Intuitively, the denotational semantics gives a distribution over final states and its second component captures the probability to reach $\langle\lightning\rangle$ , the state for violated observations. As the operational semantics is only defined for $tr(\rho)=1$ , we only consider this case:

Lemma 7.

For any program $S$ and initial state $\rho\in\mathcal{D}(\mathcal{H})$

$\blacksquare$

$\llbracket S\rrbracket(\rho,0)=(\sum_{\rho^{\prime}}Pr^{\mathfrak{R}_{\rho}% \llbracket S\rrbracket}(\lozenge\langle\downarrow,\rho^{\prime}\rangle)\cdot% \rho^{\prime},Pr^{\mathfrak{R}_{\rho}\llbracket S\rrbracket}(\lozenge\langle% \lightning\rangle))$
$\blacksquare$

$Pr^{\mathfrak{R}_{\rho}\llbracket S\rrbracket}(\lozenge\langle sink\rangle)=tr% (\llbracket S\rrbracket_{\rho}(\rho,0))+\llbracket S\rrbracket_{\lightning}(% \rho,0)$

Proof.

The first item can be shown by induction over $S$ . For the second item we use that every path that eventually reaches $\langle sink\rangle$ passes through either a $\langle\downarrow,\rho^{\prime}\rangle$ or a $\langle\lightning\rangle$ state. For more details on both proofs, see [14]. $\hfill\blacktriangleleft$

4 Weakest Preconditions

In this section, we consider how we can extend the weakest precondition calculus to capture observations and thus compute conditional probabilities of quantum programs using deductive verification. Recall that a predicate $P$ satisfies $\mathbf{0}\sqsubseteq P\sqsubseteq\textbf{I}$ . Let $tr(P\rho)$ be the probability that $\rho$ satisfies $P$ . Note that if $P$ is a projector, then $tr(P\rho)$ equals the probability that $\rho$ gives answer “yes” in a measurement defined by $P$ . Even if $P$ is not a projection, $tr(P\rho)$ is the average value of measuring $\rho$ with the measurement described by the observable $P$ . If not given directly, all proofs can be found in [14].

4.1 Total and Partial Correctness

Defining the semantics in a different way also changes the definition of Hoare logic with total and partial correctness [27]:

Definition 8.

Let $P,Q\in\mathcal{P}(\mathcal{H})$ , $S$ a program, $\rho\in\mathcal{D}^{-}(\mathcal{H})$ and $\{P\}S\{Q\}$ a correctness formula. Then

1.

(total correctness) $\models_{tot}\{P\}S\{Q\}$ iff $tr(P\rho)\leq tr(Q\llbracket S\rrbracket_{\rho}(\rho,0))$
2.

(partial correctness) $\models_{par}\{P\}S\{Q\}$ iff $tr(P\rho)\leq tr(Q\llbracket S\rrbracket_{\rho}(\rho,0))+tr(\rho)-tr(% \llbracket S\rrbracket_{\rho}(\rho,0))-\llbracket S\rrbracket_{\lightning}(% \rho,0)$

Let us explain this definition. Assume $tr(\rho)=1$ , otherwise all probabilities mentioned in the following are non-normalized. Recall that $tr(P\rho)$ is the probability that state $\rho$ satisfies predicate $P$ and $tr(Q\llbracket S\rrbracket_{\rho}(\rho,0))$ is the probability that the state after execution of $S$ starting with $\rho$ satisfies predicate $Q$ . Total correctness entails that the probability of a state satisfying precondition $P$ is at most the probability that it satisfies postcondition $Q$ after execution of $S$ . This only involves terminating runs. In the formula of partial correctness, the summand $\llbracket S\rrbracket_{\lightning}(\rho,0)$ captures the probability that an observation is violated during executing program $S$ on state $\rho$ . As before, $tr(\rho)-tr(\llbracket S\rrbracket_{\rho}(\rho,0))$ captures the probability that $S$ on state $\rho$ does not terminate.

Similar to [27], we have some nice but different properties:

Proposition 9.

1.

$\models_{tot}\{P\}S\{Q\}$ implies $\models_{par}\{P\}S\{Q\}$
2.

$\models_{tot}\{\mathbf{0}\}S\{Q\}$ . However, $\models_{par}\{P\}S\{\textbf{I}\}$ does not hold in general.
3.

For $P_{1},P_{2},Q_{1},Q_{2}\in\mathcal{P}(\mathcal{H})$ and $\lambda_{1},\lambda_{2}\in\mathbb{R}_{\geq 0}$ with $\lambda_{1}P_{1}+\lambda_{2}P_{2},\lambda_{1}Q_{1}+\lambda_{2}Q_{2}\in\mathcal% {P}(\mathcal{H})$ : $\models_{tot}\{P_{1}\}S\{Q_{1}\}\land\models_{tot}\{P_{2}\}S\{Q_{2}\}$ implies $\models_{tot}\{\lambda_{1}P_{1}+\lambda_{2}P_{2}\}S\{\lambda_{1}Q_{1}+\lambda_% {2}Q_{2}\}$

Proof.

1.

Follows from definition and $tr(\llbracket S\rrbracket_{\rho}(\rho,0))+\llbracket S\rrbracket_{\lightning}(% \rho,0)\leq tr(\rho)+0$ (Proposition 5)
2.

$\models_{tot}\{\mathbf{0}\}S\{Q\}$ follows from definition, $tr(\mathbf{0})=0$ and $tr(Q\sigma)\geq 0$ for all $\sigma\in\mathcal{D}^{-}(\mathcal{H})$ . For disproving $\models_{par}\{P\}S\{\textbf{I}\}$ , consider a program (with only one variable $q$ ) $S\equiv\mathbf{observe}(\ket{1}\bra{1},q)$ . Then the statement does not holds with $P=\textbf{I}$ and $\rho=\ket{0}\bra{0}$ because $\llbracket S\rrbracket_{\lightning}(\rho,0)>0$ .
3.

Follows from the linearity of the trace and the definition of $\models_{tot}$ .

$\hfill\blacktriangleleft$

4.2 Weakest (Liberal) Preconditions

Given a postcondition and a program, we are interested in the best (weakest) precondition w.r.t. total and partial correctness:

Definition 10.

Let program $S$ and predicate $P\in\mathcal{P}(\mathcal{H})$ .

1.

The weakest precondition is defined as $qwp\llbracket S\rrbracket(P)=\sup\{Q\mid\text{ }\models_{tot}\{Q\}S\{P\}\}$ . Thus $\models_{tot}\{qwp\llbracket S\rrbracket(P)\}S\{P\}$ and $\models_{tot}\{Q\}S\{P\}$ implies $Q\sqsubseteq qwp\llbracket S\rrbracket(P)$ for all $Q\in\mathcal{P}(\mathcal{H})$ .
2.

The weakest liberal precondition is defined as $qwlp\llbracket S\rrbracket(P)=\sup\{Q\mid\text{ }\models_{par}\{Q\}S\{P\}\}$ . Thus $\models_{par}\{qwlp\llbracket S\rrbracket(P)\}S\{P\}$ and $\models_{par}\{Q\}S\{P\}$ implies $Q\sqsubseteq qwlp\llbracket S\rrbracket(P)$ for all $Q\in\mathcal{P}(\mathcal{H})$ .

The following lemmas show that these suprema indeed exist. Both proofs are based on the Schrödinger-Heisenberg duality [25].

Lemma 11.

For a function $\llbracket S\rrbracket:\mathcal{D}\mathcal{R}\to\mathcal{D}\mathcal{R}$ with properties as in Proposition 5, the weakest precondition $qwp\llbracket S\rrbracket:\mathcal{P}(\mathcal{H})\rightarrow\mathcal{P}(% \mathcal{H})$ exists and is bounded linear and subunital. It satisfies $tr(qwp\llbracket S\rrbracket(P)\rho)=tr(P\llbracket S\rrbracket_{\rho}(\rho,0))$ for all $\rho\in\mathcal{D}^{-}(\mathcal{H}),P\in\mathcal{P}(\mathcal{H})$ and it is the only function of this type with this property.

This lemma (and the following one) does not require $\llbracket S\rrbracket$ to be a denotational semantics of some program $S$ . In contrast to [27], this result thus still holds if the language is extended as long as the conditions still holds.

Lemma 12.

For a function $\llbracket S\rrbracket:\mathcal{D}\mathcal{R}\rightarrow\mathcal{D}\mathcal{R}$ with properties as in Proposition 5, the weakest liberal precondition $qwlp\llbracket S\rrbracket:\mathcal{P}(\mathcal{H})\rightarrow\mathcal{P}(% \mathcal{H})$ exists and is subunital. It satisfies

tr(qwlp\llbracket S\rrbracket(P)\rho)=tr(P\llbracket S\rrbracket_{\rho}(\rho,0% ))+tr(\rho)-tr(\llbracket S\rrbracket_{\rho}(\rho,0))-\llbracket S\rrbracket_{% \lightning}(\rho,0)

for each $\rho\in\mathcal{D}^{-}(\mathcal{H}),P\in\mathcal{P}(\mathcal{H})$ and it is the only function of this type with this property.

This general theorem about the existence of weakest liberal preconditions also applies for programs without observations (because $\llbracket S\rrbracket_{\lightning}(\rho,0)=0$ and $\llbracket S\rrbracket_{\rho}(\rho,0)=\llbracket S\rrbracket_{og}(\rho)$ for each $\rho\in\mathcal{D}^{-}(\mathcal{H})$ and for each observation-free program $S$ , Proposition 4). Lemma 11 and 12 extend [7] to the infinite-dimensional case and to partial correctness, i.e., the existence of weakest liberal preconditions.

Now we consider some healthiness properties about weakest (liberal) preconditions:

Proposition 13.

For every program $S$ , the function $qwp\llbracket S\rrbracket:\mathcal{P}(\mathcal{H})\to\mathcal{P}(\mathcal{H})$ satisfies:

$\blacksquare$

Bounded linearity
$\blacksquare$

Subunitality: $qwp\llbracket S\rrbracket(\textbf{I})\sqsubseteq\textbf{I}$
$\blacksquare$

Monotonicity: $P\sqsubseteq Q$ implies $qwp\llbracket S\rrbracket(P)\sqsubseteq qwp\llbracket S\rrbracket(Q)$
$\blacksquare$

Order-continuity: $qwp\llbracket S\rrbracket(\bigvee_{i=0}^{\infty}P_{i})=\bigvee_{i=0}^{\infty}% qwp\llbracket S\rrbracket(P_{i})$ if $\bigvee_{i=0}^{\infty}P_{i}$ exists

Proposition 14.

For every program $S$ , the function $qwlp\llbracket S\rrbracket:\mathcal{P}(\mathcal{H})\to\mathcal{P}(\mathcal{H})$ satisfies:

$\blacksquare$

Affinity: The function $f:\mathcal{P}(\mathcal{H})\to\mathcal{P}(\mathcal{H})$ with $f(P)=qwlp\llbracket S\rrbracket(P)-qwlp\llbracket S\rrbracket(\mathbf{0})$ is linear. Note that this implies convex-linearity and sublinearity.
$\blacksquare$

Subunitality: $qwlp\llbracket S\rrbracket(\textbf{I})\sqsubseteq\textbf{I}$
$\blacksquare$

Monotonicity: $P\sqsubseteq Q$ implies $qwlp\llbracket S\rrbracket(P)\sqsubseteq qwlp\llbracket S\rrbracket(Q)$
$\blacksquare$

Order-continuity: $qwlp\llbracket S\rrbracket(\bigvee_{i=0}^{\infty}P_{i})=\bigvee_{i=0}^{\infty}% qwlp\llbracket S\rrbracket(P_{i})$ if $\bigvee_{i=0}^{\infty}P_{i}$ exists

For our denotational semantics $\llbracket S\rrbracket$ , we can also give an explicit representation of $qwp\llbracket S\rrbracket$ :

Proposition 15.

Let $P\in\mathcal{P}(\mathcal{H})$ :

$\blacksquare$

$qwp\llbracket\mathbf{skip}\rrbracket(P)=P$
$\blacksquare$

$qwp\llbracket q:=0\rrbracket(P)=\begin{cases}\ket{0}_{q}\bra{0}P\ket{0}\bra{0}% _{q}+\ket{1}\bra{0}_{q}P\ket{0}\bra{1}_{q}&,\text{if }type(q)=\mathit{Bool}\\ \sum_{n\in\mathbb{Z}}\ket{n}\bra{0}_{q}P\ket{0}\bra{n}_{q}&,\text{if }type(q)=% \mathit{Int}\end{cases}$
$\blacksquare$

$qwp\llbracket\overline{q}:=U\overline{q}\rrbracket(P)=U^{\dagger}PU$
$\blacksquare$

$qwp\llbracket\mathbf{observe}\text{ }(\bar{q},O)\rrbracket(P)=O^{\dagger}PO$
$\blacksquare$

$qwp\llbracket S_{1};S_{2}\rrbracket(P)=qwp\llbracket S_{1}\rrbracket(qwp% \llbracket S_{2}\rrbracket(P))$
$\blacksquare$

$qwp\llbracket\mathbf{measure}\text{ }M[\bar{q}]:\bar{S}\rrbracket(P)\rho=\sum_% {m}M_{m}^{\dagger}(qwp\llbracket S_{m}\rrbracket(P))M_{m}$
$\blacksquare$

$qwp\llbracket\mathbf{while}\text{ }M[\bar{q}]=1\text{ }\mathbf{do}\text{ }S^{% \prime}\rrbracket(P)=\bigvee_{n=0}^{\infty}P_{n}$ with

$\displaystyle P_{0}=\mathbf{0},$ $\displaystyle P_{n+1}=[M_{0}^{\dagger}PM_{0}]+[M_{1}^{\dagger}(qwp\llbracket S% ^{\prime}\rrbracket(P_{n}))M_{1}]$

and $\bigvee_{n=0}^{\infty}$ denoting the least upper bound w.r.t. $\sqsubseteq$ .

Proof.

We prove $tr(qwp\llbracket S\rrbracket(P)\rho)=tr(P\llbracket S\rrbracket_{\rho}(\rho,0))$ , which then, together with Lemma 11 implies that it is indeed the weakest precondition. $\hfill\blacktriangleleft$ In this and the following proposition we mean convergence of sums with respect to the SOT, more details can be found in [25].

For weakest liberal preconditions the explicit representation looks quite similar:

Proposition 16.

Let $P\in\mathcal{P}(\mathcal{H})$ . For most cases, $qwlp\llbracket S\rrbracket(P)$ is defined analogous to $qwp\llbracket S\rrbracket(P)$ (replacing every occurrence of $q w p$ by $q w l p$ ). The only significant difference is the while-loop: $qwlp\llbracket\mathbf{while}\text{ }M[\bar{q}]=1\text{ }\mathbf{do}\text{ }S^{% \prime}\rrbracket(P)=\bigwedge_{n=0}^{\infty}P_{n}$ with

\displaystyle P_{0}=\textbf{I},

\displaystyle P_{n+1}=[M_{0}^{\dagger}PM_{0}]+[M_{1}^{\dagger}(qwlp\llbracket S% ^{\prime}\rrbracket(P_{n}))M_{1}]

and $\bigwedge_{n=0}^{\infty}$ denoting the greatest lower bound w.r.t. $\sqsubseteq$ .

Proof.

This proof is similar to Proposition 15 except that we show that $tr(qwlp\llbracket S\rrbracket(P)\rho)=tr(P\llbracket S\rrbracket_{\rho}(\rho,0% ))+tr(\rho)-tr(\llbracket S\rrbracket_{\rho}(\rho,0))-\llbracket S\rrbracket_{% \lightning}(\rho,0)$ holds which then implies together with Lemma 12 that it is indeed the weakest liberal precondition. $\hfill\blacktriangleleft$ Both explicit representations above are conservative extensions of the weakest (liberal) precondition calculus in [27].

For the following explanations, assume $tr(\rho)=1$ , otherwise the probabilities are not normalized. To understand those definitions, consider $tr(qwp\llbracket S\rrbracket(P)\rho)$ . Due to the duality from Lemma 11, $tr(qwp\llbracket S\rrbracket(P)\rho)=tr(P\llbracket S\rrbracket_{\rho}(\rho,0))$ , so it is the probability that the result of running program $S$ (without violating any observations) on the initial state $\rho$ satisfies predicate $P$ . Similarly, $tr(qwlp\llbracket S\rrbracket(P)\rho)$ adds the probability of non-termination too. This is equivalent to the standard interpretation of weakest (liberal) preconditions in [27].

For programs with observations $tr(qwlp\llbracket S\rrbracket(P)\rho)$ does not include runs that violate an observation. Thus, $tr(qwlp\llbracket S\rrbracket(\textbf{I})\rho)$ gives the probability that no observation is violated during the run of $S$ on input state $\rho$ (while for programs without observations and in [27], this will always be $tr(\rho)=1$ ). The probability that a program state $\rho$ will satisfy the postcondition $P$ after executing program $S$ while not violating any observation is then a conditional probability. To handle this case, we introduce conditional weakest preconditions inspired by [23] in the next section.

4.3 Conditional Weakest Preconditions

In the following, we consider pairs of predicates. Addition and multiplication are interpreted pointwise, i.e., $(P,Q)+(P^{\prime},Q^{\prime})=(P+P^{\prime},Q+Q^{\prime})$ and $M\cdot(P,Q)=(MP,MQ)$ resp. $(P,Q)\cdot M=(PM,QM)$ where $M$ can be a constant or an operator. Multiplication binds stronger than addition.

We define a natural ordering on pairs of predicates that is used for example to express healthiness conditions:

Definition 17.

We define $\unlhd$ on $\mathcal{P}(\mathcal{H})^{2}$ as follows: $(P,Q)\unlhd(P^{\prime},Q^{\prime})\Leftrightarrow P\sqsubseteq P^{\prime}\land Q% ^{\prime}\sqsubseteq Q$ where $\sqsubseteq$ is the Loewner partial order. The least element is $(\mathbf{0},\textbf{I})$ and the greatest element $(\textbf{I},\mathbf{0})$ . The least upper bound of an increasing chain $\{(P_{i},Q_{i})\}_{i\in\mathbb{N}}$ for $(P_{i},Q_{i})\in\mathcal{P}(\mathcal{H})^{2}$ is given pointwise by $\bigvee_{i=0}^{\infty}(P_{i},Q_{i})=(\bigvee_{i=0}^{\infty}P_{i},\bigwedge_{i=% 0}^{\infty}Q_{i})$ .

Lemma 18.

$\unlhd$ is an $\omega$ -cpo on $\mathcal{P}(\mathcal{H})^{2}$ .

Proof.

We have to show that $\bigvee_{i=0}^{\infty}(P_{i},Q_{i})$ exists for any increasing chain $\{(P_{i},Q_{i})\}_{i\in\mathbb{N}}$ . If $\{(P_{i},Q_{i})\}_{i\in\mathbb{N}}$ is increasing with respect to $\unlhd$ , then $\{P_{i}\}_{i\in\mathbb{N}}$ is increasing and $\{Q_{i}\}_{i\in\mathbb{N}}$ decreasing with respect to $\sqsubseteq$ . The existence of $\bigvee_{i=0}^{\infty}P_{i}$ follows directly from $\sqsubseteq$ being an $\omega$ -cpo on $\mathcal{P}(\mathcal{H})$ . For $\bigwedge_{i=0}^{\infty}Q_{i}$ , we use the same trick as in the proof of Proposition 16: $\{\textbf{I}-Q_{i}\}_{i\in\mathbb{N}}$ is an increasing chain of predicates and thus $\bigwedge_{i=0}^{\infty}Q_{i}=\textbf{I}-\bigvee_{i=0}^{\infty}(\textbf{I}-Q_{% i})$ exists too. That means both $\bigvee_{i=0}^{\infty}P_{i}$ and $\bigwedge_{i=0}^{\infty}Q_{i}$ exist and thus also $\bigvee_{i=0}^{\infty}(P_{i},Q_{i})$ . $\hfill\blacktriangleleft$ Combining weakest preconditions and liberal weakest preconditions, we can define conditional weakest preconditions similar to the probabilistic case [23]:

Definition 19.

The conditional weakest precondition transformer is a mapping $qcwp\llbracket S\rrbracket:\mathcal{P}(\mathcal{H})^{2}\to\mathcal{P}(\mathcal% {H})^{2}$ defined as $qcwp\llbracket S\rrbracket(P,Q):=(qwp\llbracket S\rrbracket(P),qwlp\llbracket S% \rrbracket(Q))$ .

Similar to the weakest precondition calculus, we can also give an explicit representation which can be found in [14].

Again, assume $tr(\rho)=1$ in the following, otherwise the probabilities are not normalized. Note that $tr(qwlp\llbracket S\rrbracket(\textbf{I})\rho)$ is the probability that no observation is violated and $tr(qwp\llbracket S\rrbracket(P)\rho)$ the probability that $P$ is satisfied after $S$ has been executed on $\rho$ (see above). We are interested in the conditional probability of establishing the postcondition given that no observation is violated, namely $\frac{tr(qwp\llbracket S\rrbracket(P)\rho)}{tr(qwlp\llbracket S\rrbracket(% \textbf{I})\rho)}$ . Notice that for $qcwp\llbracket S\rrbracket(P,\textbf{I})=(A,B)$ , this is simply $\frac{tr(A\rho)}{tr(B\rho)}$ . That means we can immediately read of this conditional probability from $qcwp\llbracket S\rrbracket$ . Formally, we use

\displaystyle\hat{tr}(A\rho,B\rho):=\begin{cases}\frac{tr(A\rho)}{tr(B\rho)},&% \text{ if }tr(B\rho)\neq 0\\ \text{undefined},&\text{ otherwise}.\end{cases}

We now establish some properties of conditional weakest preconditions:

Proposition 20.

For every program $S$ , the function $qcwp\llbracket S\rrbracket:\mathcal{P}(\mathcal{H})^{2}\to\mathcal{P}(\mathcal% {H})^{2}$ satisfies:

$\blacksquare$

Has a linear interpretation: for all $\rho\in\mathcal{D}^{-}(\mathcal{H}),a,b\in\mathbb{R}_{\geq 0}$ and $P,P^{\prime}\in\mathcal{P}(\mathcal{H})$ with $aP+bP^{\prime}\in\mathcal{P}(\mathcal{H})$

$\displaystyle\hat{tr}(qcwp\llbracket S\rrbracket(aP+bP^{\prime},\textbf{I})% \cdot\rho)=a\cdot\hat{tr}(qcwp\llbracket S\rrbracket(P,\textbf{I})\cdot\rho)+b% \cdot\hat{tr}(qcwp\llbracket S\rrbracket(P^{\prime},\textbf{I})\cdot\rho)$
$\blacksquare$

Affinity: The function $qcwp\llbracket S\rrbracket(P,Q)-qcwp\llbracket S\rrbracket(\mathbf{0},\mathbf{% 0})$ is linear. Note that this implies convex-linearity and sublinearity.
$\blacksquare$

Monotonicity: $(P,P^{\prime})\unlhd(Q,Q^{\prime})$ implies $qcwp\llbracket S\rrbracket(P,P^{\prime})\unlhd qcwp\llbracket S\rrbracket(Q,Q^% {\prime})$
$\blacksquare$

Continuity: $qcwp\llbracket S\rrbracket(\bigvee_{i=0}^{\infty}(P_{i},Q_{i}))=\bigvee_{i=0}^% {\infty}qcwp\llbracket S\rrbracket(P_{i},Q_{i})$ if $\bigvee_{i=0}^{\infty}(P_{i},Q_{i})$ exists

4.4 Conditional Weakest Liberal Preconditions

Similar to the conditional weakest precondition, we can also define the same with weakest liberal preconditions for partial correctness:

Definition 21.

The conditional weakest liberal precondition $qcwlp:\mathcal{P}(\mathcal{H})^{2}\to\mathcal{P}(\mathcal{H})^{2}$ is defined as $qcwlp\llbracket S\rrbracket(P,Q):=(qwlp\llbracket S\rrbracket(P),qwlp% \llbracket S\rrbracket(Q))$ for each program $S$ and predicates $P,Q\in\mathcal{P}(\mathcal{H})$ .

Definition 22.

We define $\dot{\unlhd}$ on $\mathcal{P}(\mathcal{H})^{2}$ as follows $(P,Q)\phantom{.}\dot{\unlhd}\phantom{.}(P^{\prime},Q^{\prime})\Leftrightarrow P% \sqsubseteq P^{\prime}\land Q\sqsubseteq Q^{\prime}$ where $\sqsubseteq$ is the Loewner partial order. The least element is $(\mathbf{0},\mathbf{0})$ and the greatest element $(\textbf{I},\textbf{I})$ . The least upper bound of an increasing chain $\{(P_{i},Q_{i})\}_{i\in\mathbb{N}}$ for $(P_{i},Q_{i})\in\mathcal{P}(\mathcal{H})^{2}$ is given pointwise by $\bigvee_{i=0}^{\infty}(P_{i},Q_{i})=(\bigvee_{i=0}^{\infty}P_{i},\bigvee_{i=0}% ^{\infty}Q_{i})$ .

Note that in contrast to $\unlhd$ , both components are ordered in the same direction. Here it follows directly that $\dot{\unlhd}$ is an $\omega$ -cpo on $\mathcal{P}(\mathcal{H})^{2}$ .

Similar as for $q c w p$ , we can now read off the conditional satisfaction of $P$ when we want non-termination to count as satisfaction: $\hat{tr}(qcwlp\llbracket S\rrbracket(P,\textbf{I})\cdot\rho)=\frac{tr(qwlp% \llbracket S\rrbracket(P)\rho)}{tr(qwlp\llbracket S\rrbracket(\textbf{I})\rho)}$ which is equal to dividing the probability to satisfy $P$ after execution (including non-termination) by the probability to not violate an observation¹¹1So far, we considered conditional weakest preconditions for total and partial correctness, i.e., $qcwp\llbracket S\rrbracket(P,\textbf{I})=(qwp\llbracket S\rrbracket(P),qwlp% \llbracket S\rrbracket(\textbf{I}))$ and $qcwlp\llbracket S\rrbracket(P,\textbf{I})=(qwlp\llbracket S\rrbracket(P),qwlp% \llbracket S\rrbracket(\textbf{I}))$ . In [15, Sect. 8.3] it is argued why other combinations such as $(qwp\llbracket S\rrbracket(P),qwp\llbracket S\rrbracket(\textbf{I}))$ and $(qwlp\llbracket S\rrbracket(P),qwp\llbracket S\rrbracket(\textbf{I}))$ only make sense if a program is almost-surely terminating, i.e., without non-termination. Their arguments apply without change in our setting, so we do not consider these combinations either..

We can also conclude some properties about conditional weakest liberal preconditions:

Proposition 23.

For every program $S$ , the function $qcwlp\llbracket S\rrbracket:\mathcal{P}(\mathcal{H})^{2}\to\mathcal{P}(% \mathcal{H})^{2}$ satisfies:

$\blacksquare$

Affinity: The function $qcwlp\llbracket S\rrbracket(P,Q)-qcwlp\llbracket S\rrbracket(\mathbf{0},% \mathbf{0})$ is linear. Note that this implies convex-linearity and sublinearity.
$\blacksquare$

Monotonicity: $(P,Q)\phantom{.}\dot{\unlhd}\phantom{.}(P^{\prime},Q^{\prime})$ implies $qcwlp\llbracket S\rrbracket(P,Q)\phantom{.}\dot{\unlhd}\phantom{.}qcwlp% \llbracket S\rrbracket(P^{\prime},Q^{\prime})$
$\blacksquare$

Continuity: $qcwlp\llbracket S\rrbracket(\bigvee_{i=0}^{\infty}(P_{i},Q_{i}))=\bigvee_{i=0}% ^{\infty}qcwlp\llbracket S\rrbracket(P_{i},Q_{i})$ if $\bigvee_{i=0}^{\infty}(P_{i},Q_{i})$

4.5 Observation-Free Programs

For observation-free programs, our interpretations coincides with the satisfaction of weakest (liberal) preconditions from [27]:

Lemma 24.

For an observation-free program $S$ , predicate $P\in\mathcal{P}(\mathcal{H})$ and state $\rho\in\mathcal{D}(\mathcal{H})$ :

\displaystyle\hat{tr}(qcw(l)p\llbracket S\rrbracket(P,\textbf{I})\cdot\rho)=tr% (qw(l)p\llbracket S\rrbracket(P)\rho)

Proof.

For every observation-free program $S$ is $qwlp\llbracket S\rrbracket(\textbf{I})=\textbf{I}$ [27] and which means for $\rho\in\mathcal{D}(\mathcal{H})$ (and not for all $\rho\in\mathcal{D}^{-}(\mathcal{H})$ ) $\hat{tr}(qcw(l)p\llbracket S\rrbracket(P,\textbf{I})\cdot\rho)$ is equal to

\displaystyle\frac{tr(qw(l)p\llbracket S\rrbracket(P)\rho)}{tr(qwlp\llbracket S% \rrbracket(\textbf{I})\rho)}=\frac{tr(qw(l)p\llbracket S\rrbracket(P)\rho)}{tr% (\rho)}=tr(qw(l)p\llbracket S\rrbracket(P)\rho).

$\hfill\blacktriangleleft$

4.6 Correspondence to Operational MC Semantics

The aim of this section is to establish a correspondence between $qcwp\llbracket S\rrbracket(P,\textbf{I})$ and the operational semantics of $S$ . In order to reason about $P$ in terminal states of the Markov chain, we use rewards. First, we equip the Markov chain used for the operational semantics with a reward function with regard to a postcondition $P$ :

Definition 25.

For program $S$ and postcondition $P$ , the Markov reward chain $\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket$ is the MC $\mathfrak{R}_{\rho}\llbracket S\rrbracket$ extended with a function $r:\Sigma\to\mathbb{R}_{\geq 0}$ such that $r(\langle\downarrow,\rho^{\prime}\rangle)=tr(P\rho^{\prime})$ and $r(s)=0$ for all other states $s\in\Sigma$ .

The (liberal) reward of a path $\pi$ of $\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket$ is defined as $r(\pi)=\begin{cases}tr(P\rho^{\prime})&,\text{ if }\langle\downarrow,\rho^{% \prime}\rangle\in\pi\\ 0&,\text{ else}\end{cases}$ and $lr(\pi)=r(\pi)$ expect if $\langle sink\rangle\not\in\pi$ , then $lr(\pi)=1$ .

The expected reward of $\lozenge\langle sink\rangle$ is the expected value of $r(\pi)$ for all $\pi\in\lozenge\langle sink\rangle$ , i.e., $ER^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(\lozenge\langle sink\rangle% )=\sum_{\rho^{\prime}}Pr^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(% \lozenge\langle\downarrow,\rho^{\prime}\rangle)\cdot tr(P\rho^{\prime})$ . The liberal version adds rewards of non-terminating paths, i.e., $LER^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(\lozenge\langle sink% \rangle)=ER^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(\lozenge\langle sink% \rangle)+Pr^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(\neg\lozenge% \langle sink\rangle)$ .

Now we start by showing some auxiliary results, similar to [23, Lemma 5.5, 5.6]:

Lemma 26.

For a program $S$ , state $\rho\in\mathcal{D}(\mathcal{H})$ , predicate $P\in\mathcal{P}(\mathcal{H})$ we have

\displaystyle Pr^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(\neg\lozenge% \langle\lightning\rangle)=tr(qwlp\llbracket S\rrbracket(\textbf{I})\rho),

\displaystyle(L)ER^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(\lozenge% \langle sink\rangle)=tr(qw(l)p\llbracket S\rrbracket(P)\rho)

Proof.

Follows from Lemma 7, Lemma 11 and Lemma 12. $\hfill\blacktriangleleft$ We are interested in the conditional (liberal) expected reward of reaching $\langle sink\rangle$ from the initial state $\langle S,\rho\rangle$ , conditioned on not visiting $\langle\lightning\rangle$ :

\displaystyle C(L)ER^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(\lozenge% \langle sink\rangle\mid\neg\lozenge\langle\lightning\rangle):=

\displaystyle\frac{(L)ER^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(% \lozenge\langle sink\rangle)}{Pr^{\mathfrak{R}_{\rho}^{\textbf{I}}\llbracket S% \rrbracket}(\neg\lozenge\langle\lightning\rangle)}

This reward is equivalent to our interpretation of $qcw(l)p$ , analogous to [23, Theorem 5.7]:

Theorem 27.

For a program $S$ , state $\rho\in\mathcal{D}(\mathcal{H})$ , predicates $P,Q\in\mathcal{P}(\mathcal{H})$ we have

\displaystyle C(L)ER^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(\lozenge% \langle sink\rangle\mid\neg\lozenge\langle\lightning\rangle)

\displaystyle=\hat{tr}(qcw(l)p\llbracket S\rrbracket(P,\textbf{I})\cdot\rho)

Proof.

Assuming $tr(qwlp\llbracket S\rrbracket(\textbf{I})\rho)>0$ , then $C(L)ER^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(\lozenge\langle sink% \rangle\mid\neg\lozenge\langle\lightning\rangle)$ is equal to

\displaystyle\frac{(L)ER^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(% \lozenge\langle sink\rangle)}{Pr^{\mathfrak{R}_{\rho}^{\textbf{I}}\llbracket S% \rrbracket}(\neg\lozenge\langle\lightning\rangle)}=\frac{tr(qw(l)p\llbracket S% \rrbracket(P)\rho)}{tr(qwlp\llbracket S\rrbracket(\textbf{I})\rho)}=\hat{tr}(% qcw(l)p\llbracket S\rrbracket(P,\textbf{I})\cdot\rho)

by Lemma 26. If $tr(qwlp\llbracket S\rrbracket(\textbf{I})\rho)=0$ , then $C(L)ER^{\mathfrak{R}_{\rho}^{P}\llbracket S\rrbracket}(\lozenge\langle sink% \rangle\mid\neg\lozenge\langle\lightning\rangle)$ is undefined which means both sides of the statement are undefined and thus equal. $\hfill\blacktriangleleft$

5 Examples

In this section we provide two examples on how conditional quantum weakest preconditions can be applied.

5.1 The Quantum Fast-Dice-Roller

In probabilistic programs, generating a uniform distribution using fair coins is a challenge. The fast dice roller efficiently simulates the throw of a fair dice, generating a uniform distribution about $N$ possible outcomes [19]. We solve this problem for $N=6$ with quantum gates by creating qubits $q, p, r$ with Hadamard gates and using the observe statement to reject the $qp=11$ case, leaving $6$ possible outcomes ( $qpr=000,\ldots,101$ ), see Figure 2.

Figure 2: Quantum Fast-Dice-Roller. For the identity operator on

\mathcal{H}_{2}\otimes\mathcal{H}_{2}

we use

\textbf{I}_{4}

.

The Markov chain representing the operational semantics can be found in [14]. To prove correctness, we focus on the probability of termination and reaching the desired state without violating the observation. This probability cannot be directly read from the operational semantics, even for this simple program. To specify this property formally, we use the reward MC as defined in Definition 25. The desired probability can be computed using conditional weakest preconditions, see Theorem 27.

To terminate in a state where the probability of all six outcomes is equal and forms a distribution, we verify that we reach the uniform superposition

\displaystyle\ket{\phi}=\sqrt{\frac{1}{6}}\big{(}\ket{000}+\ket{001}+\ket{010}% +\ket{011}+\ket{100}+\ket{101}\big{)}

over $6$ states. Measuring in the computational basis yields a uniform distribution. After computing the conditional weakest precondition, we can determine the likelihood of each input state reaching the fixed uniform superposition and producing a uniform distribution, assuming the observation is not violated. We use the decoupling of $qcwp\llbracket S\rrbracket(P,\textbf{I})$ and compute $qwp\llbracket S\rrbracket(P)$ and $qwlp\llbracket S\rrbracket(\textbf{I})$ separately where $P=\outerproduct{\phi}{\phi}$ and $S$ stands for our fast-dice roller program (Figure 2). The probability that an input state $\rho$ will reach the desired uniform superposition is $\hat{tr}(qcwp\llbracket S\rrbracket(P,\textbf{I})\cdot\rho)$ , that is

\displaystyle\frac{tr(qwp\llbracket S\rrbracket(P)\rho)}{tr(qwlp\llbracket S% \rrbracket(\textbf{I})\rho)}=\begin{cases}1&,\text{if }\rho=\outerproduct{000}% {000}\\ 0&,\text{if }\rho=\outerproduct{x}{x}\text{ with }x\in\{001,011,101,111\}\\ 0.1111&,\text{if }\rho=\outerproduct{x}{x}\text{ with }x\in\{010,100,110\}.% \end{cases}

$\rho=\outerproduct{000}{000}$ will reach the desired superposition with probability $1$ assuming no observation is violated. We can also see that $tr(qwp\llbracket S\rrbracket(P)\outerproduct{000}{000})\neq 1$ so even with the “best” input, our conditional weakest precondition calculus gives more information than $qwp\llbracket S\rrbracket(P)$ .

5.2 MAJ-SAT

To demonstrate our approach, we will verify the correctness of a program that is used to solve MAJ-SAT. Unlike SAT, which asks whether there exists at least one satisfying assignment of a Boolean formula, MAJ-SAT asks whether a Boolean formula is satisfied by at least half of all possible variable assignments. MAJ-SAT is known to be PP-complete and [1] uses it to prove the equivalence of the complexity classes PostBQP and PP.

Figure 3: Inner loop body

S_{k}

of the quantum algorithm solving MAJ-SAT as presented in [1].

y, z

are qubits,

\overline{q}

is an

n

-qubit sized register (formally

n

qubits

q_{1},\dots,q_{n}

). We use

\overline{q}:=0^{\otimes n}

to denote that all

n

qubits of

\overline{q}

are set of

0

.

R_{k}=\frac{1}{\sqrt{1+4^{k}}}\begin{pmatrix}1&-2^{k}\\ \nobreakspace 2^{k}&1\end{pmatrix}

is a rotation matrix depending on the parameter

k

and

C H

is a controlled Hadamard.

Formally, we are faced with the following problem: A formula with $n$ variables can be represented by a function $f:\{0,1\}^{n}\to\{0,1\}$ with $s=\absolutevalue{\{f(x)=1\}}$ . The goal is to determine whether $s<2^{n-1}$ holds or not. Aaronson [1] presents a PostBQP algorithm for this problem. A PostBQP algorithm is one that runs in polynomial time, is allowed to perform measurements to check whether certain conditions are satisfied (analogous to our $\mathbf{observe}$ statement) and is required to produce the correct result with high probability conditioned on those measurements succeeding. The algorithm from [1] is as follows:

\begin{array}[]{l}\text{for }k=-n,...,n:\\ \hskip 14.22636pt\text{repeat }n\text{ times:}\\ \hskip 28.45274ptS_{k}\\ \hskip 14.22636pt\text{if }S_{k}\text{ succeeded more than }\frac{3}{4}n\text{% times}:\\ \hskip 28.45274pt\text{return true}\\ \text{return false}\end{array}

where $S_{k}$ is given in Figure 3 and succeeding means that measuring $z$ in the $\ket{+},\ket{-}$ basis returns $\ket{+}$ . The core idea is to show that $S_{k}$ succeeds with probability $\leq\frac{1}{2}$ for all $k$ if $s\geq 2^{n-1}$ and with probability $\geq\Bigl{(}\frac{1+\sqrt{2}}{\sqrt{6}}\Bigr{)}^{2}\geq 0.971$ for at least one $k$ otherwise. Hence the overall algorithm solves MAJ-SAT. To keep this example manageable, we focus on the analysis of $S_{k}$ alone.

We use conditional weakest preconditions and determine $qcwp\llbracket S_{k}\rrbracket(P,\textbf{I}^{\otimes n+2})$ (which depends on the parameters $n, s, k$ ). Here the postcondition $P$ corresponds to $z$ being in state $\ket{+}$ , formally $P=\ket{+}\bra{+}_{z}\otimes\textbf{I}$ . Then the probability that $S_{k}$ succeeds is $\Pr_{nsk}:=\hat{tr}(qcwp\llbracket S_{k}\rrbracket(P,\textbf{I}^{\otimes n+2})% \odot\rho)$ for initial state $\rho$ .

We computed the cwp symbolically using a computer algebra system, but the resulting formulas were quite unreadable. So for the sake of this example, we present numerical results of computing cwp instead. Since $S_{k}$ does not contain any loops, the cwp can be computed by mechanic application of the rules for observation, assignment, and application of unitaries. Performing these calculations for selected values of $n$ and $s$ and all $k=-n,\dots,n$ , we find that in each case the cwp is of the form $(c\textbf{I},c^{\prime}\textbf{I})$ for some $c,c^{\prime}\in\mathbb{R}$ . This is to be expected since all variables $\bar{q},z,y$ are initialized at the beginning of the program, so the cwp should not depend on the initial state, i.e., all matrices should be multiples of the identity. In that case, $\Pr_{nsk}=c/c^{\prime}$ . In Figure 4, we show $\max_{k}\Pr_{nsk}$ for selected $s, n$ . (The claim from [1] is that the success probability of $S_{k}$ is $\geq 0.971$ for some $k$ if $s<2^{n-1}$ and $\leq 1/2$ for all $k$ otherwise, so we only care about the maximum over all $k$ .) We see that $\max_{k}\Pr_{nsk}$ is indeed $\geq 0.971$ and $\leq 1/2$ in those two cases. This confirms the calculation from [1], using our logic. (At least for the values of $s, n$ we computed.)

	$s=2$	$s=3$	$s=4$	$s=7$	$s=8$	…
$n=2$	$0.5$	$0.3838$	$0.3286$
$n=3$	$\underline{0.9714}$	$\underline{0.9991}$	$0.5$	$0.4247$	$0.4123$	…
$n=4$	$\underline{0.9991}$	$\underline{0.9933}$	$\underline{0.9714}$	$\underline{0.9889}$	$0.5$	…
$n=5$	$\underline{0.9889}$	$\underline{0.9828}$	$\underline{0.9991}$	$\underline{0.9977}$	$\underline{0.9714}$	…
…	…	…	…	…	…

Figure 4: Maximum of

\Pr_{nsk}={\hat{tr}(qcwp\llbracket S_{k}\rrbracket(P,\textbf{I}^{\otimes n+2})% \odot\rho)}

for

k\in[-n,n]

. The cases where

s<2^{n-1}

are underlined.

6 Conclusion

We introduced the observe statement in the quantum setting for infinite-dimensional cases, supported by operational, denotational and weakest precondition semantics. We defined conditional weakest preconditions, proved their equivalence to the operational semantics and applied them to an example using Bayesian inference. Future work includes the interpretation of predicates and exploration of alternatives to observe statements such as rejection sampling or hoisting in the probabilistic case. Additionally, the challenge of combining non-determinism with conditioning in probabilistic systems [23] may extend to quantum programs.

References

[1] Scott Aaronson. Quantum computing, postselection, and probabilistic polynomial-time. Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences, 461, September 2005. doi:10.1098/rspa.2005.1546.
[2] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
[3] Stephen Boyd and Lieven Vandenberghe. Convex Optimization. Cambridge University Press, 2004.
[4] John B. Conway. A Course in Operator Theory. Graduate Studies in Mathematics. American Mathematical Society, 2000.
[5] John B. Conway. A Course in Functional Analysis. Graduate Texts in Mathematics. Springer New York, 2007. doi:10.1007/978-1-4757-4383-8.
[6] Yuxin Deng and Yuan Feng. Formal semantics of a classical-quantum language. Theoretical Computer Science, 913:73–93, 2022. doi:10.1016/j.tcs.2022.02.017.
[7] Ellie D’Hondt and Prakash Panangaden. Quantum weakest preconditions. Math. Struct. Comput. Sci., 16(3):429–451, 2006. doi:10.1017/S0960129506005251.
[8] Olivia Di Matteo. On the need for effective tools for debugging quantum programs. In Proceedings of the 5th ACM/IEEE International Workshop on Quantum Software Engineering, Q-SE 2024, pages 17–20, New York, NY, USA, 2024. Association for Computing Machinery. doi:10.1145/3643667.3648226.
[9] Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453–457, 1975. doi:10.1145/360933.360975.
[10] Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
[11] Paul A. M. Dirac. The Principles of Quantum Mechanics. Clarendon Press, Oxford, 1930.
[12] Yuan Feng and Yingte Xu. Verification of nondeterministic quantum programs. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3, ASPLOS 2023, pages 789–805, New York, NY, USA, 2023. Association for Computing Machinery. doi:10.1145/3582016.3582039.
[13] Yuan Feng and Mingsheng Ying. Quantum Hoare logic with classical variables. ACM Transactions on Quantum Computing, 2(4), 2021. doi:10.1145/3456877.
[14] Christina Gehnen, Dominique Unruh, and Joost-Pieter Katoen. Bayesian inference in quantum programs, 2025. arXiv:2504.20732.
[15] Benjamin L. Kaminski. Advanced Weakest Precondition Calculi for Probabilistic Programs. PhD thesis, RWTH Aachen University, February 2019. doi:10.18154/RWTH-2019-01829.
[16] Dexter Kozen. A probabilistic PDL. Journal of Computer and System Sciences, 30(2):162–178, 1985. doi:10.1016/0022-0000(85)90012-1.
[17] Marco Lewis, Sadegh Soudjani, and Paolo Zuliani. Formal verification of quantum programs: Theory, tools, and challenges. ACM Transactions on Quantum Computing, 2023. doi:10.1145/3624483.
[18] Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, and Yuan Xie. Projection-based runtime assertions for testing and debugging quantum programs. Proc. ACM Program. Lang., 4(OOPSLA), 2020. doi:10.1145/3428218.
[19] Jérémie O. Lumbroso. Optimal discrete uniform generation from coin flips, and applications. CoRR, abs/1304.1916, 2013. arXiv:1304.1916.
[20] Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005. doi:10.1007/b138392.
[21] Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, 2010. doi:10.1017/CBO9780511976667.
[22] Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, and Selva Samuel. R2: an efficient mcmc sampler for probabilistic programs. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, AAAI’14, pages 2476–2482. AAAI Press, 2014. doi:10.1609/AAAI.V28I1.9060.
[23] Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin L. Kaminski, Joost-Pieter Katoen, and Annabelle Mciver. Conditioning in probabilistic programming. ACM Trans. Program. Lang. Syst., 40(1), 2018. doi:10.1145/3156018.
[24] Masamichi Takesaki. Theory of Operator Algebras I. Number Bd. 1 in Encyclopaedia of Mathematical Sciences. Springer New York, 1979. doi:10.1007/978-1-4612-6188-9.
[25] Dominique Unruh. Quantum references, 2024. arXiv:2105.10914v3.
[26] Peng Yan, Hanru Jiang, and Nengkun Yu. On incorrectness logic for quantum programs. Proc. ACM Program. Lang., 6(OOPSLA1), 2022. doi:10.1145/3527316.
[27] Mingsheng Ying. Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst., 2012. doi:10.1145/2049706.2049708.
[28] Mingsheng Ying, Runyao Duan, Yuan Feng, and Zhengfeng Ji. Predicate transformer semantics of quantum programs. Semantic Techniques in Quantum Computation, 2010. doi:10.1017/CBO9781139193313.009.
[29] Li Zhou, Nengkun Yu, and Mingsheng Ying. An applied quantum Hoare logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pages 1149–1162, New York, NY, USA, 2019. Association for Computing Machinery. doi:10.1145/3314221.3314584.

[bib.bib1] [1] Scott Aaronson. Quantum computing, postselection, and probabilistic polynomial-time. Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences, 461, September 2005. doi:10.1098/rspa.2005.1546.

[bib.bib2] [2] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.

[bib.bib3] [3] Stephen Boyd and Lieven Vandenberghe. Convex Optimization. Cambridge University Press, 2004.

[bib.bib4] [4] John B. Conway. A Course in Operator Theory. Graduate Studies in Mathematics. American Mathematical Society, 2000.

[bib.bib5] [5] John B. Conway. A Course in Functional Analysis. Graduate Texts in Mathematics. Springer New York, 2007. doi:10.1007/978-1-4757-4383-8.

[bib.bib6] [6] Yuxin Deng and Yuan Feng. Formal semantics of a classical-quantum language. Theoretical Computer Science, 913:73–93, 2022. doi:10.1016/j.tcs.2022.02.017.

[bib.bib7] [7] Ellie D’Hondt and Prakash Panangaden. Quantum weakest preconditions. Math. Struct. Comput. Sci., 16(3):429–451, 2006. doi:10.1017/S0960129506005251.

[bib.bib8] [8] Olivia Di Matteo. On the need for effective tools for debugging quantum programs. In Proceedings of the 5th ACM/IEEE International Workshop on Quantum Software Engineering, Q-SE 2024, pages 17–20, New York, NY, USA, 2024. Association for Computing Machinery. doi:10.1145/3643667.3648226.

[bib.bib9] [9] Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453–457, 1975. doi:10.1145/360933.360975.

[bib.bib10] [10] Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

[bib.bib11] [11] Paul A. M. Dirac. The Principles of Quantum Mechanics. Clarendon Press, Oxford, 1930.

[bib.bib12] [12] Yuan Feng and Yingte Xu. Verification of nondeterministic quantum programs. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3, ASPLOS 2023, pages 789–805, New York, NY, USA, 2023. Association for Computing Machinery. doi:10.1145/3582016.3582039.

[bib.bib13] [13] Yuan Feng and Mingsheng Ying. Quantum Hoare logic with classical variables. ACM Transactions on Quantum Computing, 2(4), 2021. doi:10.1145/3456877.

[bib.bib14] [14] Christina Gehnen, Dominique Unruh, and Joost-Pieter Katoen. Bayesian inference in quantum programs, 2025. arXiv:2504.20732.

[bib.bib15] [15] Benjamin L. Kaminski. Advanced Weakest Precondition Calculi for Probabilistic Programs. PhD thesis, RWTH Aachen University, February 2019. doi:10.18154/RWTH-2019-01829.

[bib.bib16] [16] Dexter Kozen. A probabilistic PDL. Journal of Computer and System Sciences, 30(2):162–178, 1985. doi:10.1016/0022-0000(85)90012-1.

[bib.bib17] [17] Marco Lewis, Sadegh Soudjani, and Paolo Zuliani. Formal verification of quantum programs: Theory, tools, and challenges. ACM Transactions on Quantum Computing, 2023. doi:10.1145/3624483.

[bib.bib18] [18] Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, and Yuan Xie. Projection-based runtime assertions for testing and debugging quantum programs. Proc. ACM Program. Lang., 4(OOPSLA), 2020. doi:10.1145/3428218.

[bib.bib19] [19] Jérémie O. Lumbroso. Optimal discrete uniform generation from coin flips, and applications. CoRR, abs/1304.1916, 2013. arXiv:1304.1916.

[bib.bib20] [20] Annabelle McIver and Carroll Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005. doi:10.1007/b138392.

[bib.bib21] [21] Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, 2010. doi:10.1017/CBO9780511976667.

[bib.bib22] [22] Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, and Selva Samuel. R2: an efficient mcmc sampler for probabilistic programs. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, AAAI’14, pages 2476–2482. AAAI Press, 2014. doi:10.1609/AAAI.V28I1.9060.

[bib.bib23] [23] Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin L. Kaminski, Joost-Pieter Katoen, and Annabelle Mciver. Conditioning in probabilistic programming. ACM Trans. Program. Lang. Syst., 40(1), 2018. doi:10.1145/3156018.

[bib.bib24] [24] Masamichi Takesaki. Theory of Operator Algebras I. Number Bd. 1 in Encyclopaedia of Mathematical Sciences. Springer New York, 1979. doi:10.1007/978-1-4612-6188-9.

[bib.bib25] [25] Dominique Unruh. Quantum references, 2024. arXiv:2105.10914v3.

[bib.bib26] [26] Peng Yan, Hanru Jiang, and Nengkun Yu. On incorrectness logic for quantum programs. Proc. ACM Program. Lang., 6(OOPSLA1), 2022. doi:10.1145/3527316.

[bib.bib27] [27] Mingsheng Ying. Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst., 2012. doi:10.1145/2049706.2049708.

[bib.bib28] [28] Mingsheng Ying, Runyao Duan, Yuan Feng, and Zhengfeng Ji. Predicate transformer semantics of quantum programs. Semantic Techniques in Quantum Computation, 2010. doi:10.1017/CBO9781139193313.009.

[bib.bib29] [29] Li Zhou, Nengkun Yu, and Mingsheng Ying. An applied quantum Hoare logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pages 1149–1162, New York, NY, USA, 2019. Association for Computing Machinery. doi:10.1145/3314221.3314584.