# On the Hardness of Analyzing Quantum Programs Quantitatively

Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix

► To cite this version:

Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix. On the Hardness of Analyzing Quantum Programs Quantitatively. ESOP 2024 - 33rd European Symposium on Programming, Apr 2024, Luxembourg, Luxembourg. pp.28, 10.1007/978-3-031-57267-8_2. hal-04349874

HAL Id: hal-04349874

https://inria.hal.science/hal-04349874v1

Submitted on 20 Dec 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# On the Hardness of Analyzing Quantum Programs Quantitatively

**Abstract.** In this paper, we study quantitative properties of quantum programs. Properties of interest include (positive) almost-sure termination, expected runtime or expected cost, that is, for example, the expected number of applications of a given quantum gate, etc. After studying the completeness of these problems in the arithmetical hierarchy over the Clifford+T fragment of quantum mechanics, we express these problems using a variation of a quantum pre-expectation transformer, a weakest pre-condition based technique that allows to symbolically compute these quantitative properties. Under a smooth restriction—a restriction to polynomials of bounded degree over a real closed field—we show that the quantitative problem, which consists in finding an upper-bound to the pre-expectation, can be decided in time double-exponential in the size of a program, thus providing, despite its great complexity, one of the first decidable results on the analysis and verification of quantum programs. Finally, we sketch how the latter can be transformed into an efficient synthesis method.

## 1 Introduction

**Motivations.** Quantum computation is a promising and emerging computational paradigm which can efficiently solve problems considered to be intractable on classical computers [40,20]. However, the unintuitive nature of quantum mechanics poses challenging questions for the design and analysis of corresponding quantum programming. Indeed, the quantum program dynamics are considerably more complicated compared to the behavior of classical or probabilistic programs. Therefore, formal reasoning requires the development of novel methods and tools, a development that has already started and recently gathered momentum in various areas, like *design automation* [42,22], *programming languages* [38,2,30,23,15], *verification* [35,10], etc.

Among these formal methods, those that allow us to obtain quantitative properties on quantum programs are particularly interesting. They can be used to obtain relevant information about the computations of a quantum program, such as the number of qubits used, the number of unitary operators used. Thus enabling the corresponding compiled quantum circuit to be optimized (for example, by minimizing the use of gates that are hard to make fault-tolerant, or by reducing the number of qubits) or to avoid undesirable behavior such as non-termination. Quantitative properties of interest may also be the question whether or not a program *terminates almost-surely*, that is, whether its probability of non-termination is zero or not. Similarly, we could aim to capture the *expected values* of (classical) program variables upon termination assumption.
The latter can also be employed to reason about the *expected runtime* or the *expected cost* of quantum programs, if we suitable instrument the code with counter variables.

The program of Figure 1 implements a Repeat-Until-Success algorithm that can be used to simulate quantum unitary operators on input qubit $q_1$ by using repeated measurements. The quantum step-circuit on the right part corresponds to one iteration of the loop. Variable $i$ in the program just acts as a counter for T-gates. Hence an analysis on the expected value of variable $i$ can be used to infer upper bounds on the expected $T$-count, i.e., the expected number of times the so-called T-gate is used in the full compiled quantum circuit. Such an approach offers the advantage to allow the programmer to implement quantum programs using fewer T-gates, which are costly to implement fault-tolerantly [9,16], and it therefore provides a simple quantum program to illustrate that the study of quantitative properties is paramount.

<figure><img src="image_2.png" /><figcaption>Fig. 1. Repeat-until-success program RUS and step-circuit.</figcaption></figure>

In [5,29], new methodologies named *quantum expectation transformers* based on *predicate transformers* [12,27] and *expectation transformers* [31,17] have been put forward to naturally express and study the quantitative properties of quantum programs. However, no attempt was made to automate the corresponding techniques or delineate how complicated such an *automation* could be. Automation of these formal verification techniques in the context of quantum programs is a particularly difficult problem. Indeed, the consideration of Hilbert spaces as a mathematical framework for describing principles and laws of quantum mechanics makes it seemingly impossible to reason fully automatically about quantitative properties of quantum program: they involve computational objects of exponential dimensions (in the number of qubits) with scalars ranging over an uncountable domain (i.e., complex numbers). This problem is directly linked to the fact that the set $\mathbb{C}$ includes non-computable numbers [41] and that
testing the inequality $\le$ or the equality $=$ of two real numbers is not decidable, even if one restricts their study to computable real numbers. Consequently, the particular nature of quantum programs and of their semantic domain, Hilbert spaces, makes it impossible to directly apply the results obtained in the classical and probabilistic setting [36,24].

**Contributions.** In this paper, we study the hardness of the quantitative properties of mixed classical-quantum programs and provide a first step towards their (full) automation using quantum expectation transformers.

Towards that end, we restrict the considered quantum gates to the Clifford+T fragment, which is known to be the simplest approximately universal fragment of quantum mechanics [1]. Clifford+T makes it possible to only consider quantum states with algebraic amplitudes, thus restricting the study to a countable domain. It implies that our results can accommodate quantum gates employed in actual hardware, recently employed to claim *quantum advantage*, cf [3]. Moreover, the obtained results are very general as it can be extended to any set of gates with algebraic coefficients.

As motivated, our first contribution is about the general hardness of deciding quantitative properties for mixed classical-quantum programs. For a given input state, we study properties such as (positive) almost-sure termination, (P)AST for short, which consists in verifying that a program terminates with probability 1; testing problems, $TEST_R$, which consist in comparing a quantum expectation (for example, the mean value of a variable) with a given value (an algebraic and positive real number) wrt the relation $R$; and the finiteness problem, $TEST_{\neq\infty}$, which consists in checking that a quantum expectation is finite. For each of those problems, we also study the related universal problem, which consists to check the corresponding property for every input. We establish a precise mapping (Theorem 1) of the inherent complexity of each problem in the arithmetical hierarchy [33] that is summarized in Table 1, see Section 3. E.g., AST is $Π_2^0$-complete while PAST is $Σ_2^0$-complete. In Table 1, we have emphasized problems whose hardness has been studied neither in the classical nor in the probabilistic framework by marking them with (‡).

Our second contribution aims to overcome the aforementioned undecidability results. For that, we study approximations. More precisely, we focus on inferring bounding functions (in general depending on the input) on the expected values of classical program variables upon termination. The decision problem has thus been altered to an optimization problem. Further, we restrict the set of potential bounding functions. As a suitable class of functions, we consider polynomials over the real-closed field of the algebraic numbers. The restriction to algebraic numbers guarantees that comparison operations between real numbers remain decidable. On the other hand for any real closed field, quantifier elimination for formulas over polynomials is decidable, that is, there exists a double-exponential algorithm computing a quantifier-free formula equivalent to the original formula [21]. This recasting of the problem and restriction of the solution space suffices to render the problem decidable. The inference algorithm
established remains double-exponential (Theorem 4). Thus of similar complexity
as the underlying quantifier elimination procedure.

Finally, our last contribution (Section 5.3) studies effective automation of
the inference of upper bounds on the expected values of program variables. To
improve upon the double-exponential complexity, we further restrict the class of
polynomials considered, that is, to degree-2 polynomials and sketch how tech-
niques from optimization theory can be employed. Several simple quantum algo-
rithms such as program RUS can be analyzed using this approach (Example 6).
This further reduction in expressivity allows the encoding of the problem in SMT
and thus paves the way towards (full) automation.

**Related work.** Predicate transformers [12,27]—on which our work is based—were introduced as a method for reasoning about the semantics of imperative programs. They have been adapted to the probabilistic setting, leading to the notion of expectation transformer [31,17], which has been used to reason about expected values [25,7], runtimes [26,32], and costs [6,4,32], and to the quantum paradigm, leading to the notion of quantum pre-expectation transformer [34,29,5].

The problem of studying the difficulty of analyzing quantitative program
properties has been deeply studied in the classical setting. To mention a few,
[13] and [36] study termination properties and runtime/derivational properties
of first-order programs, respectively. Further, in [24] completeness results for
various quantitative properties of (pure) probabilistic programs have been estab-
lished. The inference problem of expectation transformers, i.e., establishing nice
implementation that automate the search for pre-expectations, has been studied
intensively. Examples of successful implementation are presented in [32,6,7]. Up
to now, however, no practical, feasible studies have been carried out on quan-
tum languages. Among the techniques using quantum expectation transformers,
we believe [5] to be the most amenable to automation. Indeed, by lifting up-
per invariants of [26] to the quantum setting, it enables approximate reasoning
and eliminate the need to reason about fixpoints or limits, stemming from the
semantics of loops.

## 2 Quantum programming language

In this section, we introduce the syntax and operational semantics of the con-
sidered mixed-quantum imperative programming language.

### 2.1 Syntax

We make use of three basic datatypes $\mathcal{B}$, $\mathcal{N}$ and $\mathcal{Q}$ for Boolean, numbers (non-negative integers), and qubit data, respectively. Let $\mathcal{K}$ be an arbitrary classical type in $\{\mathcal{B}, \mathcal{N}\}$. Each program variable comes with a fixed datatype and can be optionally annotated by its type as a superscript. In what follows, we will use $x, x', y, \dots$ to denote classical variables of type $\mathcal{K}$ and $q, q', \dots$ to denote quantum variables of type $\mathcal{Q}$. A program, denoted $P$, is simply a statement; see
<table><caption>Fig. 2. Syntax of quantum programs.</caption><tr><td>$\mathcal{N} \text{Exp} \ni \mathbf{n}, \mathbf{n}_1, \mathbf{n}_2$</td><td>::= $\mathbf{x}^{\mathcal{N}} | n \in \mathbb{N} | \mathbf{n}_1 + \mathbf{n}_2 | \mathbf{n}_1 - \mathbf{n}_2 | \mathbf{n}_1 \times \mathbf{n}_2$</td></tr><tr><td>$\mathcal{B} \text{Exp} \ni \mathbf{b}, \mathbf{b}_1, \mathbf{b}_2$</td><td>::= $\mathbf{x}^{\mathcal{B}} | \text{tt} | \text{ff} | \mathbf{n}_1 = \mathbf{n}_2 | \mathbf{n}_1 < \mathbf{n}_2 | \neg \mathbf{b} | \mathbf{b}_1 \wedge \mathbf{b}_2 | \mathbf{b}_1 \vee \mathbf{b}_2$</td></tr><tr><td>$\text{Exp} \ni \mathbf{e}, \mathbf{e}_1, \mathbf{e}_2$</td><td>::= $\mathbf{n} | \mathbf{b}$</td></tr><tr><td>$\text{Stmt} \ni \text{stm}, \text{stm}_1, \text{stm}_2$</td><td>::= $\text{skip} | \mathbf{x}^{\mathcal{K}} = \mathbf{e}^{\mathcal{K}} | \text{stm}_1; \text{stm}_2 | \text{if } \mathbf{b}^{\mathcal{B}} \text{ then } \text{stm}_1 \text{ else } \text{stm}_2 | \text{while } \mathbf{b}^{\mathcal{B}} \text{ do } \text{stm} | \bar{\mathbf{q}}^{\mathcal{Q}} * = \mathbf{U} | \mathbf{x}^{\mathcal{B}} = \text{meas } \mathbf{q}^{\mathcal{Q}}$</td></tr></table>

Figure 2. Program statements are either classical assignments, conditionals, sequences, loops, quantum assignments $\bar{\mathbf{q}}^{\mathcal{Q}} * = \mathbf{U}$, or measurements $\mathbf{x}^{\mathcal{B}} = \text{meas } \mathbf{q}^{\mathcal{Q}}$. A quantum assignment consists in the application of a quantum unitary gate $\mathcal{U}$ of arity $\mathbf{ar}(\mathcal{U})$ to a sequence of qubits $\bar{\mathbf{q}} \triangleq \mathbf{q}_1, \dots, \mathbf{q}_{\mathbf{ar}(\mathcal{U})}$ of type $\mathcal{Q}$. As we will see in the semantics section, a unitary matrix $\mathcal{U}$ will be associated with each quantum gate $\mathcal{U}$. A measurement performs a single qubit measurement of $\mathbf{q}$ in the computational basis: the outcome is a Boolean value and the quantum state evolves accordingly. For a given syntactic construct $t$, let $\mathcal{B}(t)$ (respectively $\mathcal{N}(t)$, $\mathcal{Q}(t)$) be the set of Boolean (respectively, number, qubit) variables in $t$.

**Example 1.** We consider the program of Figure 3, adapted from [5], as a simple leading example. Let $\mathcal{H}$ be the unitary operator computing the Hadamard gate. This program simulates coin tossing by repeatedly measuring the qubit $\mathbf{q}$ in the loop body `stm`, given as initial input parameter until the measurement outcome `ff` occurs.

The probability to terminate within $n$ steps depends on the initial state $\rho = \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix}$ (a density matrix in $\mathbb{C}^{2 \times 2}$, which implies $\alpha + \delta = 1$ and $\gamma = \bar{\beta}$) of the qubit $\mathbf{q}$. Variable $i$ is increased by one at each iteration and, hence, when the program terminates, $i$ stores as final value the number of loop iterations performed. The overall probability of termination is 1. The mean value of variable $i$, that is, the expected number of loop iterations, depends on the program input (hence, on the initial quantum state). The expected number of iterations is thus given as

$$F\left(\begin{pmatrix} \alpha & \beta \\ \bar{\beta} & \delta \end{pmatrix}\right) = p_0 \times 1 + \sum_{i=1}^{\infty} \frac{p_1}{2^i} (i+1) = p_0 + p_1 + 2p_1 = 1 + (\alpha - \beta - \bar{\beta} + \delta) = 2 - (\beta + \bar{\beta}),$$

where $p_0 = \frac{\alpha+\beta+\bar{\beta}+\delta}{2} = \frac{1+\beta+\bar{\beta}}{2} = 1 - p_1$ is the probability to measure $|0\rangle$ on the first iteration of the loop. For a qubit initialized in state $|\phi\rangle = \sqrt{1/3}|0\rangle + \sqrt{2/3}|1\rangle$, the corresponding density matrix is $\rho_{|\phi\rangle} = |\phi\rangle\langle\phi| = \begin{pmatrix} 1/3 & \sqrt{2}/3 \\ \sqrt{2}/3 & 2/3 \end{pmatrix}$ and hence the expected number of loop iterations is $F(\rho_{|\phi\rangle}) = 2 - 2\sqrt{2}/3$. It will be simply 2 in the case of an initialization in the computational basis $|\phi\rangle = |0\rangle$ or $|\phi\rangle = |1\rangle$.

Notice that the language can be extended to deal with statements initializing qubits in the basis states. For example, the following syntactic sugar can be used $\mathbf{q}^{\mathcal{Q}} = |0\rangle \triangleq \mathbf{x} = \text{meas } \mathbf{q}$; if $\mathbf{x}$ then $\mathbf{q} * = \mathbf{X}$ else skip, with $\mathbf{X}$ being the Pauli $\mathbf{X}$ gate and for some fresh variable $\mathbf{x}$ of type $\mathcal{B}$.
<figure><img src="image_3.png" /><figcaption>Fig. 3. Quantum Coin tossing</figcaption></figure>

## 2.2 Operational semantics

Following [5], we model the dynamics of our language as a probabilistic abstract reduction system (see [8]), a transition system where reduction is determined as a relation over probability distributions.

**Probabilistic abstract reduction systems.** Given a subset $\mathbb{K}$ of $\mathbb{R}$, let $\mathbb{K}^+$ be the set of non-negative numbers in $\mathbb{K}$, i.e., $\mathbb{K}^+ \triangleq \mathbb{K} \cap \{x \mid x \ge 0\}$ and let $\mathbb{K}^\infty$ be defined by $\mathbb{K}^\infty \triangleq \mathbb{K} \cup \{\infty\}$.

A discrete (sub)distribution $\delta$ over a set $A$ is a function $\delta : A \to [0, 1]$ with countable support that maps an element $a$ of $A$ to a probability $\delta(a)$ such that $|\delta| \triangleq \sum_{a \in \text{supp}(\delta)} \delta(a) = 1$ (respectively $|\delta| \le 1$). Any (sub)distribution $\delta$ can be written as $\{\delta(a) : a\}_{a \in \text{supp}(\delta)}$. The set of subdistributions over $A$, denoted by $\mathcal{D}(A)$, is closed under denumerable convex combinations $\sum_i p_i \cdot \delta_i \triangleq \lambda a. \sum_i p_i \delta_i(a)$, with $p_i \in [0, 1]$ and $\sum_i p_i \le 1$. Slightly simplifying standard notation, given $f : A \to \mathbb{R}^{+\infty}$ and a subdistribution $\delta \in \mathcal{D}(A)$, we define $\mathbb{E}_{\delta}(f)$, the expectation of $f$ on $\delta$, by $\mathbb{E}_{\delta}(f) \triangleq \sum_{a \in \text{supp}(\delta)} \delta(a) f(a)$. Note that $\mathbb{E}_{\delta}(f) \in \mathbb{R}^{+\infty}$ is always defined, since the co-domain of $f$ is restricted to non-negative reals.

Bournez and Garnier [8] introduced the notion of *Probabilistic Abstract Reduction System (PARS)* as a means to study reduction systems that evolve probabilistically. A PARS $\rightarrow$ on $A$ is a binary relation $\cdot \rightarrow \subseteq A \times \mathcal{D}(A)$. The intended meaning is that when $a \rightarrow \delta$, then $a$ reduces to $b \in \text{supp}(\delta)$ with probability $\delta(b)$. Here, we focus on *deterministic* PARSs, i.e., PARSs $\rightarrow$ with $a \rightarrow \delta_1$ and $a \rightarrow \delta_2$ implies $\delta_1 = \delta_2$. An object $a \in A$ is called *terminal* if there is no rule $a \rightarrow \delta$, which we write as $a \nrightarrow$.

Every deterministic PARS $\rightarrow$ over $A$ naturally lifts to a reduction relation $\rightarrow\vdash$ over distributions so that $\delta \rightarrow\vdash \varepsilon$, if the reduct distribution $\varepsilon$ is obtained from $\delta$ by replacing reducts in $\text{supp}(\delta)$ according to the PARS $\rightarrow$. In fact, we define this lifting in terms of a ternary relation $\cdot \stackrel{c}{\rightarrow} \subseteq \mathcal{D}(A) \times \mathbb{R}^+ \times \mathcal{D}(A)$ on distributions, where in a step $\delta \stackrel{c}{\rightarrow} \varepsilon$ the *weight* $c$ signifies the probability that a reduction has occurred. This relation is defined according to the following three rules.
$$ \frac{a \not\to}{\{1 : a\} \xrightarrow{0} \{1 : a\}} \qquad \frac{a \to \delta}{\{1 : a\} \xrightarrow{1} \delta} \qquad \frac{\delta_i \xrightarrow{c_i} \epsilon_i \sum_i p_i \le 1}{\sum_i p_i \cdot \delta_i \xrightarrow{\sum_i p_i c_i} \sum_i p_i \cdot \epsilon_i} $$

We may sometimes use the n-fold ($n \ge 0$) composition of $\to$, denoted $\to^n$, given by $\delta \xrightarrow{c^n} \epsilon$ if $\delta \xrightarrow{c_1} \dots \xrightarrow{c_n} \epsilon$ and the weights satisfy $c = \sum_{i=1}^n c_i$. Notice that since $\to$ is deterministic, so is $\xrightarrow{c}$ in the sense that $\delta \xrightarrow{c_1} \epsilon_1$ and $\delta \xrightarrow{c_2} \epsilon_2$ implies $c_1 = c_2$ and $\epsilon_1 = \epsilon_2$. Thus, in particular, for every $a \in A$ there is precisely one infinite reduction

$$ \{1 : a\} = \delta_0 \xrightarrow{c_0} \delta_1 \xrightarrow{c_1} \delta_2 \xrightarrow{c_2} \delta_3 \to \dots $$

For any $b \in A$, the probability $\delta_i(b)$ gives the probability that $a$ reduces to $b$ in $i$ steps. Note that when $b$ is terminal, this probability only increases along reductions (i.e., $\delta_i(b) \le \delta_{i+1}(b)$ for all $i$). This justifies that we define the terminal distribution of $a$ as the distribution $\delta(b) \triangleq \lim_{i \to \infty} \delta_i(b)$. Note that $\delta(b)$ gives the probability that $a$ reaches $b$ in an arbitrary (but finite) number of steps. Since the weights $c_i$ indicate the probability that a step has been performed from $\delta_i$ to $\delta_{i+1}$, the infinite sum $\sum_{i=0}^{\infty} c_i \in \mathbb{R}^{+\infty}$ gives the expected number of reduction steps carried out, the *expected derivation length of a*.

For a PARS $\to$, we denote by $\text{term}_\to: A \to \mathcal{D}(A)$ the function associating with each $a \in A$ its terminal distribution. The *expected derivation length function* $\text{edl}_\to: A \to \mathbb{R}^{+\infty}$ associates each $a \in A$ to its expected derivation length. The PARS $\to$ is *almost surely terminating* [39] (a.s. terminating for short) if $a \in A$ reduces to a terminal object $b \not\to$ with probability 1, that is, if $|\text{term}_\to(a)| = 1$ for every $A$. It is *positive almost surely terminating*, if the expected derivation length is always finite, that is, $\text{edl}_\to(a) < \infty$ for all $a \in A$.

Apart from termination, we are interested also in questions related to functional correctness, such as (i) what is the probability that $a$ reaches a terminal $b$, (ii) what is the probability that $a$ reaches a terminal satisfying predicate $P$, and more generally, (iii) which value does $f: A \to \mathbb{R}^{+\infty}$ take, in expectation, when fully reducing an object $a$. In the literature [31], one tool to answer all of these are given by *weakest pre-expectation transformers*, the natural generalisation of classical weakest pre-condition transformers to a quantitative, probabilistic setting. We suite this notion to PARSs.

**Definition 1 (Weakest pre-expectation).** The weakest pre-expectation for a PARS $\to$ over $A$ is given by the function

$$ \text{wp}_{\to}: (A \to \mathbb{R}^{+\infty}) \to (A \to \mathbb{R}^{+\infty}) $$

$$ \text{wp}_{\to} \triangleq \lambda f.\lambda a. \mathbb{E}_{\text{term}_{\to}(a)}(f). $$

For $\mathbf{1}_b$ the indicator function evaluating to 1 on argument $b$ and to 0 otherwise, and by seeing a predicate $P$ as 0, 1 valued function, $\text{wp}_{\to} \mathbf{1}_b$ $a$ answers question (i), $\text{wp}_{\to} P$ $a$ answers (ii), and generally $\text{wp}_{\to} F$ $a$ answers question (iii). Note also that a PARS is a.s. terminating iff $\text{wp}_{\to} (\lambda b. 1)$ $a = 1$ for each $a \in A$. On the other hand, positive a.s. termination cannot be expressed through an application of $\text{wp}_{\to}$.
$$
\begin{align*}
& \frac{\overline{(\text{skip}, s, \rho) \to_Q \{1 : (\downarrow, s, \rho)\}}}{\overline{(\bar{q}^* = \mathbf{U}, s, \rho) \to_Q \{1 : (\downarrow, s, \Phi_{U\bar{q}}(\rho))\}}} \quad (\text{Skip}) \quad \frac{\overline{(\mathbf{x} = \mathbf{e}, s, \rho) \to_Q \{1 : (\downarrow, s[\mathbf{x} := \llbracket \mathbf{e} \rrbracket^s], \rho)\}}}{\overline{(\bar{q}^* = \mathbf{U}, s, \rho) \to_Q \{1 : (\downarrow, s, \Phi_{U\bar{q}}(\rho))\}}} \quad (\text{Exp}) \\
& \frac{\overline{(\mathbf{x} = \text{meas } q_i, s, \rho) \to_Q \{\text{tr}(M_{k,i}\rho) : (\downarrow, s[\mathbf{x} := k], m_{k,i}(\rho))\}_{k \in \{0,1\}}}}{\overline{(\text{stm}_1, s, \rho) \to_Q \{p_i : (\text{stm}_\downarrow^i, s^i, \rho^i)\}_{i \in I}} \quad (\text{Meas})} \\
& \frac{\overline{(\text{stm}_1; \text{stm}_2, s, \rho) \to_Q \{p_i : (\text{stm}_\downarrow^i; \text{stm}_2, s^i, \rho^i)\}_{i \in I}}}{\overline{\llbracket \mathbf{b} \rrbracket^s \in \{0,1\}}} \quad (\text{Seq}) \\
& \frac{\overline{(\text{if } \mathbf{b} \text{ then } \text{stm}_1 \text{ else } \text{stm}_0, s, \rho) \to_Q \{1 : (\text{stm}_{\llbracket \mathbf{b} \rrbracket^s}, s, \rho)\}}}{\overline{(\text{while } \mathbf{b} \text{ do } \text{stm}, s, \rho) \to_Q \{1 : (\downarrow, s, \rho)\}}} \quad (\text{Cond}) \\
& \frac{\overline{\llbracket \mathbf{b} \rrbracket^s = 0}}{\overline{(\text{while } \mathbf{b} \text{ do } \text{stm}, s, \rho) \to_Q \{1 : (\downarrow, s, \rho)\}}} \quad (\text{Wh}_0) \\
& \frac{\overline{\llbracket \mathbf{b} \rrbracket^s = 1}}{\overline{(\text{while } \mathbf{b} \text{ do } \text{stm}, s, \rho) \to_Q \{1 : (\text{stm}; \text{while } \mathbf{b} \text{ do } \text{stm}, s, \rho)\}}} \quad (\text{Wh}_1)
\end{align*}
$$

<caption>Fig. 4. Operational semantics in terms of PARS.</caption>

**Quantum programs as PARSs.** We now endow quantum programs with an operational semantics defined in terms of a PARS. Given a totally ordered set of qubits $Q = \{q_1, \dots, q_n\}$, let $\mathcal{H}_Q$ be the $2^n$-dimensional Hilbert space defined by $\mathcal{H}_Q \triangleq \otimes_{i=1}^n \mathcal{H}_{q_i}$, with $\mathcal{H}_q = \mathbb{C}^2$ being the vector space of computational basis $\{|0\rangle, |1\rangle\}$ and $\otimes$ being the tensor product. With $\langle k|$ we denote the transpose conjugate of $|k\rangle$, for $k \in \{0, 1\}$. Let $\mathcal{M}(\mathcal{H}_Q)$ be the set of complex square matrices acting on the Hilbert space $\mathcal{H}_Q$, i.e., $\mathcal{M}(\mathcal{H}_Q) = \mathbb{C}^{2^n \times 2^n}$. Given $M \in \mathcal{M}(\mathcal{H}_Q)$, $M^\dagger$ denotes the transpose conjugate of $M$ and let $I_{2^n}$ be the identity matrix over $\mathcal{M}(\mathcal{H}_Q)$. We will write $I$ when the dimension is clear from the context.

Let $\mathcal{D}(\mathcal{H}_Q) \subsetneq \mathcal{M}(\mathcal{H}_Q)$ be the set of all *density operators* (or quantum states), i.e., positive semi-definite matrices of trace equal to 1 on $\mathcal{H}_Q$. Density operators can be viewed as the mathematical representation of a (mixed) *quantum state*. A *unitary operator* $U$ is a matrix in $\mathcal{M}(\mathcal{H}_Q)$ such that $UU^\dagger = U^\dagger U = I$. A *superoperator* $\Phi_U : \mathcal{D}(\mathcal{H}_Q) \to \mathcal{D}(\mathcal{H}_Q)$, an endomorphism over density operators, is attached to each unitary operator $U$ and defined by $\Phi_U \triangleq \lambda\rho.U\rho U^\dagger$. By definition, $\Phi_U$ is a completely positive trace preserving linear map. Indeed, $\text{tr}(U\rho U^\dagger) = \text{tr}(\rho)$, by unitarity. Hence $U\rho U^\dagger$ is a density operator in $\mathcal{D}(\mathcal{H}_Q)$ for each $\rho \in \mathcal{D}(\mathcal{H}_Q)$.

Regarding measurements, for each $i$, $1 \le i \le \text{card}(Q)$, we define $M_{k,i} \in \mathcal{M}(\mathcal{H}_Q)$, with $k \in \{0,1\}$, by $M_{0,i} \triangleq I_{2^{i-1}} \otimes (|0\rangle\langle 0|) \otimes I_{2^{n-i}}$ and $M_{1,i} \triangleq I - M_{0,i}$. The measurement of the qubit $q_i$ (in the computational basis) of a density matrix $\rho \in \mathcal{D}(\mathcal{H}_Q)$, produces the classical outcome $k \in \{0,1\}$ with probability $\text{tr}(M_{k,i}\rho)$.
The (normalized) quantum state, after the measurement, is defined by

$$m_{k,i}(\rho) \triangleq \begin{cases} \frac{M_{k,i}\rho M_{k,i}^{\dagger}}{\mathrm{tr}(M_{k,i}\rho)}, & \text{if } \mathrm{tr}(M_{k,i}\rho) \neq 0, \\ \frac{I}{2^n}, & \text{otherwise.} \end{cases}$$

Note that for all $\rho \in \mathcal{D}(\mathcal{H}_Q)$, $m_{k,i}(\rho) \in \mathcal{D}(\mathcal{H}_Q)$, as it holds that $\mathrm{tr}(m_{k,i}(\rho)) = 1$. Indeed, $\mathrm{tr}(M_{k,i}\rho M_{k,i}^{\dagger}) = \mathrm{tr}(M_{k,i}^2\rho) = \mathrm{tr}(M_{k,i}\rho)$, as $M_{k,i}$ is a projection. Hence $m_{k,i}$ is a map in $\mathcal{D}(\mathcal{H}_Q) \to \mathcal{D}(\mathcal{H}_Q)$.

Set $[[\mathcal{B}]] \triangleq \{0,1\}$ and $[[\mathcal{N}]] \triangleq \mathbb{N}$. The classical state is modeled as a (well-typed) store $s$ of domain $dom(s)$ mapping each variable $x$ of type $\mathcal{K}$ to a value in $[[\mathcal{K}]]$. Let $s[x^\mathcal{K}] := k]$ with $k \in [[\mathcal{K}]]$ be the store obtained from $s$ by updating the value assigned to $x$ in the map $s$. Given a store $s$, let $[[\cdot]]^s: \mathcal{K}\mathrm{Exp} \to [[\mathcal{K}]]$ be the map associating to each expression $e$ of type $\mathcal{K}$ and such that $\mathcal{B}(e) \cup \mathcal{N}(e) \subseteq dom(s)$, a value in $[[\mathcal{K}]]$, and defined in a standard way. For example $[[x]]^s \triangleq s(x)$, $[[n]]^s \triangleq n$, $[[tt]]^s \triangleq 1$, $[[n_1 - n_2]]^s \triangleq \max(0, [[n_1]]^s - [[n_2]]^s)$, etc. Let Store be the set of stores.

Let $\downarrow$ be a special symbol for termination. A configuration $\mu$, for statement $\mathrm{stm} \in \mathrm{Stmt} \cup \{\downarrow\}$, store $s$, and a quantum state $\rho$, has the form $(\mathrm{stm}, s, \rho)$. Let Conf be the set of configurations. A configuration $(\mathrm{stm}, s, \rho)$ is well-formed with respect to the sets of variables $B, V$, and $Q$ if $\mathcal{B}(\mathrm{stm}) \subseteq B$, $\mathcal{N}(\mathrm{stm}) \subseteq V$, $\mathcal{Q}(\mathrm{stm}) \subseteq Q$, $dom(s) = B \cup V$, and $\rho \in \mathcal{D}(\mathcal{H}_Q)$. Throughout the paper, we only consider configurations that are well-formed with respect to the sets of variables of the program under consideration.

The operational semantics is described in Figure 4 as a PARS $\to_Q$ over objects in Conf, where terminal objects are precisely the configurations of the shape $(\downarrow, s, \rho)$. The (classical or quantum) state of a configuration can only be updated by the three rules (Exp), (Op), and (Meas). Rule (Exp) updates the classical store wrt the value of the evaluated expression. Rule (Op) updates the quantum state to a new quantum state $\Phi_{U_{\bar{q}}}(\rho) = U_{\bar{q}}\rho U_{\bar{q}}^{\dagger}$, where $U_{\bar{q}}$ is the unitary operator in $\mathcal{M}(\mathcal{H}_Q)$ computed by extending the quantum gate $U$ to the entire set of qubits $Q$. Rule (Meas) performs a measurement on qubit $q_i$. This rule returns a distribution of configurations corresponding to the two possible outcomes, $k = 0$ and $k = 1$, with their respective probabilities $\mathrm{tr}(M_{k,i}\rho)$ and, in each case, updates the classical store and the quantum state accordingly. In the particular case where $\mathrm{tr}(M_{k_0,i}\rho) = 0$ for some $k_0 \in \{0,1\}$, $\{\mathrm{tr}(M_{k,i}\rho) : (\downarrow, s[x := k], m_{k,i}(\rho))\}_{k \in \{0,1\}} = \{1 : (\downarrow, s[x := 1 - k_0], m_{1-k_0,i}(\rho))\}$. Rule (Seq) governs the execution of a sequence of statements $\mathrm{stm}_1; \mathrm{stm}_2$, under the covenant that $\downarrow; \mathrm{stm} \triangleq \mathrm{stm}$, for each statement $\mathrm{stm}$. The rule accounts for potential probabilistic behavior when $\mathrm{stm}_1$ performs a measurement and it is otherwise standard. All the other rules are standard.

In a configuration $\mu = (\mathrm{stm}, s, \rho)$, the pair $\sigma \triangleq (s, \rho)$ is called a state. Let $\mathrm{St}^{\mathrm{stm}}$ be the set of states $\sigma, \tau, ...$ that are well-formed wrt statement $\mathrm{stm}$. For simplicity, we will denote this set by $\mathrm{St}$ when $\mathrm{stm}$ is clear from the context. To ease the presentation, we sometimes write $(\mathrm{stm}, \sigma)$ for the configuration $\mu$.
Specifically, we will be interested also in expected runtimes and expectation based reasoning. These carry over from PARSs as expected. In what follows, we call functions $f: \text{Conf} \to \mathbb{R}^{+\infty}$ expectations.

**Definition 2.** For a statement `stm`, a state `σ`, and an expectation `f: St → R⁺∞`, we overload the notions of expected derivation length and weakest pre-expectation by:

$$ 
\begin{aligned}
edl_{\text{stm}}: \text{St} &\to \mathbb{R}^{+\infty} & qwp_{\text{stm}}: (\text{St} &\to \mathbb{R}^{+\infty}) &\to (\text{St} &\to \mathbb{R}^{+\infty}) \\
edl_{\text{stm}} &\triangleq \lambda\sigma.edl_{\sim\chi_1}(\text{stm}, \sigma) & qwp_{\text{stm}} &\triangleq \lambda f.\lambda\sigma .wp_{\sim\chi_1}(f_{st})(\text{stm}, \sigma),
\end{aligned}
$$

where $f_{st}(\text{stm}, \tau) = f(\tau)$.

**Example 2.** Consider the program Cointoss given Figure 3. In the setting of the program Cointoss, $Q = \{q\}$, $M_{0,1} = (\begin{smallmatrix} 1 & 0 \\ 0 & 0 \end{smallmatrix})$ and $M_{1,1} = (\begin{smallmatrix} 0 & 0 \\ 0 & 1 \end{smallmatrix})$. On an initial state $\sigma = (s, \rho)$, the reduction starts deterministically as in the classical setting, performing the initialization $x = tt$ and $i = 0$. From there, evaluation reaches the loop while $x$ do `stm`. At each loop iteration, the loop counter $i$ is incremented, and the Hadamard gate applied to the quantum variable `q`. The loop guard is obtained through measuring `q`.

To see how this is reflected in the semantics, let us first look at an iteration of the loop. If `x` was set to false, that is `x` holds the value 0, by rule (Wh₀) the loop terminates within one step:

$$ \{1: (\text{while } x \text{ do } \text{stm}, [x:=0, i:=i], \rho)\} \xrightarrow{1} {}_Q \{1: (\downarrow, [x:=0, i:=i], \rho)\}. \quad (0) $$

On the other hand, when `x` was previously set to true, the loop executes its body. Precisely, we have:

$$ \begin{aligned} & \{1: (\text{while } x \text{ do } \text{stm}, [x:=1, i:=i], \rho)\} \\ & \xrightarrow{1} {}_Q \{1: (i = i+1; q = H; x = \text{meas } q; \text{ while } x \text{ do } \text{stm}, [x:=1, i:=i], \rho)\} \end{aligned} \quad (1) $$

$$ \xrightarrow{1} {}_Q \{1: (q = H; x = \text{meas } q; \text{ while } x \text{ do } \text{stm}, [x:=1, i:=i+1], \rho)\} \quad (2) $$

$$ \xrightarrow{1} {}_Q \{1: (x = \text{meas } q; \text{ while } x \text{ do } \text{stm}, [x:=k, i:=i+1], \Phi_H(\rho))\} \quad (3) $$

$$ \xrightarrow{1} {}_Q \{p_k: (\text{while } x \text{ do } \text{stm}, [x:=k, i:=i+1], \rho_k)\}_{k \in \{0,1\}}, \quad (4) $$

where in the last step, the probability $p_k$ equals $\text{tr}(M_{k,1}\Phi_H(\rho))$, while the normalized quantum state $\rho_k$ is given as $m_{k,1}(\Phi_H(\rho))$. The above reduction is obtained by applying the rules of Figure 4: rule (Wh₁) for reduction (1); rules (Exp) and (Seq) for reduction (2); rules (Op) and (Seq) for reduction (3); and finally rules (Meas) and (Seq) for reduction (4).

For an arbitrary initial quantum state $\rho = \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix} \in \mathcal{D}(\mathcal{H}_Q)$ (where $\alpha, \beta, \gamma, \delta \in \mathbb{C}$ and $\text{tr}(\rho) = \alpha + \delta = 1, \gamma = \bar{\beta}$, etc.), it follows that

$$ p_0 = \text{tr}(M_{0,1} H \rho H^\dagger) = \text{tr}((\begin{smallmatrix} 1 & 0 \\ 0 & 0 \end{smallmatrix}) \frac{1}{2} \begin{pmatrix} \alpha+\beta+\gamma+\delta & \alpha-\beta+\gamma-\delta \\ \alpha+\beta-\gamma-\delta & \alpha-\beta-\gamma+\delta \end{pmatrix}) = \frac{1+\beta+\gamma}{2}, $$
and likewise, $p_1 = 1-p_0 = \frac{1-(\beta+\gamma)}{2}$. Using $\rho_k = \frac{M_{k,1}H\rho H^\dagger M_{k,1}^\dagger}{\text{tr}(M_{k,1}H\rho H^\dagger)} = \frac{(M_{k,1}H)\rho(M_{k,1}H)^\dagger}{p_k}$,

$$ \rho_0 = \frac{\begin{pmatrix} 1/\sqrt{2} & 1/\sqrt{2} \\ 0 & 0 \end{pmatrix} \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix} \begin{pmatrix} 1/\sqrt{2} & 0 \\ 1/\sqrt{2} & 0 \end{pmatrix}}{p_0} = \begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix} \quad \rho_1 = \frac{\begin{pmatrix} 0 & 0 \\ 1/\sqrt{2} & 1/\sqrt{2} \end{pmatrix} \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix} \begin{pmatrix} 0 & 1/\sqrt{2} \\ 0 & 1/\sqrt{2} \end{pmatrix}}{p_1} = \begin{pmatrix} 0 & 0 \\ 0 & 1 \end{pmatrix}. $$

Summarizing (1)–(4) we thus get:

$$ \begin{aligned} & \{1: (\text{while } x \text{ do } \text{stm}, [x:=1, i:=i], \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix})\} \\ & \xrightarrow{4} \begin{Bmatrix} p_0: (\text{while } x \text{ do } \text{stm}, [x:=0, i:=i+1], \rho_0), \\ p_1: (\text{while } x \text{ do } \text{stm}, [x:=1, i:=i+1], \rho_1) \end{Bmatrix}. \end{aligned} $$

Putting everything together, we have

$$ \begin{aligned} & (\text{Cointoss}, s, \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix}) \xrightarrow{2} \begin{Bmatrix} 1: (\text{while } x \text{ do } \text{stm}, [x:=1, i:=0], \rho) \\ \rho_0: (\text{while } x \text{ do } \text{stm}, [x:=0, i:=1], \rho_0), \\ \rho_1: (\text{while } x \text{ do } \text{stm}, [x:=1, i:=1], \rho_1) \end{Bmatrix} \\ & \xrightarrow{4} \begin{Bmatrix} p_0+4p_1: (\text{while } x \text{ do } \text{stm}, [x:=0, i:=1], \rho_0), \\ \frac{p_1}{2}: (\text{while } x \text{ do } \text{stm}, [x:=0, i:=2], \rho_0), \\ \frac{p_1}{2}: (\text{while } x \text{ do } \text{stm}, [x:=1, i:=2], \rho_1) \end{Bmatrix} \\ & \xrightarrow{\frac{p_1}{2}+4\frac{p_1}{2}} \begin{Bmatrix} p_0: (\text{while } x \text{ do } \text{stm}, [x:=0, i:=1], \rho_0), \\ \frac{p_1}{2}: (\text{while } x \text{ do } \text{stm}, [x:=0, i:=2], \rho_0), \\ \frac{p_1}{4}: (\text{while } x \text{ do } \text{stm}, [x:=0, i:=3], \rho_0), \\ \frac{p_1}{4}: (\text{while } x \text{ do } \text{stm}, [x:=1, i:=3], \rho_1) \end{Bmatrix} \\ & \xrightarrow{\frac{p_1}{4}+4\frac{p_1}{4}} \dots \end{aligned} $$

where terminal configurations are underlined. This reduction converges to the terminal distribution

$\text{term}_{\text{Cointoss}}(s, \rho) = \{p_0: (\downarrow, [x:=0, i:=1], \rho_0)\} + \{\frac{p_1}{2^i}: (\downarrow, [x:=0, i:=i+1], \rho_0)\}_{i \ge 1}$, with an expected derivation length of

$$ \text{edl}_{\text{Cointoss}}(s, \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix}) = 2 + 4 + (p_0 + 4p_1) + \sum_{i=1}^{\infty} \frac{5p_1}{2^i} = 7 + 8p_1 = 11 - 4(\beta + \gamma). $$

For the expectation $f: \text{St} \to \mathbb{R}^{+\infty}$ defined by $f(s, \rho) \triangleq s(i)$ we have

$$ \text{qwp}_{\text{Cointoss}} f(s, \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix}) = p_0 \times 1 + \sum_{i=1}^{\infty} \frac{p_1}{2^i} (i+1) = p_0 + p_1 + 2p_1 = 2 - (\beta + \gamma), $$

that is, the mean value held by i holds after execution is $2 - (\beta + \gamma)$. The termination probability is

$$ \text{qwp}_{\text{Cointoss}} (\lambda\sigma.1) (s, \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix}) = p_0 \times 1 + \sum_{i=1}^{\infty} \frac{p_1}{2^i} \times 1 = p_0 + p_1 = 1, $$

i.e., the program is almost surely terminating.
# 3 Weakest pre-expectations and the arithmetical hierarchy

In this section, we study the hardness of some natural quantitative problems for weakest pre-expectations and expected derivation length.

## 3.1 Computability-aimed restrictions

This subsection is devoted to putting some restrictions on programs and on the considered notion of expectation to overcome the above computability issues.

*Algebraic numbers.* Towards that end, a solution is to target a subset of complex numbers, where simple operations like equality are decidable. We consider the set $\overline{\mathbb{Q}}$ of algebraic numbers, i.e., complex numbers in $\mathbb{C}$ that are roots of a non-zero polynomial in $\mathbb{Q}[X]$. Let $A \triangleq \overline{\mathbb{Q}} \cap \mathbb{R}$ be the real closed field of real algebraic numbers in $\mathbb{R}$. The following inclusions trivially hold (i) $\mathbb{N} \subseteq \mathbb{Q} \subseteq A \subseteq \mathbb{R} \subseteq \mathbb{C}$ and (ii) $\overline{\mathbb{Q}} \subseteq \mathbb{C}$. It was proved in [18, Proposition 2.2] that equality over $\overline{\mathbb{Q}}$ and inequality over $A$ are decidable using Cohn's representation [11] and is well-known that the product and sum over $\overline{\mathbb{Q}}$ are computable in polynomial time.

The program semantics is then restricted to matrices and density operators over the algebraic numbers. Given a totally ordered set of qubits $Q = \{q_1, \dots, q_n\}$, let $\tilde{H}_Q$ be the Hausdorff pre-Hilbert space $\overline{\mathbb{Q}}^{2^n}$ (i.e., the completeness requirement on Hilbert spaces is withdrawn) of $n$ qubits defined by $\tilde{H}_Q \triangleq \otimes_{i=1}^n \tilde{H}_{q_i}$, with $\tilde{H}_q \triangleq \overline{\mathbb{Q}}^2$ being the vector space of computational basis $\{|0\rangle, |1\rangle\}$ over the field $\overline{\mathbb{Q}}$. Let $M(\tilde{H}_Q)$ and $\mathcal{D}(\tilde{H}_Q)$ be the set of matrices and density operators on $\tilde{H}_Q$, respectively.

*Clifford+T gates.* For the program semantics to be defined on the space $\mathcal{D}(\tilde{H}_Q)$, the considered quantum gates will be restricted to gates whose corresponding unitary operators are in $M(\tilde{H}_Q)$, i.e., have a matrix representation over the algebraic numbers. We consider a restriction to the Clifford+T gates: I, X, Y, Z, H, S, CNOT, and T, whose unitary matrices are given below:

$$I \triangleq \begin{pmatrix} 1 & 0 \\ 0 & 1 \end{pmatrix}, X \triangleq \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, Y \triangleq \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}, Z \triangleq \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}, H \triangleq \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix},$$

$$S \triangleq \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 0 \\ 0 & i \end{pmatrix}, \quad \text{CNOT} \triangleq \begin{pmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \end{pmatrix}, \quad T \triangleq \begin{pmatrix} 1 & 0 \\ 0 & e^{i \frac{\pi}{4}} \end{pmatrix}.$$

The Clifford+T fragment is the set of unitary transformations generated by sequential (matrix multiplication) and parallel (Kronecker product) compositions of the gates H, S, CNOT, and T. This constitutes a reasonable restriction for unitary operators as it is known to be the simplest approximately universal fragment of quantum mechanics [1].

Moreover, the superoperator of any unitary operator of the Clifford+T fragment is an endomorphism over density operators in $\mathcal{D}(\tilde{H}_Q)$.
**Lemma 1.** The Clifford+T fragment preserves $\mathcal{D}(\tilde{\mathcal{H}}_Q)$, i.e., there exist $Q$ and $\bar{q} \in Q$ such that for each unitary operator $U$ of the Clifford+T fragment $\Phi_{U_q} \in \mathcal{D}(\tilde{\mathcal{H}}_Q) \to \mathcal{D}(\tilde{\mathcal{H}}_Q)$.

Notice that, while a restriction to Clifford+T is reasonable in terms of quantum mechanics and universality, our result can be extended by adding any quantum gate preserving the above lemma. For example, the phase shift gate, defined by $P_\varphi \triangleq \begin{pmatrix} 1 & 0 \\ 0 & e^{i\varphi} \end{pmatrix}$, preserves $\mathcal{D}(\tilde{\mathcal{H}}_Q)$ whenever $\varphi = r\pi$, for any $r \in \mathbb{Q}$.

Let $\text{Stmt}_{\text{CT}}$ be the set of statements restricted to quantum gates computing Clifford+T unitary operators (hence a subset of $\text{Stmt}$), $\text{St}_{\text{CT}}$ be the set of states whose quantum state is in $\mathcal{D}(\tilde{\mathcal{H}}_Q)$, and $\text{Conf}_{\text{CT}}$ be the set of well-formed configurations in $(\text{Stmt}_{\text{CT}} \cup \{\downarrow\}) \times \text{St}_{\text{CT}}$. Let $\text{St}_{\text{CT}}^{\text{stm}}$ be the set of states in $\text{St}_{\text{CT}}$ that are well-formed wrt statement $\text{stm}$. Once again, by abuse of notation, we will denote this set by $\text{St}$ when $\text{stm}$ is clear from the context.

A crucial observation is that $\text{Conf}_{\text{CT}}$ is closed under reduction, in the following sense. Let $\mathcal{D}_{\mathbb{A}^+}^{\text{fin}}(A) \subseteq \mathcal{D}(A)$ be the set of finitely supported sub-distributions $\delta$ with algebraic probabilities, i.e., $\delta(a) \in \mathbb{A}^+$ for all $a \in A$.

**Lemma 2.** The set $\mathcal{D}_{\mathbb{A}^+}^{\text{fin}}(\text{Conf}_{\text{CT}})$ is stable under reduction, more precisely, if $\delta \in \mathcal{D}_{\mathbb{A}^+}^{\text{fin}}(\text{Conf}_{\text{CT}})$ and $\delta \stackrel{c}{\Rightarrow}_{\mathbb{Q}} \varepsilon$, then $\varepsilon \in \mathcal{D}_{\mathbb{A}^+}^{\text{fin}}(\text{Conf}_{\text{CT}})$ and $c \in \mathbb{A}^+$.

*Computable expectations.* We also restrict the expectation codomain to algebraic numbers. Hence the considered expectations will be functions in $\text{St}_{\text{CT}} \to \mathbb{A}^+$. On its own, this restriction is not sufficient as the set $\text{St}_{\text{CT}} \to \mathbb{A}^+$ is not countable. It implies that there exist expectations in $\text{St}_{\text{CT}} \to \mathbb{A}^+$ that are not computable functions. To solve this issue, we adopt the convention by considering only computable expectations in $\text{St}_{\text{CT}} \to \mathbb{A}^+$:

$$ \mathbb{E}_{\text{CT}} \triangleq \{f \mid f : \text{St}_{\text{CT}} \to \mathbb{A}^+, f \text{ computable}\}. $$

An immediate consequence of Lemma 2 is that $\text{term}_{\text{stm}}(\sigma) \in \mathcal{D}(\text{Conf}_{\text{CT}})$ for any $\text{stm} \in \text{Stmt}_{\text{CT}}$ and $\sigma \in \text{St}_{\text{CT}}$. In consequence, $\text{qwp}_{\text{stm}} f \sigma$ is well-defined for all $f \in \text{St}_{\text{CT}}$. This justifies that in our treatment below, we restrict expectations to the class $\mathbb{E}_{\text{CT}}$. However, keep in mind that despite Lemma 2, the subdistribution $\text{term}_{\text{stm}}(\sigma)$, obtained at the limit, does not fall within $\mathcal{D}_{\mathbb{A}^+}^{\text{fin}}(A)$. It is neither finite nor are probabilities algebraic ($\mathbb{A}^+$ is not complete). In particular, in general $\text{qwp}_{\text{stm}} f \sigma$ is a real number, rather than an algebraic one.

## 3.2 Quantitative problems

We now define formally the quantitative problems that we study.

*Testing problems.* Some natural quantitative problems related to weakest pre-expectations are to determine for a given program $\text{stm}$, a given state $\sigma$, a given expectation $f$, and a given algebraic number $a$, whether the corresponding weakest pre-expectation $\text{qwp}_{\text{stm}} f \sigma$ is smaller or equal than $a$. In this setting, it makes sense to consider any possible relation in the set $\{<, \leq, =, \geq, >\} \subseteq \mathcal{P}(\mathbb{A} \times \mathbb{A})$ as one could be interested in finding precise values, (strict) upper or lower bounds.
**Definition 3.** The testing problem sets $TEST_R \subseteq Conf_{CT} \times E_{CT} \times A^+$, for $R \in \{<, \leq, =, \geq, >\}$, are defined by:

$$ (stm, \sigma, f, a) \in TEST_R :\iff (qwp_{stm} f \sigma) R a. $$

The consideration of both $TEST_{\leq}$ and $TEST_{>}^>$ may seem redundant, as $TEST_{>}^>$ can be viewed as the complement of $TEST_{\leq}$. However, it makes perfect sense to distinguish both properties, when considering the corresponding universal problems. I.e. properties for any possible input.

**Finiteness problem.** Another problem of interest consists in checking whether the weakest pre-expectations produces some finitary output.

**Definition 4.** The finiteness problem set $TEST_{\neq\infty} \subseteq Conf_{CT} \times E_{CT}$ is defined by:

$$ (stm, \sigma, f) \in TEST_{\neq\infty} :\iff qwp_{stm} f \sigma < \infty. $$

**Termination problems.** We also define two termination problems for almost sure termination and positive almost sure termination:

**Definition 5.** The sets of (positive) almost-sure terminating configurations $AST \subseteq Conf_{CT}$ ($PAST \subseteq Conf_{CT}$) are defined by:

$$ (stm, \sigma) \in AST :\iff |term_{stm}(\sigma)| = 1 $$

$$ (stm, \sigma) \in PAST :\iff edl_{stm}(\sigma) < \infty. $$

It is well-known that $PAST \subseteq AST$, cf. [8].

**Universal problems.** Another kind of natural problems arises if one tries to check some properties for each possible program input (i.e., for each state $\sigma$). We can thus defined universal properties for each of the sets described previously.

**Definition 6.** The sets of universal testing, finiteness and (positive) a.s. termination problems are defined by:

$$ (stm, f, g) \in UTEST_R \subseteq Stmt_{CT} \times E_{CT}^2 \iff \forall \sigma \in St_{CT}, (stm, \sigma, f, g(\sigma)) \in TEST_R, $$

$$ (stm, f) \in UTEST_{\neq\infty} \subseteq Stmt_{CT} \times E_{CT} \iff \forall \sigma \in St_{CT}, (stm, \sigma, f) \in TEST_{\neq\infty}, $$

$$ \mathit{stm} \in \mathit{UAST} \subseteq \mathit{Stmt}_{\mathit{CT}} \iff \forall \sigma \in \mathit{St}_{\mathit{CT}}, (\mathit{stm}, \sigma) \in \mathit{AST}, $$

$$ \mathit{stm} \in \mathit{UPAST} \subseteq \mathit{Stmt}_{\mathit{CT}} \iff \forall \sigma \in \mathit{St}_{\mathit{CT}}, (\mathit{stm}, \sigma) \in \mathit{PAST}. $$

**Example 3.** We have Cointoss $\in UA$ST and Cointoss $\in UP$AST, for the program Cointoss of Figure 3. Indeed, it was shown in Example 2 that Cointoss terminates with probability 1 and a finite expected derivation length. This property holds for any input of the domain. In the same example, we have proven (Cointoss, f) $\in TEST_{\neq\infty}$ for $f(s, \rho) = s(i)$. Indeed, we have shown the stronger property (Cointoss, f, g) $\in TEST_=$, where $g(s, (\alpha, \beta, \gamma, \delta)) = 2 - (\beta + \gamma)$.
<table><caption>**Table 1.** Completeness results for quantitative problems in the arithmetical hierarchy.</caption><thead><tr><th rowspan="2"></th><th colspan="2">Standard</th><th colspan="2">Universal</th></tr><tr><th>Problem</th><th>Class</th><th>Problem</th><th>Class</th></tr></thead><tbody><tr><td rowspan="5">Testing</td><td>TEST&gt;</td><td>Σ<sub>1</sub><sup>0</sup></td><td>UTEST&gt;</td><td>Π<sub>2</sub><sup>0 (‡)</sup></td></tr><tr><td>TEST≥</td><td>Π<sub>2</sub><sup>0 (‡)</sup></td><td>UTEST≥</td><td>Π<sub>2</sub><sup>0 (‡)</sup></td></tr><tr><td>TEST=</td><td>Π<sub>2</sub><sup>0</sup></td><td>UTEST=</td><td>Π<sub>2</sub><sup>0 (‡)</sup></td></tr><tr><td>TEST≤</td><td>Π<sub>1</sub><sup>0 (‡)</sup></td><td>UTEST≤</td><td>Π<sub>1</sub><sup>0 (‡)</sup></td></tr><tr><td>TEST&lt;</td><td>Σ<sub>2</sub><sup>0</sup></td><td>UTEST&lt;</td><td>Π<sub>3</sub><sup>0 (‡)</sup></td></tr><tr><td>Finiteness</td><td>TEST<sub>≠∞</sub></td><td>Σ<sub>2</sub><sup>0</sup></td><td>UTEST<sub>≠∞</sub></td><td>Π<sub>3</sub><sup>0 (‡)</sup></td></tr><tr><td rowspan="2">Termination</td><td>AST</td><td>Π<sub>2</sub><sup>0</sup></td><td>UAST</td><td>Π<sub>2</sub><sup>0</sup></td></tr><tr><td>PAST</td><td>Σ<sub>2</sub><sup>0</sup></td><td>UPAST</td><td>Π<sub>3</sub><sup>0</sup></td></tr></tbody></table>

## 3.3 Completeness results in the arithmetical hierarchy

In what follows, we place the introduced quantitative problems within the *arithmetical hierarchy* [33]. The arithmetical hierarchy is a means to classify and relate *undecidable* problems wrt. to their inherent difficulty, measured in terms of the number of (unbounded) quantifier alternations needed to state the problem as a formula in first-order arithmetic, based on a decidable (recursive) predicate.

*Reminder on the arithmetical hierarchy.* Classes of the arithmetical hierarchy are defined inductively as follows:

$$ \Pi_0^0 = \Sigma_0^0 \triangleq_{\text{REC}} \text{REC} \text{ being the class of decidable problems (recursive sets)} $$

$$ \Pi_{n+1}^0 \triangleq \{ \psi \mid \exists \phi \in \Sigma_n^0, \forall \bar{x}. (\psi(\bar{x}) \iff \forall \bar{y}. \phi(\bar{x}, \bar{y})) \}, $$

$$ \Sigma_{n+1}^0 \triangleq \{ \psi \mid \exists \phi \in \Pi_n^0, \forall \bar{x}. (\psi(\bar{x}) \iff \exists \bar{y}. \phi(\bar{x}, \bar{y})) \}. $$

For each $n$, $\Pi_n^0$ is the complement of $\Sigma_n^0$ (i.e., $\Pi_n^0 = \text{co-}\Sigma_n^0$, and vice versa) and it is a well-known result that $\Sigma_1^0$ and $\Pi_1^0$ correspond to the classes RE of recursively enumerable (i.e., semi-decidable) problems and co-RE of co-recursively enumerable (i.e., co-semi-decidable) problems, respectively. Given the sets $A \subseteq X$ and $B \subseteq Y$, we write $A \leq_m B$ ($A$ is many-one reducible to $B$) if there exists a computable function $f: X \to Y$ such that $\forall x \in X, x \in A \iff f(x) \in B$. Given a class C of the arithmetical hierarchy and a set $A$, $A$ is C-hard if $\forall B \in C, B \leq_m A$. A set $A$ is C-complete if $A \in C$ and $A$ is C-hard. It is well-known that if a set $A$ is C-complete then its complement, noted co-A, is (co-C)-complete.

*Results.* Table 1 associates the quantum decision problems to the corresponding classes in the arithmetical hierarchy for which we have proven them complete, that is, we have proven membership and hardness for the corresponding class. Some of the results may seem surprising. For instance, the testing problem $TEST>$, i.e., deciding $qwp_{stm} f \sigma > a$ within the Clifford+T fragment, turns
out to be recursive enumerable. It is thus not more difficult than the halting problem $\mathcal{H}$.\* Remarkable, through the restriction to the Clifford+T fragment, corresponding problems are ranked within the arithmetical hierarchy identical to their non-quantum counterparts ([36,24]). This observation holds for all problems apart those marked with (‡) which, to the best of our knowledge, have not been studied in a classical/probabilistic setting.

A crucial observation towards these results is that, restricting to the Clifford+T fragment, the weakest pre-expectation of a program P can be approximated through computable transformers $qwp_{\text{stm}}^{\le n} : E_{\text{CT}} \to E_{\text{CT}}$ that limit execution of \texttt{stm} to at most $n \in \mathbb{N}$ reduction steps. That is,

$$qwp_{\text{stm}}^{\le n} f \sigma \triangleq E_{\text{term}_{\text{stm}}^{\le n}}(\sigma)(f),$$

for $\text{term}_{\text{stm}}^{\le n}(\sigma)$ the distribution of terminal configurations obtained within $n$ reduction steps, when evaluating $(\text{stm}, \sigma)$. With regards to the above mentioned $\text{TEST}_> \in \Sigma_1^0$ for instance, observe that:

$$ \begin{align*} (\text{stm}, f, \sigma, a) \in \text{TEST}_> &\iff qwp_{\text{stm}} f \sigma > a \\ &\iff \lim_{i \to \infty} qwp_{\text{stm}}^{\le n} f \sigma > a \\ &\iff \exists n \in \mathbb{N}, \exists \delta \in A^+ \setminus \{0\}, qwp_{\text{stm}}^{\le n} f \sigma \ge a + \delta. \end{align*} $$

Crucially, the predicate $qwp_{\text{stm}}^{\le n} f \sigma \ge a + \delta$ becomes computable. In essence, this is a consequence of Lemma 2: The n-th step normal form distribution $\text{term}_{\text{stm}}^{\le n}(\sigma)$ is finite and computable, as $f$ is computable so is thus $qwp_{\text{stm}}^{\le n} f \sigma$. From here, the result follows now as equality on $A$ is decidable. The proof of this, as well as all completeness proofs listed in Table 1 can be found in the Appendix. The following constitutes our first main result.

**Theorem 1.** All completeness results in Table 1 hold.

# 4 Quantum expectation transformers

We now define a notion of quantum expectation transformer as a means to compute symbolically the weakest pre-expectation of a program. To this end, we first introduce some preliminary notations in order to lighten the presentation.

*Notations.* For any expression $e$, $\llbracket e \rrbracket$ is a shorthand notation for the function $\lambda(s, \rho).\llbracket e \rrbracket^s \in \text{St} \to \mathbb{R}^{+\infty}$. We will also use $f[x := e]$ for the expectation $\lambda(s, \rho).f(s[x := \llbracket e \rrbracket^s], \rho)$. Similarly, for a given map $\chi : \mathcal{D}(\mathcal{H}_Q) \to \mathcal{D}(\mathcal{H}_Q)$, $f[\chi] \triangleq \lambda(s, \rho).f(s, \chi(\rho))$. We will also sometimes group such state modifications, for instance, $f[x := e; \chi]$ stands for $(f[x := e])[\chi]$ and $f[x := e, y := e']$ stands for $(f[x := e])[y := e']$.

<footnote>\*In our context the halting set $\mathcal{H}$ can be defined as the class of classical programs and states $(P, \sigma)$ for which P is halting on $\sigma$.</footnote>
$$
\begin{align*}
\text{qet}[\text{skip}]\{f\} &\triangleq f \\
\text{qet}[x = e]\{f\} &\triangleq f[x := e] \\
\text{qet}[\text{stm}_1; \text{stm}_2]\{f\} &\triangleq \text{qet}[\text{stm}_1]\{\text{qet}[\text{stm}_2]\{f\}\} \\
\text{qet}[\text{if } b \text{ then } \text{stm}_1 \text{ else } \text{stm}_2]\{f\} &\triangleq \text{qet}[\text{stm}_1]\{f\} +_{[b]} \text{qet}[\text{stm}_2]\{f\} \\
\text{qet}[\text{while } b \text{ do } \text{stm}]\{f\} &\triangleq \text{lfp}(\lambda F.\text{qet}[\text{stm}]\{F\} +_{[b]} f) \\
\text{qet}[\bar{q} * = U]\{f\} &\triangleq f[\Phi_{U_{\bar{q}}}] \\
\text{qet}[x = \text{meas } q_i]\{f\} &\triangleq f[x := 0; m_{0,i}] +_{p_{0,i}} f[x := 1; m_{1,i}].
\end{align*}
$$

<caption>Fig. 5. Quantum expectation Transformer $qet[\cdot]\{\cdot\}$</caption>

For $p \in \text{St} \to [0, 1]$ and $f, g \in \text{St} \to \mathbb{R}^{+\infty}$, $f +_p g$ denotes the function $\lambda\sigma.p(\sigma) \cdot f(\sigma) + (1-p(\sigma)) \cdot g(\sigma) \in \text{St} \to \mathbb{R}^{+\infty}$, similar we use $f \cdot g$ to denote $\lambda\sigma.f(\sigma) \cdot g(\sigma) \in \text{St} \to \mathbb{R}^{+\infty}$. Thus, for instance, $f[x := x+1] +_{[x=1]} f$ behaves like $f$, except that $x$ is first incremented when applied to states with classical variable $x$ equal to 1. In correspondence to the normalization of quantum state $m_{k,i}$, we define probabilities $p_{k,i} \triangleq \lambda\rho.\text{tr}(M_{k,i}\rho M_{k,i}^\dagger)$. We overload this function from $\mathcal{D}(\mathcal{H}_Q)$ to $\text{St}$ s.t. $p_{k,i}(s, \rho) = p_{k,i}(\rho)$. In this way, $f[x := 0; m_{0,i}] +_{p_{0,i}} f[x := 1; m_{1,i}]$ computes precisely the expected value of $f$ on the distribution of states obtained by measuring the $i$-th qubit and assigning the outcome to classical variable $x$.

Finally, we denote by $\le$ also the pointwise extension of the order from $\mathbb{R}^{+\infty}$ to functions, that is, $f \le g$ holds iff $\forall \sigma \in \text{St}, f(\sigma) \le g(\sigma)$.

**Definition 7 (Quantum expectation transformer).** The quantum expectation transformer consists in a program semantics mapping expectations to expectations in a continuation passing style

$$
\text{qet}[\cdot]\{\cdot\} : \text{Stmt} \to (\text{St} \to \mathbb{R}^{+\infty}) \to (\text{St} \to \mathbb{R}^{+\infty})
$$

and is defined inductively on statements in Figure 5.

This transformer corresponds to the notion of *expected value transformer* of [5] on the Kegelspitze $S = (\mathbb{R}^{+\infty}, +_f)$, with $+_f$ being the forgetful addition. In the case of loops, the least fixed point $\text{lfp}$ is defined with respect to the pointwise ordering on the function space $\text{St} \to \mathbb{R}^{+\infty}$. Equipped with this ordering, this space forms a $\omega$-CPO. As the quantum transformer can be shown to be $\omega$-continuous, the fixed-point is always defined, cf. [43].

**Theorem 2 (Adequacy).** The following holds:

$$
\forall \text{stm} \in \text{Stmt}, \forall f : \text{St} \to \mathbb{R}^{+\infty}, \text{qwp}_{\text{stm}}(f) = \text{qet}[\text{stm}]\{f\}.
$$

Apart from continuity, the quantum expectation transformer satisfies several useful laws, see Figure 6. The (monotonicity) Law permits us to reason modulo
$$continuity \qquad qet[stm] \{sup_i f_i\} = sup_i qet[stm] \{f_i\}$$

$$monotonicity \qquad f \le g \Rightarrow qet[stm] \{f\} \le qet[stm] \{g\}$$

$$up. \ invariance \ ([[\neg b]] \cdot f \le g \wedge [[b]] \cdot qet[stm] \{g\} \le g) \Rightarrow qet[while b do STM] \{f\} \le g$$

<caption>**Fig. 6.** Universal laws derivable for the quantum expectation transformer.</caption>

upper-bounds: actual expectations can be always substituted by upper-bounds. It is in fact an immediate consequence from the (continuity) Law, which is defined for any $\omega$-chain $(f_i)_i$. The (up. invariance) Law constitutes a generalization of the notion of invariant stemming from Hoare calculus. It is used to find closed-form upper-bounds $g$ to expectations $f$ of loops. The pre-conditions state that $g$ should dominate $f$ on states where the loop would immediately exist, and otherwise, should remain invariant under iteration. It is worth mentioning that this proof rule is not only sound, but also complete, in the sense that any upper-bound satisfies the two constraints. The following example illustrates the use of this rule on the running example.

**Example 4.** Following up on Example 2, we over-approximate $qet[\text{Cointoss}] \{f\}$, for $f(s, \rho) = s(i)$ the post-expectation measuring the classical variable $i$.

To this end, observe that the function $g: \text{St} \to \mathbb{R}^{+\infty}$ is an upper-invariant (Figure 6) to the while loop `while x do STM`, given a post-expectation $f: \text{St} \to \mathbb{R}^{+\infty}$. Recall that the loop body `STM` comprises $(i = i+1; q*=H; x = \text{meas } q)$. To fulfill the conditions of the (up. invariance) Law the following inequalities have to be met

$$[[\neg x]] \cdot f \le g \qquad [[x]] \cdot qet[i = i+1; q*=H; x = \text{meas } q] \{g\} \le g. \quad (5)$$

By unfolding the definition, we see

$$ \begin{align*} qet[i = i+1; q*=H; x = \text{meas } q] \{g\} & = qet[i = i+1] \{qet[q*=H] \{qet[x = \text{meas } q] \{g\}\}\} \\ & = qet[i = i+1] \{qet[q*=H] \{g[x:=0; m_{0,1}] + p_{0,1} g[x:=1; m_{1,1}]\}\} \\ & = qet[i = i+1] \{g[x:=0; m_{0,1}; \Phi_H] + p_{0,1} \cdot \Phi_H g[x:=1; m_{1,1}; \Phi_H]\} \\ & = g[x:=0; m_{0,1}; \Phi_H; i:=i+1] + p_{0,1} \cdot \Phi_H g[x:=1; m_{1,1}; \Phi_H; i:=i+1] \\ & = \lambda(s, \rho) \cdot \sum_{k \in \{0,1\}} p_{k,1}(\Phi_H(\rho)) \cdot g(s[x = k, i:=i+1], m_{k,1}(\Phi_H(\rho))) \dots \end{align*} $$

By using the identities computed already in Example 2, we thus obtain

$$qet[stm] \{g\} (s, \binom{\alpha}{\gamma} \binom{\beta}{\delta}) = \sum_{k \in \{0,1\}} p_k \cdot g(s[x = k, i:=i+1], \rho_k), \quad (6)$$

where, as in Example 2, $p_0 = \frac{1+\beta+\gamma}{2}$, $p_1 = \frac{1-(\beta+\gamma)}{2}$, $\rho_0 = \binom{1}{0}, \binom{0}{0}$ and $\rho_1 = \binom{1}{0}, \binom{0}{0}$
We claim that $g(s, (\begin{pmatrix} \alpha \\ \gamma \\ \beta \\ \delta \end{pmatrix})) \triangleq s(i) + s(x) \cdot (2 - (\beta + \gamma))$ is an upper-bound to the pre-expectation of the while loop wrt. to the post expectation $f$. To this end, we check (5). The first inequality is trivially satisfied. Concerning the second, notice that by definition,

$$g(s[x = 0, i:=i+1], (\begin{pmatrix} 1 & 0 \\ 0 & 0 \end{pmatrix})) = s(i)+1 \quad \text{and} \quad g(s[x = 1, i:=i+1], (\begin{pmatrix} 0 & 0 \\ 0 & 1 \end{pmatrix})) = s(i)+3.$$

By (6) we have

$$ \begin{aligned} \text{qet[stm]}\{g\}(s, (\begin{pmatrix} \alpha \\ \gamma \\ \beta \\ \delta \end{pmatrix})) &= \frac{1+\beta+\gamma}{2}(s(i)+1) + \frac{1-(\beta+\gamma)}{2}(s(i)+3) \\ &= (s(i)+2) - (\beta+\gamma) = g(s, (\begin{pmatrix} \alpha \\ \gamma \\ \beta \\ \delta \end{pmatrix})), \end{aligned} $$

from which now the second constraint follows by case analysis on the value of $x$. Hence $\text{qet[while } x \text{ do } \text{stm}]\{f\} \le g$ and, by monotonicity (Figure 6),

$$ \begin{aligned} \text{qet[Cointoss]}\{f\}(s, (\begin{pmatrix} \alpha \\ \gamma \\ \beta \\ \delta \end{pmatrix})) &\le \text{qet}[x = \text{tt}; i = 0]\{g\}(s, (\begin{pmatrix} \alpha \\ \gamma \\ \beta \\ \delta \end{pmatrix})) \\ &= g([x:=1, i:=0], (\begin{pmatrix} \alpha \\ \gamma \\ \beta \\ \delta \end{pmatrix})) = 2 - (\beta + \gamma). \end{aligned} $$

Note that, in this case, the computed bound is exact.

One question of interest is to find the $\text{qet}[\cdot]\{\cdot\}$ of a given statement. We obtain the following completeness results as a corollary of Theorems 11, 12, and 2 on the Clifford+T fragment.

**Corollary 1.** *The following completeness results hold:*

- $\{(\text{stm}, f, g) \in \text{StmtCT} \times \mathbb{E}_{\text{CT}}^2 | \forall \sigma, \text{qet[stm]}\{f\}(\sigma) = g(\sigma)\} \text{ is } \Pi_2^0\text{-complete.}$

- $\{(\text{stm}, f, g) \in \text{StmtCT} \times \mathbb{E}_{\text{CT}}^2 | \forall \sigma, \text{qet[stm]}\{f\}(\sigma) \le g(\sigma)\} \text{ is } \Pi_1^0\text{-complete.}$

The same kind of result can be straightforwardly obtained for each of the quantitative problems defined in previous section. All the corresponding sets are undecidable: they are at best (co-)semi-decidable as illustrated by Figure 1. This motivates us for restricting the problem a bit further to find a class of functions for which the quantitative problems for $wp_{\text{stm}} f$ can be decided.

# 5 Decidability of qet inference over a real closed field

Corollary 1 illustrates that it is not sufficient to relax the problem of finding the quantum expectation transformer of a given statement to upper bounds in order to make it decidable. The undecidability of finding the quantum expectation transformer of a given program is due to two other issues:

- Issue 1: the computation of a fixed-point for $\text{qet}[\cdot]\{\cdot\}$ in the case of loops,

- Issue 2: the check for inequalities over the set $\mathbb{E}_{\text{CT}}$, whose first-order theory is not decidable.

This section is devoted to overcome these two issues by finding an expressive fragment on which the inference of an upper-bound of the quantum expectation transformer becomes decidable.
<figure><img src="image_4.png" /><figcaption>Fig. 7. Term representations of $qinf[\cdot] \{\cdot\}$ and their corresponding side-conditions.</figcaption></figure>

## 5.1 Symbolic inference

As a first step towards automated inference, we define a symbolic variant of the quantum expectation transformer in Figure 7. In the case of conditionals, loops, and measurements, we will use fresh variables for expectations; side conditions will guarantee that these variables indeed denote (upper-bounds to) the corresponding expectations. This means that the symbolic version yields correct results only when the expectations assigned to these variables satisfy all the side conditions. By solving the generated constraints, viz., by finding an interpretation of ascribed variables that satisfy the imposed side-conditions, we effectively arrive at an inference procedure overcoming Issue 1.

To formalize this approach, we associate a unique label $\ell$ with each loop, conditional, and measurement, occurring in the considered program. This follows standard practice in (static) program analysis, cf. [14]. Notationally, we write `while$^\ell$ b do STM / if$^\ell$ b then STM else STM2 / meas$^\ell$ q`. Such labels permit us to associate a unique expectation variable $X_\ell$ to each of these constructs. Given a set of such expectation variables `EVar`, the set of terms `ETerm`, upon which the symbolic quantum expectation transformer operates, is defined according to the following grammar:

$$ETerm F, G ::= X \mid F[x := e] \mid F[\chi] \mid F +_p G,$$

where X stands for arbitrary expectations variable in `EVar`. As stressed above, X will be used to denote certain expectations wrt. loops, conditionals, and measurements. We have already introduced the notations $F[x := e]$ and $F[\chi]$ to represent updates to the classical and quantum state, respectively, of the expectation term $F$. Here, $\chi$ will always denote a finite composition of superoperators $\phi_U$ and measurements $m_{k,i}$. By ensuring that normalization of quantum states
$m_{k,i}(\rho)$ is never considered in the degenerate case of a zero-probability measurement $p_{k,i}(\rho)$, it will thereby always be possible to write $\chi$ as $\lambda\rho \frac{M\rho M^\dagger}{\mathrm{tr}(N\rho N^\dagger)}$, for some $M \in \mathcal{M}(\tilde{\mathcal{H}}_Q)$ in the Clifford+T fragment. Finally, following the same reasoning, in the barycentric sum $F +_p G$ the probability $p$ is a function in the quantum state, and will always be of general form $\lambda\rho \frac{\mathrm{tr}(M\rho M^\dagger)}{\mathrm{tr}(N\rho N^\dagger)}$, for some $M, N \in \mathcal{M}(\tilde{\mathcal{H}}_Q)$ in the Clifford+T fragment. Similar to before, we may use the notation $F[x := e; \chi]$.

The symbolic variation of the expectation transformer can now be defined as

$$ \mathrm{qinf}[\cdot] \{ \cdot \} : \mathrm{Stmt} \to \mathrm{ETerm} \to \mathrm{ETerm}, $$

generating also a set of side-conditions of the shape $\Gamma \vdash F \leq G$, with the intended meaning that $G$ binds $F$ on all input states that satisfy the predicate $\Gamma$. The full definition of $\mathrm{qinfer}$ is given in Figure 7. As already hinted, the side conditions ensure that introduced variables $X_\ell$ indeed yield an upper-bound on the corresponding expectation, in the case of conditionals by case-analysis, and in the case of loops via an application of the upper-invariant law from Figure 6. In the case of measurements, $m_{k,i}$ and $p_{k,i}$ are defined exactly as before. Here, we single out the two cases where the probability of a measurement, either $p_{0,i}(\rho) = \mathrm{tr}(M_{0,i}\rho) = \mathrm{tr}(M_{0,i}\rho M_{0,i}^\dagger)$ or $p_{1,i}(\rho) = 1 - p_{0,i}(\rho)$, is zero. This way, we avoid the case analysis underlying the definition of $m_{k,i}$ and may, wlog., assume that it is indeed of the form $\lambda\rho \frac{M_{k,i}\rho M_{k,i}^\dagger}{\mathrm{tr}(M_{k,i}\rho M_{k,i}^\dagger)}$, with non-zero trace $\mathrm{tr}(M_{k,i}\rho M_{k,i}^\dagger)$.

**Example 5.** In correspondence to Example 4, let us consider the application of the inference procedure on the program Cointoss, wrt. to the post-expectation $f(s, \rho) = s(i)$. We label the loop and measurement with $m$ and $w$, respectively.

Let $X$ denote the post-expectation $f$. Unfolding the definition, we see

$$ \begin{aligned} \mathrm{qinf}[\mathrm{Cointoss}]\{X\} &= \mathrm{qinf}[x = \mathrm{tt}; i = 0; \text{while}^w x \mathrm{do} \mathrm{stm}]\{X\} \\ &= X_w[x:=1; i:=0], \end{aligned} $$

generating the two side-conditions $x \vdash X_m[\Phi_H; i:=i+1] \leq X_w$ and $\neg x \vdash X \leq X_w$. The left-hand side of the first constraint is obtained from

$$ \begin{aligned} \mathrm{qinf}[\mathrm{stm}]\{X_w\} &= \mathrm{qinf}[i = i+1]\{\mathrm{qinf}[q^* = H]\}\{\mathrm{qinf}[\mathrm{meas}^m q]\{X_w\}\} \\ &= X_m[\Phi_H; i:=i+1]. \end{aligned} $$

Note that this expansion generates further constraints, this time on $X_m$ representing the measurement. Specifically, it yields the following constraints:

$$ p_{1-k,1} = 0 \vdash X_w[x:=k; m_{k,1}] \leq X_m, \quad (\text{for } k \in \{0,1\}), $$

$$ p_{0,1} \neq 0 \neq p_{1,1} \vdash X_w[x:=0; m_{0,1}] +_{p_{0,1}} X_w[x:=1; m_{1,1}] \leq X_m. $$

Using the analysis from Example 4, we interpret $X_w$ and $X_m$ as:

$$ \alpha(X_w) \triangleq \lambda(s, \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix}). s(i) + s(x)(2 - (\beta + \gamma)), $$

$$ \alpha(X_m) \triangleq \lambda(s, \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix}). s(i) + 2 - 2\alpha. $$
Furthermore, we interpret the input variable $X$ as $f$, i.e., $\alpha(X) \triangleq \lambda(s, \rho)$. $s(i)$. Notice how $\alpha(X_w)$ just corresponds to the upper-invariant $g$ derived in Example 4. Using the assignment, it is now standard to check that it is a solution to the five constraints. For instance, considering states $\sigma = (\{i:=n, x:=x\}, \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix})$, the ultimate constraint amount to the implication

$$ \alpha \neq 0 \neq \delta \Rightarrow n + \alpha (n + 2) \leq n + 2 - 2\alpha, $$

which trivially holds. Finally, recall $qinf[Cointoss]\{X\} = X_w[x:=1; i:=0]$. This term is interpreted as $\lambda(s, \begin{pmatrix} \alpha & \beta \\ \gamma & \delta \end{pmatrix})$. $2 - (\beta + \gamma)$, yielding the optimal bound computed in Example 4.

**Example 6.** Re-consider program RUS depicted in Figure 1. We are interested in an upper-bound on the number of T-gates, counted by the program variable i. As before, we label the loop and measurement with m and w, respectively. Let

$$ \text{stm} = \overbrace{\text{qinf[stm}_0\{X\}}^{\text{stm}_0} = \overbrace{\text{qinf[stm}_1\{X\}}^{\text{stm}_1} = \dots = \overbrace{\text{qinf[stm}_n\{X\}}^{\text{stm}_n}}; \quad \text{x = meas}^m \text{q}_2, $$

be the body of the while loop statement (see Figure 1). We proceed with the analysis backwards. By the rules of Figure 7 it holds that $qinf[\text{stm}_0]\{F\} = F[\Phi; i:=i+2]$ for any $F$, where $\Phi$ gives the quantum state updates within $\text{stm}_0$. Unfolding definitions, we have

$$ qinf[RUS]\{X\} = X_w[x:=0; i:=1] \text{ with } x \vdash X_m[\Phi; i:=i+2] \leq X_w, \neg x \vdash X \leq X_w, $$

since, by the above observation,

$$ qinf[\text{stm}][X_w] = qinf[\text{stm}_0][qinf[x = \text{meas}^m q_2][X_w]] = X_m[\Phi; i:=i+2], $$

subject to the following additional constraints stemming from measurements:

$$ \begin{align*} p_{1-k,2} &= 0 \vdash X_w[x:=k; m_{k,2}] \leq X_m, && (\text{for } k \in \{0, 1\}), \\ p_{0,2} &= 0 \neq p_{1,2} \vdash X_w[x:=0; m_{0,2}] + p_{0,2} X_w[x:=1; m_{1,2}] \leq X_m. \end{align*} $$

Taking $\alpha(X) \triangleq \lambda(s, \rho)$. $s(i)$ and solving the constraints yields a constant upper bound of $8/3$ on the expected number of T-gates used by the program. This is due to the fact that the probability of the internal measurement is always $3/4$. Note that this bound is tight.

The transformer $qinfer$ can be linked to $qet$ of course only when variables $X_\ell$ are interpreted in a way that the side conditions generated by $infer$ are met. To spell this out formally, let $\alpha: EVar \to E_{CT}$ be an assignment of expectations to variables in $EVar$, and let $[[F]]^\alpha: E_{CT}$ denote the interpretation of $F \in ETerm$ under $\alpha$ defined in the natural way, e.g., $[[X_\ell]]^\alpha = \alpha(X_\ell)$, $[[F[\chi]]]^\alpha = [[F]]^\alpha[\chi]$, etc.

We say that a constraint $\Gamma \vdash F \leq G$ is valid under $\alpha$ if $[[F]]^\alpha(\sigma) \leq [[G]]^\alpha(\sigma)$ holds for all states $\sigma \in St_{CT}$ with $\Gamma(\sigma)$. An assignment $\alpha$ is a solution to a set
of constraints $\mathcal{C}$, if it makes every constraint in $\mathcal{C}$ valid. Finally, we say $\alpha$ is a solution to $\text{qinf}[\text{stm}]{f}$ if it is a solution to the set of constraints generated by $\text{qinf}[\text{stm}]{f}$. We have the following correspondence:

**Theorem 3.** For any $\alpha \in \text{EVar} \to \text{E}_{\text{CT}}$, if $\alpha$ is solution to $\text{qinf}[\text{stm}]{F} = G$, then it holds that $\text{qet}[\text{stm}]{[F]^\alpha} \le [G]^\alpha$.

It is worth mentioning that the above procedure could have been defined without restriction to the full space $\text{St} \to \mathbb{R}^{+\infty}$ of expectations. In this case, this symbolic approach is also complete, in the sense that if $\text{qet}[\text{stm}]{f} = g$ then $\text{qinf}[\text{stm}]{X} = G$ for some $G$ such that the side-conditions have a solution $\alpha$, with $\alpha(X) = f$ and $[G]^\alpha = g$. As our main focus is on decidability, however, we have made the choice to restrict ourself to the Clifford+T setting.

## 5.2 Restriction to polynomials over the real closed field $\mathbb{A}$

We now turn our eyes towards constraint solving, addressing the remaining Issue 2 through restricting the domain of expectations to polynomials over algebraic numbers. To be more precise, we consider the following problem.

**Definition 8.** Let $E \subseteq \text{E}_{\text{CT}}$ be a class of expectations. The inference problem $\text{QINFER}(E) \subseteq \text{Stmt}_{\text{CT}} \times E \times (\text{EVar} \to E)$ is given by

$$ (\text{stm}, f, \alpha) \in \text{QINFER}(E) \iff \alpha[X := f] \text{ is solution to } \text{qinf}[\text{stm}]{X} $$

In the above definition, $(\text{stm}, f, \alpha) \in \text{QINFER}(E)$ is satisfied if the statement $\text{stm}$ has solution $\alpha[X := f]$ wrt. the expectation $f$. Hence it can be seen as checking whether $f$ is a post-expectation for $\text{stm}$. In particular, any solution $\alpha[X := f]$ constitutes an upper bound on the weakest pre-expectation of $f$ (see Theorem 3). We will now see that $\text{QINFER}(E)$ is decidable, for $E$ the set of (real algebraic) polynomial expectations of (arbitrary but fixed) degree $d$. For states $\text{St}_{\text{CT}}$ over $n$ classical variables $y_1, \dots, y_n$ and $m$ qubits, let $\mathbb{A}^d[\text{St}_{\text{CT}}]$ denotes the class of functions of polynomial expectations of the form

$$ \lambda(\{y_i := Y_i\}_{1 \le i \le n}, (A_{j,k} + iB_{j,k})_{1 \le j,k \le 2^m}). P, \quad (7) $$

where variables $Y_i$ refer to the classical, where variables $A_{j,k}$ and $B_{j,k}$ refer to the real part and imaginary part, respectively, of each algebraic coefficient in the quantum state. Further, $P \in \mathbb{A}[Y_1, \dots, Y_n, A_{1,1}, \dots, A_{2^m,2^m}, B_{1,1}, \dots, B_{2^m,2^m}]$ is a multivariate polynomial with coefficients in $\mathbb{A}$. The index $d$ refers to the (total) degree of the underlying polynomial $P$. For instance,

$$ \lambda(\{x := X; i := I\}, \binom{A_{1,1}+iB_{1,1} \ A_{1,2}+iB_{1,2}}{A_{2,1}+iB_{2,1} \ A_{2,2}+iB_{2,2}}). I + X(2 - (A_{1,2} + A_{2,1})) \in \mathbb{A}^2[\text{St}_{\text{CT}}] $$

One important remark here is that we allow for possibly negative polynomials whereas expectations only output positive real algebraic numbers. Consequently, some side conditions are put on the admissible coefficients $A_{j,k}$ and $B_{j,k}$ of the input density matrix to preserve this condition (the matrix is positive, has trace
1, is hermitian). For example, $\sum_{i=1}^{2^m} A_{i,i} = 1$, $\sum_{i=1}^{2^m} B_{i,i} = 0$ (trace is 1) and $\forall i, k, A_{i,k} = A_{k,i}$ and $B_{i,k} = -B_{k,i}$ (self-adjointness). One can easily check that the expectations defined in Example 5 are in $\mathbb{A}^d[\mathrm{St}_{\mathrm{CT}}]$, for $d \ge 1$.

The restriction to polynomials is made on purpose as quantifier elimination is decidable in the theory of real closed fields, a well known result due to Tarski and Seidenberg. Recall that the theory of real closed fields is the first-order theory in which the primitive operations are multiplication, addition, the order relation $\le$, and the constants 0 and 1. Consequently, the only numbers that can be defined are the real algebraic numbers. Specifically, we will make use of the following result, quantifying the complexity of the quantifier elimination decision procedure as a function exponential in number of variables, and double-exponential in the number of quantifier alternations.

**Proposition 1 ([21, Theorem 6]).** Let $\mathbf{A}$ be an integral ring over a real closed field $\mathbf{R}$. Let $\psi = Q_1\vec{x}_1.Q_2\vec{x}_2.\cdots Q_i\vec{x}_i$. $\phi$ be a formula in prenex-normal form, where $\forall k, Q_k \in \{\forall,\exists\}, Q_k \ne Q_{k+1}$, and $\phi$ is a quantifier-free formula over $i$ variables and $j$ atomic propositions of the shape $P \ge 0$, each $P$ being a polynomial of degree at most $d$ with coefficients in $\mathbf{A}$. There exists an algorithm computing a quantifier-free formula equivalent to $\psi$ in time $O(|\psi|) \cdot (jd)^{i^{O(1)}}$.

As $\mathbf{A}$ constitutes both an integral ring and a real closed field, the above theorem is in particular applicable taking $\mathbf{A} = \mathbf{R} \triangleq \mathbf{A}$. In the particular case where $\psi$ is a closed formula, the resulting quantifier-free formula is simply a Boolean combination of inequalities over constants from $\mathbf{A}$. Since we already observed that these can be decided in polynomial time, the above proposition thus implies that validity of $\psi$ is decidable under the given time bound.

By restricting assignment $\alpha$ to polynomial expectations, it becomes decidable to check that $\alpha$ is a solution to a given constraint set $C$. Indeed, under such a polynomial assignment $\alpha$, a constraint $\Gamma \vdash F \le G$ becomes expressible as a formula in the theory of real closed field $\mathbf{A}$. By letting $\alpha$ range over polynomial expectations with undetermined coefficients, we can this way arrive at the main decidability result of this section.

**Theorem 4.** For any degree $d \in \mathbb{N}$, $d \ge 1$, the problem $\mathrm{QINFER}(\mathbb{A}^d[\mathrm{St}_{\mathrm{CT}}])$ is decidable in time $2^{2^{dO(n)}}$, where $n$ is the size of the considered program.

## 5.3 Practical algorithm

Theorem 4 established a computable algorithm on the inference of upper bounds on weakest pre-expectation on quantitative program properties of any given mixed classical-quantum program. Nevertheless, the complexity of this algorithm — double-exponential in the program size — is forbiddingly high. In order to turn this procedure into a practical algorithm, we have to tame this inherent complexity. For this, significant further restrictions on the class of bounding functions are necessary. We propose to proceed as follows. (1) *Bounding functions*: in (7) we restricted the class of expectations to polynomials, which in turn
yield a bound on the weakest pre-expectation. Based on an analysis of concrete examples considered in the literature (e.g., [29,5]), this can be tightened further to degree 2 polynomials. (2) *Approximate solutions*: Theorem 4 rests upon (the decidability) of quantifier elimination. Thus the constraints *C* induced through the symbolic inference of qinf[stm]{X} = *G* (*G*, *X* ∈ ETerm) are solved exactly. Over-approximation, however, suffices, if we are only interested in soundness of the inference mechanism.

The restriction of the class of bounding functions is in essence a question of applicability of the automation, taking into account particular use-cases. With respect to approximate solutions, we observe that the actual constraints *C* considered have at most one quantifier alternation and admit a quantifier prenex of the form ∃*∀**, that is, a sequence of existential quantifier follows by a sequence of universal quantifiers. Roughly speaking the existential quantifiers refer to the inference of coefficients in the bounding polynomials, while the universal quantifiers refer to program variables. It is well-known that universal quantification in optimization problems can be turned into existential quantification, like Farka's lemma or generalizations thereof, cf. [37,19]. (E.g., [6,28] for instances of this approach for the inference of expected program costs.)

Summarizing, the inference mechanism detailed in Section 5.2 can be overapproximated to generate purely existential constraints. The latter can be effectively solved via SMT. We expect that (full) automation of the inference mechanism can capitalize on these ideas. Working out the details and in particular implementation of an effective prototype is subject to future work.

# 6 Conclusion and future work

We have studied the complexity and inference of techniques for obtaining qualitative program properties. One particular property of interest would be the cost of quantum programs, that is average time, average number of gates, mean value of a variable, etc. We show that these problems were undecidable in general by placing them in the arithmetic hierarchy and saw that inference could become decidable on a restricted fragment: quantum gates in Clifford+T and a function space with a decidable theory (polynomials of bounded degree over a real closed field). Further, we sketch how the latter can be transformed into an efficient synthesis method.

Many open questions remain. The studied notion of expectation transformer describes *local* properties of the quantum state, while it would be interesting to extend this technique to the *global* state so as to study a mixed state in a quantum-only setting (without classical variables and stores). Another question of interest is to what extent a characterization of the quantum class ZBQP, the class of problems computed by quantum programs in polynomial expected runtime, could be obtained using this tool.
References

1. Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Physical Review A **70**(5), 052328 (2004)

2. Altenkirch, T., Grattage, J.: A functional quantum programming language. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings. pp. 249-258. IEEE Computer Society (2005). https://doi.org/10.1109/LICS.2005.1, https://doi.org/10.1109/LICS.2005.1

3. Arute, F., Arya, K., et al.: Quantum supremacy using a programmable superconducting processor. Nature **574**, 505-510 (2019). https://doi.org/10.1038/s41586-019-1666-5

4. Avanzini, M., Barthe, G., Lago, U.D.: On continuation-passing transformations and expected cost analysis. Proc. of the ACM on Programming Languages **5**(ICFP), 1-30 (2021). https://doi.org/10.1145/3473592, https://doi.org/10.1145/3473592

5. Avanzini, M., Moser, G., Péchoux, R., Perdrix, S., Zamdzhiev, V.: Quantum expectation transformers for cost analysis. In: LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022. pp. 10:1-10:13 (2022). https://doi.org/10.1145/3531130.3533332

6. Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. of the ACM on Programming Languages **4**(OOPSLA), 172:1-172:30 (2020). https://doi.org/10.1145/3428240, https://doi.org/10.1145/3428240

7. Avanzini, M., Moser, G., Schaper, M.: Automated expected value analysis of recursive programs. Proceedings of the ACM on Programming Languages **7**(PLDI), 1050-1072 (2023). https://doi.org/10.1145/3591263

8. Bournez, O., Garnier, F.: Proving Positive Almost-Sure Termination. In: Proc. of RTA 2005. LNCS, vol. 3467, pp. 323-337. Springer (2005). https://doi.org/10.1142/S0129054112400588

9. Bravyi, S., Kitaev, A.: Universal quantum computation with ideal clifford gates and noisy ancillas. Physical Review A **71**(2), 022316 (2005). https://doi.org/10.1103/PhysRevA.71.022316

10. Chen, Y.F., Chung, K.M., Lengál, O., Lin, J.A., Tsai, W.L., Yen, D.D.: An automata-based framework for verification and bug hunting in quantum circuits. Proceedings of the ACM on Programming Languages **7**(PLDI), 1218-1243 (2023). https://doi.org/10.1145/3591270

11. Cohn, P.M.: Further algebra and applications. Springer Science & Business Media (2002)

12. Dijkstra, E.W.: A discipline of programming. Prentice-Hall Englewood Cliffs (1976)

13. Endrullis, J., Geuvers, H., Zantema, H.: Degrees of undecidability in term rewriting. In: Grädel, E., Kahle, R. (eds.) Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5771, pp. 255-270. Springer (2009). https://doi.org/10.1007/978-3-642-04027-6_20, https://doi.org/10.1007/978-3-642-04027-6_20

14. Flemming Nielson, Hanne Riis Nielson, C.H.: Principles of Program Analysis. Springer, 2nd edn. (2005)

15. Fu, P., Kishida, K., Ross, N.J., Selinger, P.: Proto-quipper with dynamic lifting. POPL **7**, 309-334 (2023)
16. Gosset, D., Kliuchnikov, V., Mosca, M., Russo, V.: An algorithm for the t-count. Quantum Information & Computation 14(15-16), 1261-1276 (2014). https://doi.org/10.26421/QIC14.15-16-1, https://doi.org/10.26421/QIC14.15-16-1

17. Gretz, F., Katoen, J.P., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Performance Evaluation 73, 110-132 (2014). https://doi.org/10.1016/j.peva.2013.11.004

18. Halava, V., Harju, T., Hirvensalo, M., Karhumäki, J.: Skolem's problem - on the border between decidability and undecidability. Tech. Rep. 683, Turku Center for Computer Science (2005), http://oldtucs.abo.fi/publications/view/?pub_id=tHaHaHiKa05a

19. Handelman, D.: Representing Polynomials by Positive Linear Functions on Compact Convex Polyhedra. PJM 132(1), 35-62 (1988). https://doi.org/http://dx.doi.org/10.2140/pjm.1988.132.35

20. Harrow, A.W., Hassidim, A., Lloyd, S.: Quantum algorithm for linear systems of equations. Physical Review Letters 103, 150502 (2009). https://doi.org/10.1103/PhysRevLett.103.150502, https://link.aps.org/doi/10.1103/PhysRevLett.103.150502

21. Heintz, J., Roy, M.F., Solernó, P.: Sur la complexité du principe de tarski-seidenberg. Bulletin de la Société mathématique de France 118(1), 101-126 (1990)

22. Hillmich, S., Zulehner, A., Kueng, Richardand Markov, I.L., Wille, R.: Approximating decision diagrams for quantum circuit simulation. ACM Trans. Quantum Comput. 3(4), 1-21 (2022)

23. Jia, X., Kornell, A., Lindenhovius, B., Mislove, M.W., Zamdzhiev, V.: Semantics for variational quantum programming. Proc. ACM Program. Lang. 6(POPL), 1-31 (2022). https://doi.org/10.1145/3498687, https://doi.org/10.1145/3498687

24. Kaminski, B.L., Katoen, J.P.: On the hardness of almost-sure termination. In: MFCS 2015, Part I. pp. 307-318. LNCS, Springer (2015). https://doi.org/10.1007/978-3-662-48057-1_24

25. Kaminski, B.L., Katoen, J.P.: A weakest pre-expectation semantics for mixed-sign expectations. In: LICS 2017. pp. 1-12. IEEE (2017). https://doi.org/10.1109/LICS.2017.8005153

26. Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: ESOP 2016. LNCS, vol. 9632, pp. 364-389. Springer (2016). https://doi.org/10.1007/978-3-662-49498-1_15

27. Kozen, D.: A probabilistic PDL. Journal of Computer and System Sciences 30(2), 162-178 (1985)

28. Leutgeb, L., Moser, G., Zuleger, F.: Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In: Proc. of 34th CAV. LNCS, vol. 13372, pp. 70-91 (2022). https://doi.org/10.1007/978-3-031-13188-2_4

29. Liu, J., Zhou, L., Barthe, G., Ying, M.: Quantum weakest preconditions for reasoning about expected runtimes of quantum programs (2022)

30. Malherbe, O., Díaz-Caro, A.: Quantum control in the unitary sphere: Lambda-s1 and its categorical model. Logical Methods in Computer Science 18(3) (2022)

31. McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Springer Science & Business Media (2005)

32. Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. ACM SIGPLAN Notices 53(4), 496-512 (2018). https://doi.org/10.1145/3296979.3192394

33. Odifreddi, P.: Classical recursion theory: The theory of functions and sets of natural numbers. Elsevier (1992)
34. Olmedo, F., Díaz-Caro, A.: Runtime analysis of quantum programs: A formal approach. In: PLanQC 2020 (2020)

35. Perdrix, S.: Quantum entanglement analysis based on abstract interpretation. In: SAS. pp. 270–282. LNCS (2008). https://doi.org/10.1007/978-3-540-69166-2_18, https://doi.org/10.1007%2F978-3-540-69166-2_18

36. Schnabl, A., Simonsen, J.G.: The exact hardness of deciding derivational and runtime complexity. In: Proc. 20th CSL. LIPIcs, vol. 12, pp. 481–495 (2011). https://doi.org/10.4230/LIPIcs.CSL.2011.481

37. Schrijver, A.: Theory of linear and integer programming. Wiley (1999)

38. Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527–586 (2004). https://doi.org/10.1017/S0960129504004256, https://doi.org/10.1017/S0960129504004256

39. Sharir, M., Pnueli, A., Hart, S.: Verification of probabilistic programs. SIAM Journal on Computing 13(2), 292–314 (1984)

40. Shor, P.W.: Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer. SIAM Review 41(2), 303–332 (1999). https://doi.org/10.1137/S0036144598347011

41. Weihrauch, K.: Computable analysis: an introduction. Springer Science & Business Media (2012)

42. Wille, R., Van Meter, R., Naveh, Y.: IBM's Qiskit Tool Chain: Working with and Developing for Real Quantum Computers. In: 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE). pp. 1234–1240 (2019). https://doi.org/10.23919/DATE.2019.8715261

43. Winskel, G.: The formal semantics of programming languages - an introduction. Foundation of computing series, MIT Press (1993)
## A Further PARS Preliminaries

Let $\rightarrow$ be a PARS. If $\delta \stackrel{c}{\rightarrow}^{n} \epsilon$ then $\delta$ reduces to $\epsilon$ in $n$ steps, with an expected runtime of $c$. Notice that since $\rightarrow$ is deterministic, so is $\stackrel{c}{\rightarrow}^{n}$ in the sense that $\delta \stackrel{c_1}{\rightarrow}^{n} \epsilon_1$ and $\delta \stackrel{c_2}{\rightarrow}^{n} \epsilon_2$ implies $c_1 = c_2$ and $\epsilon_1 = \epsilon_2$. It thus justifies to define $edl_{\rightarrow}^{=n}(a) \triangleq c$, when $\{1 : a\} \stackrel{c}{\rightarrow}^{n} \delta$. Likewise, we denote by $\text{term}_{\rightarrow}^{\leq n}(a) \triangleq \{\delta(b) : b | b \not\rightarrow \land \exists c \in \mathbb{R}^{+}, \{1 : a\} \stackrel{c}{\rightarrow}^{n} \delta\}$ the distribution of terminal objects reachable within up-to $n$ steps.

**Definition 9 (Terminal distribution).** For a PARS $\rightarrow$ over A and $a \in A$, the terminal distribution of $a \in A$ is given by

$$ \text{term}_{\rightarrow}(a) \triangleq \sup_{n \in \mathbb{N}} \text{term}_{\rightarrow}^{\leq n}(a). $$

Here, the supremum should be understood wrt. the pointwise ordering on distributions. This supremum always exists, the probability of reaching a certain terminal object only increases during reductions, i.e., $\text{term}_{\rightarrow}^{\leq n}(a)$ is monotonic in $n$. The (sub)distribution $\text{term}_{\rightarrow}(a)$ yields for each terminal object $b \not\rightarrow$ the probability that $a$ reduces to $b$ in a finite number of steps. Specifically, the total weight $|\text{term}_{\rightarrow}(a)|$ corresponds to the probability that $a$ is terminating.

**Definition 10 (Expected derivation length).** The expected derivation length of a PARS $\rightarrow$ over A is given by the function:

$$ \begin{aligned} \text{edl}_{\rightarrow} & : A \rightarrow \mathbb{R}^{+\infty} \\ \text{edl}_{\rightarrow} & \triangleq \lambda a. \sup_{n \in \mathbb{N}} (\text{edl}_{\rightarrow}^{=n} a). \end{aligned} $$

We define the following approximations of $wp_{\rightarrow}$:

$$ \text{wp}_{\rightarrow}^{\leq n}(f) \triangleq \lambda a. \mathbb{E}_{\text{term}_{\rightarrow}^{\leq n}(a)}(f) \quad \text{wp}_{\rightarrow}^{-n}(f)(\sigma) \triangleq \begin{cases} \text{wp}_{\rightarrow}^{\leq n}(f)(\sigma) & \text{if } n = 0, \\ \text{wp}_{\rightarrow}^{\leq n} f \sigma - \text{wp}_{\rightarrow}^{\leq n-1}(f)(\sigma) & \text{if } n > 0. \end{cases} $$

By definition, it holds that

$$ \text{wp}_{\rightarrow}(f)(\sigma) = \sup_{n} \text{wp}_{\rightarrow}^{\leq n}(f)(\sigma) = \sup_{n} \sum_{i=0}^{n} \text{wp}_{\rightarrow}^{=i}(f)(\sigma) = \sum_{i=0}^{\infty} \text{wp}_{\rightarrow}^{=i}(f)(\sigma). $$

Notice also that the weight of a terminal distribution—thus the termination probability—can be expressed as a particular weakest pre-expectation.

Let $\underline{1} \triangleq \lambda a.1$.

**Proposition 2.** $|\text{term}_{\rightarrow} a| = \text{wp}_{\rightarrow} \underline{1} a$.

*Proof.* As $| \cdot |$ is an increasing and continuous function, the following holds:

$$ \begin{aligned} |\text{term}_{\rightarrow}(a)| &= |\sup_{n \in \mathbb{N}} \text{term}_{\rightarrow}^{\leq n}(a)| = \sup_{n \in \mathbb{N}} |\text{term}_{\rightarrow}^{\leq n}(a)| = \sup_{n \in \mathbb{N}} \mathbb{E}_{\text{term}_{\rightarrow}^{\leq n}(a)}(\underline{1}) = \sup_{n \in \mathbb{N}} \text{wp}_{\rightarrow}^{\leq n} \underline{1} a \\ &= \text{wp}_{\rightarrow} \underline{1} a. \end{aligned} $$
# B Proofs from Section 3

**Lemma 2.** The set $D_{\mathbb{A}^+}^{\text{fin}}(\text{Conf}_{\text{CT}})$ is stable under reduction, more precisely, if $\delta \in D_{\mathbb{A}^+}^{\text{fin}}(\text{Conf}_{\text{CT}})$ and $\delta \stackrel{c}{\Rightarrow}_{\mathbb{Q}} \varepsilon$, then $\varepsilon \in D_{\mathbb{A}^+}^{\text{fin}}(\text{Conf}_{\text{CT}})$ and $c \in \mathbb{A}^+$.

*Proof.* Let us first observe that if $\mu \to_{\mathbb{Q}} \delta$ then $\delta \in D_{\mathbb{A}^+}^{\text{fin}}(\text{Conf}_{\text{CT}})$. By looking at the rules of Figure 4, it is immediate that right-hand sides $\delta$ are finitely supported. In addition, quantum states are only updated by rules (Op) and (Meas). In both cases, the resulting density operator is in $\mathcal{D}(\tilde{H}_Q)$, as $\forall i, \forall k, M_{k,i} \in \mathcal{D}(\tilde{H}_Q)$ and algebraic numbers are closed under product and finite sum. Following the same reasoning, in each rule of Figure 4, the probabilities are also algebraic numbers in $\mathbb{A}^+$. Conclusively $\delta \in D_{\mathbb{A}^+}^{\text{fin}}(\text{Conf}_{\text{CT}})$.

Now consider a step $\delta \stackrel{c}{\Rightarrow}_{\mathbb{Q}} \varepsilon$, for $\delta \in D_{\mathbb{A}^+}^{\text{fin}}(\text{Conf}_{\text{CT}})$. Then, since $\cdot \stackrel{c}{\Rightarrow}_{\mathbb{Q}} \cdot$ is deterministic, wlog $\delta$ is of the form $\{p_i : \mu_i\}_{0 \le i \le n}$ and $\varepsilon = \sum_{i=0}^n p_i \cdot \varepsilon_i$ for $\{1 : \mu_i\} \stackrel{c}{\Rightarrow}_{\mathbb{Q}} \varepsilon_i$, i.e., $\varepsilon_i$ is either $\{1 : \mu_i\}$ (when $\mu_i$ is terminal) or $\mu_i \to_{\mathbb{Q}} \varepsilon_i$. In any case, by the previous observation the scaled distributions $p_i \cdot \varepsilon_i \in D_{\mathbb{A}^+}^{\text{fin}}(\text{Conf}_{\text{CT}})$, and so is their finite summation $\varepsilon$.

In the remainder, we establish the completeness results, summarized in Table 1, that is we prove Theorem 1. We start with some preliminaries.

## B.1 Preliminaries

Let $\text{Stmt}_K$ be the subset of $\text{Stmt}$ that only contains classical statements (i.e., statements that do not contain any quantum feature). This fragment of our language is clearly still a Turing-complete programming language. It obviously holds that $\text{Stmt}_K \subsetneq \text{Stmt}_{\text{CT}}$. For the sake of the hardness proofs, we briefly introduce the following well-known problems and the corresponding class for which they are complete (see [33]):

(Halting Problem) $\mathcal{H} : \Sigma_1^0$-complete
(stm, s) $\in \mathcal{H} \subseteq \text{Stmt}_K \times \text{Store} \iff \exists s' \in \text{Store}, \exists n \in \mathbb{N}, (\text{stm}, s, \cdot) \stackrel{n}{\Rightarrow}_{\mathbb{Q}} (\downarrow, s', \cdot)$,
(Universal Halting Problem) $\mathcal{U}\mathcal{H} : \Pi_2^0$-complete
stm $\in \mathcal{U}\mathcal{H} \subseteq \text{Stmt}_K \iff \forall s \in \text{Store}, (\text{stm}, s) \in \mathcal{H}$,
(Cofiniteness Problem) $\mathcal{COF} : \Sigma_3^0$-complete
stm $\in \mathcal{COF} \subseteq \text{Stmt}_K \iff \text{co-}\{s \mid (\text{stm}, s) \in \mathcal{H}\}$ is cofinite.

It is well-known that if a set $A$ is c-complete then its complement, noted co-$A$, is (co-c)-complete and that if $A$ is c-complete and $A \leq_m B$ then $B$ is c-hard. Recall that a set is cofinite, if its complement is finite. In the above definition, we use a $\cdot$ for the quantities that are not relevant. E.g., the quantum state is useless for the halting problem with respect to classical statements.
The following syntactic sugar will be used throughout the paper to represent some statements in `StmtCT`:

$$ 
\begin{align*}
q^Q &= |+\rangle &\triangleq& q &= |0\rangle; q^* &= H, \\
x^B &= \text{Cointoss}() &\triangleq& q' &= |+\rangle; x &= \text{meas } q', \\
x^N &= \text{GEO}() &\triangleq& x' &= \text{tt}; x &= -1; \text{ while } x' \text{ do } \{x' &= \text{Cointoss}(); x &= x+1\},
\end{align*}
$$

for some fresh variables $q'$ and $x'$ of type $Q$ and $B$, respectively. The two first notations initialize a qubit to the basis vector $|0\rangle$ of the standard basis and to the basis vector $|+\rangle$ of the orthogonal basis, respectively. The penultimate notation simulate a fair coin toss by performing a measurement on $|+\rangle$. The last notation amounts to sampling an integer from a geometric distribution, assigning probability $\frac{1}{2^{n+1}}$ to each integer $n \in \mathbb{N}$.

Given a classical statement $P \in \text{Stmt}_K$ and a store $s$, we will also define $P(s)$ to be a statement in `StmtK` simulating $P$ on variables initialized by values of $s$. Given a computable enumeration of stores $(s_i)_{i \in \mathbb{N}}$ and a variable $n^N$, $P(s_n)$ will be used as syntactic sugar for the statement which, on input store $r$, first initializes the classical state to $s_{r(n)}$, and then simulates $P$. The existence of such a program is implied by the Turing-completeness of `StmtK`.

## Termination Problems

**Theorem 5.** AST is $\Pi_2^0$-complete and the corresponding universal problem UAST is $\Pi_2^0$-complete.

*Proof.* - CASE AST. Observe that

$$ 
\begin{align*}
(\text{stm}, \sigma) \in \text{AST} &\iff |\text{term}_{\text{stm}}(\sigma)| = 1 \\
&\iff \sup_{n \in \mathbb{N}} |\text{term}_{\text{stm}}^{\le n}(\sigma)| = 1 \\
&\iff \forall \epsilon \in \mathbb{R}^+, \exists n, |\text{term}_{\text{stm}}^{\le n}(\sigma)| \ge 1 - \epsilon \\
&\iff \forall \epsilon \in \mathbb{A}^+, \exists n, |\text{term}_{\text{stm}}^{\le n}(\sigma)| \ge 1 - \epsilon
\end{align*}
$$

Since $|\text{term}_{\text{stm}}^{\le n}(\sigma)| \in \mathbb{A}^+$ is computable, $\Pi_2^0$-membership of AST follows. Concerning $\Pi_2^0$-hardness, we directly obtain $\mathcal{U}\mathcal{H} \le_m \text{AST}$, via the reduction

$$ 
\begin{align*}
r & : \text{Stmt}_K \to \text{Conf}_{\text{CT}} \\
r(P) & \triangleq ((i = \text{GEO}(); P(s_i)), \sigma^*),
\end{align*}
$$

for fresh variable $i$ of type $\mathcal{N}$ and arbitrary but fixed initial state $\sigma^*$. Observe how this program is almost surely terminating, precisely if $P(s_i)$ is terminating for all $i \in \mathbb{N}$, i.e., if $P \in \mathcal{U}\mathcal{H}$.

- CASE UAST. Since $\text{stm} \in \text{UAST} \iff \forall \sigma \in \text{St}_{\text{CT}}, (\text{stm}, \sigma) \in \text{AST}$, by the first part of the theorem, UA$\text{ST} \in \Pi_2^0$. $\Pi_2^0$-hardness is proven identically to that of AST, via the reduction $r(P) \triangleq (i = \text{GEO}(); P(s_i))$ for some fresh variable $i$ of type $\mathcal{N}$, and showing that $\mathcal{U}\mathcal{H} \le_m \text{UAST}$.
**Theorem 6.** PAST is $\Sigma_2^0$-complete and the corresponding universal problem UPAST is $\Pi_3^0$-complete. □

*Proof.* - CASE PAST. Membership is established as follows:

$$ (\mathbf{stm}, \sigma) \in \mathbf{PAST} \iff \begin{aligned} \mathrm{edl}_{\mathbf{stm}}(\sigma) &< \infty \\ \sup_{n \in \mathbb{N}} \mathrm{edl}_{\mathbf{stm}}^{\le n}(\sigma) &< \infty \\ \exists c, \forall n, \mathrm{edl}_{\mathbf{stm}}^{= n}(\sigma) &< c. \end{aligned} $$

Since $\mathrm{edl}_{\mathbf{stm}}^{=n}(\sigma) < c$ is computable, $\Sigma_2^0$-membership of PAST follows. Hardness can be shown using the reduction of [24, Theorem 8] and the statement $\mathbf{x}^B = \mathbf{Cointoss}()$ to simulate a fair coin tossing.

- CASE UPAST. Since $\mathbf{stm} \in \mathbf{UPAST} \iff \forall \sigma \in \mathrm{St}_{\mathrm{CT}}, (\mathbf{stm}, \sigma) \in \mathbf{PAST}$, by Theorem 6, $\mathbf{UPAST} \in \Pi_3^0$. Hardness can be shown using the reduction of [24, Theorem 10] and the statement $\mathbf{x}^B = \mathbf{Cointoss}()$ to simulate a fair coin tossing.

## Testing problems

To simplify notations, we extend the notion of approximated weakest pre-expectation (see Section A transformers from PARSs to quantum programs:

$$ \mathbf{qwp}_{\mathbf{stm}}^{\le n}(f)(\sigma) \triangleq \mathbf{wp}_{\mathbf{x}_{\sigma}}^{\le n}(f_{\mathrm{st}})(\mathbf{stm}, \sigma) \quad \mathbf{qwp}_{\mathbf{stm}}^{= n}(f)(\sigma) \triangleq \mathbf{wp}_{\mathbf{x}_{\sigma}}^{= n}(f_{\mathrm{st}})(\mathbf{stm}, \sigma). $$

In a similar vein, we set $\mathrm{term}_{\mathbf{x}_{\sigma}}(\mathbf{stm}, \sigma) \triangleq \mathrm{term}_{\mathbf{stm}}(\sigma)$.

**Theorem 7.** $\mathrm{TEST}_>^0$ is $\Sigma_1^0$-complete and $\mathrm{TEST}_\le^0$ is $\Pi_1^0$-complete. □

*Proof.* - CASE $\mathrm{TEST}_>^0$. As $\mathbf{qwp}_{\mathbf{stm}}^{\le n}(f)$ is monotonically increasing, the following equivalences hold:

$$ (\mathbf{stm}, \sigma, f, a) \in \mathrm{TEST}_> \iff \begin{aligned} \mathbf{qwp}_{\mathbf{stm}}(f)(\sigma) &> a \\ \sup_{n \in \mathbb{N}} \mathbf{qwp}_{\mathbf{stm}}^{\le n}(f)(\sigma) &> a \\ \exists k \in \mathbb{N}, \exists \delta > 0, \mathbf{qwp}_{\mathbf{stm}}^{\le k}(f)(\sigma) &\ge a + \delta \end{aligned} $$

Consequently, $\mathrm{TEST}_>^0 \in \Sigma_1^0$. For $\Sigma_1^0$-hardness, we have $\mathcal{H} \le_m \mathrm{TEST}_>^0$ via the reduction

$$ \begin{aligned} r : \mathrm{Stmt}_K \times \mathrm{Store} \to \mathrm{Conf}_{\mathrm{CT}} \times \mathrm{E}_{\mathrm{CT}} \times \mathbb{A}^+ \\ r(\mathrm{P}, s) \triangleq (\mathrm{stmt}_P, s, |+\rangle\langle+|, \underline{1}, \overline{1/2}), \end{aligned} $$

where $\mathrm{stmt}_P \triangleq (x = \mathrm{meas} q; \text{ if } x \text{ then } P \text{ else } \mathrm{skip})$, for some fresh variable $x$ of type $\mathcal{B}$. Note that

$$ \mathbf{qwp}_{\mathrm{stmt}_P}(\underline{1})(s, |+\rangle\langle+|) = \frac{\mathbf{qwp}_P(\underline{1})(s[x := \underline{1}], |1\rangle\langle1|)}{2} + \frac{1}{2} = \frac{\mathbf{qwp}_P(\underline{1})(s, |+\rangle\langle+|)}{2} + \frac{1}{2}. $$
After performing the measure, the program executes P with probability $1/2$. Note that $|1\rangle\langle 1|$ is the quantum state obtained from $|+\rangle\langle +|$ just before executing P. The second equality above holds as $P \in \text{Stmt}_K$ and $x$ is fresh with respect to P. Finally, $qwp_P(s, |+\rangle\langle +|)(1) = 1$ iff P is terminating on $s$, as programs in $\text{Stmt}_K$ do not depend on the quantum state. Thus, it holds that:

$$ (P, s) \in \mathcal{H} \iff qwp_{\text{stmt}}(1)(s, |+\rangle\langle +|) > 1/2 \iff r(P, s) \in \text{TEST}_{>}. $$

- **CASE TEST<.** Since TEST< = co-TEST>, the claim follows by the first part of the theorem.

**Theorem 8.** TEST< is $\Sigma_2^0$-complete and TEST$\ge$ is $\Pi_2^0$-complete.

*Proof.* - **CASE TEST<.**

As $qwp_{\text{stmt}}^{\le n}(f)$ is monotonically increasing, the following equivalences hold:

$$ \begin{align*} (\text{stmt}, \sigma, f, a) \in \text{TEST}_{<} &\iff qwp_{\text{stmt}}(f)(\sigma) < a \\ &\iff \sup_{n \in \mathbb{N}} qwp_{\text{stmt}}^{\le n}(f)(\sigma) < a \\ &\iff \exists b \in \mathbb{A}^{+} - \{0\}, \forall k \in \mathbb{N}, < qwp_{\text{stmt}}^{\le k}(f)(\sigma) < a - b \end{align*} $$

Consequently, $\text{TEST}_{<} \in \Sigma_2^0$. To prove completeness, we show that co-$\mathcal{U}\mathcal{H} \le_m \text{TEST}_{<}$, via the reduction

$$ \begin{align*} r: \text{Stmt}_K \to \text{Conf}_{\text{CT}} \times \text{E}_{\text{CT}} \times \mathbb{A}^+ \\ r(P) \triangleq (\text{stmt}, \sigma^*, f_P, 1), \end{align*} $$

where $\text{stmt} \triangleq (i = \text{GEO}(); k = \text{GEO}())$, $\sigma^*$ is an arbitrary but fixed initial state and

$$ f_P(s, \rho) \triangleq qwp_P^{=s(k)}(1)(\sigma_{s(i)}) \cdot 2^{s(k)+1}, $$

for $(\sigma_i)_{i \in \mathbb{N}}$ a sequence of states whose stores provide an enumeration of classical states in Store for P. Being computed as a finite sum, $f_P$ is a computable expectation in $\text{E}_{\text{CT}}$. Notice that after execution, the values held by $i$ and $k$ are independently distributed according to a geometric distribution, conclusively

$$ qwp_{\text{stmt}}(f_P)(\sigma^*) = \sum_{i=0}^{\infty} \frac{1}{2^{i+1}} \sum_{k=0}^{\infty} \frac{1}{2^{k+1}} qwp_P^{=k}(1)(\sigma_i) \cdot 2^{k+1} = \sum_{i=0}^{\infty} \sum_{k=0}^{\infty} \frac{qwp_P^{=k}(1)(\sigma_i)}{2^{i+1}} $$

Notice that $qwp_P^{=k}(1)(\sigma_i) = 1$ iff P terminates with precisely $k$ steps on input $\sigma_i$, and 0 otherwise. Thus, if P is terminating on $\sigma_i$, then $\sum_{k=0}^{\infty} \frac{qwp_P^{=k}(1)(\sigma_i)}{2^{i+1}} = \frac{1}{2^{i+1}}$, and 0 otherwise. Using the identity $\sum_{i=0}^{\infty} \frac{1}{2^{i+1}} = 1$ from this it is not difficult to establish that

$$ P \notin \mathcal{U}\mathcal{H} \iff qwp_{\text{stmt}}(f_P)(\sigma^*) < 1 \iff r(P) \in \text{TEST}_{<}. $$

- **CASE TEST$\ge$.** Since TEST$\ge$ = co-TEST<, the claim follows by the first part of the theorem.
**Theorem 9.** TEST_ is $\Pi_2^0$-complete.

*Proof.* Membership follows from the second parts of Theorems 7 and 8, respectively, since TEST_ = TEST_≤ ∩ TEST_≥. By definition (stm, σ) ∈ AST iff |term_stm(σ)| = 1. By Proposition 2, it holds that |term_stm(σ)| = qwp_stm(1)(σ). Consequently, (stm, σ) ∈ AST iff qwp_stm(1)(σ) = 1 and the reduction r(stm, σ) ≜ (stm, σ, 1, 1) shows AST ≤_m TEST_, hence TEST_ ∈ $\Pi_2^0$ by Theorem 5.

**Theorem 10.** UTEST> is $\Pi_2^0$-complete and UTEST≥ is $\Pi_2^0$-complete.

*Proof.* - CASE UTEST>.

That UTEST_ ∈ $\Pi_2^0$ follows directly from Theorem 7. Following the pattern of the proof of Theorem 7, for hardness, we show $\mathcal{U}\mathcal{H} \le_m UTEST>$ via the reduction

$$r : \text{Stmt}_K \to \text{Stmt}_{\text{CT}} \times \mathbb{E}_{\text{CT}} \times \mathbb{E}_{\text{CT}} \\ r(\mathbb{P}) \triangleq (\text{stmt}_p, \underline{1}, \underline{1/2}),$$

where stmt_p ≜ (q = |+⟩; x = meas q; if x then P else skip), for some fresh variables x and q of type B and Q, respectively. Note that

$$qwp_{\text{stmt}}(1)(s, \rho) = \frac{qwp_{\text{P}}(1)(s[x := 1], \rho')}{2} + \frac{1}{2} = \frac{qwp_{\text{P}}(1)(s, \rho)}{2} + \frac{1}{2}$$

where ρ' is the quantum state obtained from ρ just before executing P, as after performing the measure, the program executes P with probability 1/2. The second equality above holds as P ∈ Stmt_K and x is fresh with respect to P. It holds that qwp_P(s, ρ)(1) = 1 iff P is terminating on s, as programs in Stmt_K do not depend on the quantum state. Thus

$$P \in \mathcal{U}\mathcal{H} \iff \forall \sigma \in \text{St}_{\text{CT}}, qwp_{\text{stmt}}(1)(\sigma) > 1/2 \iff r(\mathbb{P}) \in \text{UTEST}_{>}$$

- CASE UTEST≥. We have

$$(stm, f, g) \in \text{UTEST}_{\ge} \iff \forall \sigma \in \text{St}_{\text{CT}}, (stm, \sigma, f, g(\sigma)) \in \text{TEST}_{\ge}$$

and conclusively UTEST≥ is in $\Pi_2^0$ by Corollary 8. Exploiting that stmt ∈ AST ⇐⇒ ∀σ ∈ St<sub>CT</sub>, qwp<sub>stmt</sub>(1)(σ) = 1, the reduction r defined by

$$r : \text{Stmt}_K \to \text{Stmt}_{\text{CT}} \times \mathbb{E}_{\text{CT}} \times \mathbb{E}_{\text{CT}} \\ r(\mathbb{P}) \triangleq (\mathbb{P}, \underline{1}, \underline{1}),$$

proves that UAST ≤_m UTEST≥ and, conclusively, UTEST≥ is $\Pi_2^0$-hard, by Theorem 5.

**Theorem 11.** UTEST_ is $\Pi_2^0$-complete.
*Proof.* Membership is a direct consequence of Theorem 9. Hardness is provable by showing $\mathcal{U}\mathcal{H} \le_m \text{UTEST}_=$ using the reduction

$$r : \text{Stmt}_K \to \text{Stmt}_{\text{CT}} \times \text{E}_{\text{CT}} \times \text{E}_{\text{CT}}$$

$$r(\mathbf{P}) \triangleq (\text{stm}, f_{\mathbf{P}}, \underline{1}),$$

where `stm` and `f_P` are precisely taken as in the proof of Theorem 8. As reasoned there, independent of the initial state $\sigma^*$,

$$\text{qwp}_{\text{stm}}(f_{\mathbf{P}})(\sigma^*) = \sum_{i=0}^{\infty} \sum_{k=0}^{\infty} \frac{\text{qwp}_{\mathbf{P}}^{=k}(\underline{1})(\sigma_i)}{2^{i+1}}$$

for $(\sigma_i)_{i \in \mathbb{N}}$ a sequence of states whose stores provide an enumeration of classical states in Store for P. Since $\sum_{k=0}^{\infty} \frac{\text{qwp}_{\mathbf{P}}^{=k}(\underline{1})(\sigma_i)}{2^{i+1}} = \frac{1}{2^{i+1}}$ iff P halts on $\sigma_i$ and 0 otherwise, by the identity $\sum_{i=0}^{\infty} \frac{1}{2^{i+1}} = 1$ it follows that

$$\mathbf{P} \in \mathcal{U}\mathcal{H} \iff \forall \sigma \in \text{St}_{\text{CT}}, \text{qwp}_{\text{stm}}(f_{\mathbf{P}})(\sigma^*) = 1 \iff r(\mathbf{P}) \in \text{UTEST}_=$$

**Theorem 12.** $\text{UTEST}_\le$ is $\Pi_1^0$-complete.

*Proof.* We have

$$(\text{stm}, f, g) \in \text{UTEST}_\le \iff \forall \sigma \in \text{St}_{\text{CT}}, (\text{stm}, \sigma, f, g(\sigma)) \in \text{TEST}_\le$$

and conclusively $\text{UTEST}_\le$ is in $\Pi_1^0$ by the second part of Theorem 7. To conclude, it is sufficient to realize that $\text{co-}\mathcal{H} \le_m \text{UTEST}_\ge$ via the reduction

$$r : \text{Stmt}_K \times \text{Store} \to \text{Stmt}_{\text{CT}} \times \text{E}_{\text{CT}} \times \text{E}_{\text{CT}}$$

$$r(\mathbf{P}, s) \triangleq (\text{stm}_{\mathbf{P}}^s, \underline{1}, \underline{1/2}),$$

with $\text{stm}_{\mathbf{P},s} \triangleq (\mathbf{x} = \text{Coinloss}(); \text{if } \mathbf{x} \text{ then } \mathbf{P}(s) \text{ else skip})$, for some fresh variable $\mathbf{x}$ of type $\mathcal{B}$.

By definition, $\text{qwp}_{\text{stm}_{\mathbf{P},s}}(\underline{1})(\sigma) = \underline{1/2}$ if P diverges on input store $s$ (i.e., if $(\mathbf{P}, s) \in \text{co-}\mathcal{H}$) for any input state $\sigma$. On the other hand, if P terminates on $s$ then $\text{qwp}_{\text{stm}_{\mathbf{P},s}}(\underline{1})(\sigma) = 1$. Conclusively,

$$(\mathbf{P}, s) \in \text{co-}\mathcal{H} \iff \forall \sigma \in \text{St}_{\text{CT}}, \text{qwp}_{\text{stm}_{\mathbf{P},s}}(\underline{1})(\sigma) \le \underline{1/2} \iff r(\mathbf{P}, s) \in \text{UTEST}_\le$$

**Theorem 13.** $\text{UTEST}_<$ is $\Pi_3^0$-complete.

*Proof.* From Theorem 8, it follows immediately that $\text{UTEST}_< \in \Pi_3^0$. For a given expectation $f$, let $f+2$ denote the function defined by $(f+1)(\sigma) \triangleq f(\sigma)+2$, for each state $\sigma \in \text{St}_{\text{CT}}$. To show that it is $\Pi_3^0$-hard, we prove $\text{co-}\mathcal{COF} \le_m \text{UTEST}_<$ via the reduction

$$r : \text{Stmt}_K \to \text{Stmt}_{\text{CT}} \times \text{E}_{\text{CT}} \times \text{E}_{\text{CT}}$$

$$r(\mathbf{P}) \triangleq (\text{stm}_{\mathbf{P}}, f_{\downarrow}, f_{\downarrow} + 2),$$
where $\mathit{stmp} \triangleq (x = tt; i = 0; \mathit{while} x \mathit{do} \{x = \mathit{Cointoss}(); i = i + 1; P(s_i)\})$, for some fresh variables $i^N$ and $x^B$, and where $f_\downarrow(s, \rho) \triangleq s(i)$ is the expectation outputting value of $i$ obtained after program execution. The program $\mathit{stmp}$ executes $P$ with increasing inputs; gradually losing interest since the loop aborts with probability $1/2$ after each iteration. Note that the loop body gets stuck if $P(s_i)$ is non-terminating.

Recall $P \notin \mathcal{COF}$, if $P$ is a program in $\mathit{Stmt}_K$ that is non-terminating on infinitely many inputs. We claim

$$P \notin \mathcal{COF} \iff \forall \sigma \in \mathit{St}_{\mathit{CT}}, \mathit{qwp}_{\mathit{stmp}}(f_{\downarrow})(\sigma) < f_{\downarrow}(\sigma) + 2 \iff r(P) \in \mathit{UTEST}_{<}$$

- **CASE P \in COF.** In the considered case, there are at most finitely many inputs on which $P$ is non-terminating. In particular, this means that $P$ is terminating on all $i \ge \ell$ for some $\ell \in \mathbb{N}$. Consider an initial store $\sigma = (s, \rho)$ such that $i \triangleq s(i) \ge \ell$. Thus

$$\mathit{qwp}_{\mathit{stmp}}(f_{\downarrow})(\sigma) = \frac{1}{2}(i+1) + \frac{1}{4}(i+2) + \frac{1}{8}(i+3) + \dots = \sum_{k=1}^{\infty} \frac{i+k}{2^k} = i + \sum_{k=1}^{\infty} \frac{k}{2^k} = i + 2.$$

Conclusively, $(\mathit{stmp}, f_\downarrow, f_\downarrow + 2) \notin \mathit{UTEST}_{<}$.

- **CASE P \notin COF.** Let $\sigma = (s, \rho)$ be arbitrary, and define $i \triangleq s(i)$. Since in the considered case, there are infinitely many inputs on which $P$ is non-terminating, there exists in particular (a minimal) $n \ge 0$ for which $P$ is non-terminating on $s_{i+n}$, i.e., the $n$-th iteration of the loops gets stuck. Thus

$$\mathit{qwp}_{\mathit{stmp}}(f_{\downarrow})(\sigma) = \sum_{i=1}^{n} \frac{i+k}{2^k} < i + 2 = f_{\downarrow}(\sigma) + 2$$

Conclusively, $(\mathit{stmp}, f_\downarrow, f_\downarrow + 2) \in \mathit{UTEST}_{<}$.

## Finiteness problems

**Theorem 14.** $\mathit{TEST}_{\neq \infty}$ is $\Sigma_2^0$-complete.

*Proof.* For membership, we have

$$(\mathit{stm}, \sigma, f) \in \mathit{TEST}_{\neq \infty} \iff \exists a \in \mathbb{A}^+, (\mathit{stm}, \sigma, f, a) \in \mathit{TEST}_{<}$$

and thus $\mathit{TEST}_{\neq \infty}$ is in $\Sigma_2^0$, by Theorem 8. For hardness, we prove $\mathit{co-UH} \le_m \mathit{TEST}_{\neq \infty}$ via the reduction

$$r : \mathit{Stmt}_K \times \mathit{Store} \to \mathit{Conf}_{\mathit{CT}} \times \mathit{E}_{\mathit{CT}} \times \mathbb{A}^+$$

$$r(P, s) = (\mathit{stmp}, \sigma^*, f),$$

where $\mathit{stmp}$ is exactly as in Theorem 13, $\sigma^*$ is an arbitrary but fixed initial state assigning the value 0 to the fixed variable $i$ of type $\mathcal{N}$, and where $f(s, \rho) \triangleq 2^{s(i)}$.
For correctness of the reduction, first assume $P \notin \text{co-}\mathcal{U}\mathcal{H}$, i.e., $P$ is not universally terminating. Then, reasoning as in Theorem 13,

$$ \text{qwp}_{\text{stmp}}(f)(\sigma^*) = \frac{1}{2} \cdot 2^1 + \frac{1}{4} \cdot 2^2 + \dots = \sum_{n=1}^{\infty} \frac{2^n}{2^n} = \sum_{n \in \mathbb{N}} 1 = \infty $$

and hence $r(P) \notin \text{TEST}_{\neq \infty}$. If, on the other hand, $P \in \text{co-}\mathcal{U}\mathcal{H}$, then $\text{qwp}_{\text{stmp}}(f)(\sigma^*) = \sum_{n=1}^{k} 1 = k$ where $k$ is the first index with $P$ diverging on $s_k$, hence $r(P) \in \text{TEST}_{\neq \infty}$.

**Theorem 15.** $\text{UTEST}_{\neq \infty}$ is $\Pi_3^0$-complete.

*Proof.* Membership follows by Theorem 14, since we have

$$ \text{stm} \in \text{UTEST}_{\neq \infty} \iff \forall \sigma \in \text{St}_{\text{CT}}, (\text{stm}, \sigma) \in \text{TEST}_{\neq \infty} $$

For hardness, we prove $\text{co-}\mathcal{COF} \leq_m \text{UTEST}_{\neq \infty}$ via the reduction $r$ defined by $r(P) \triangleq (\text{stmp}, f)$ where $\text{stmp}$ is exactly as in Theorem 13 but $f(s, P) = 2^{s(1)}$. The proof now proceeds identical to Lemma 13. If $P \notin \text{co-}\mathcal{COF}$ then $\text{qwp}_{\text{stmp}}(f)(s, \rho) = \sum_{i=1}^{\infty} \frac{2^{n+i}}{2^i} = \sum_{i=1}^{\infty} 2^n = \infty$ considering an initial store $(s, \rho)$ with $n = s(n)$ so that $P$ is terminating on all $(s_k)_{k \geq n}$. Hence $r(P) \notin \text{UTEST}_{\neq \infty}$. On the other hand, if $P \in \text{co-}\mathcal{COF}$ then reasoning identical to Theorem 13 $\text{qwp}_{\text{stmp}}(f)(\sigma)$ is a finitely indexed sum independent of the initial state $\sigma$, thus finite. Hence $r(P) \in \text{UTEST}_{\neq \infty}$.

# C Proof of Theorem 2

**Theorem 2 (Adequacy).** *The following holds:*

$$ \forall \text{stm} \in \text{Stmt}, \forall f : \text{St} \to \mathbb{R}^{+\infty}, \text{qwp}_{\text{stm}}(f) = \text{qet}[\text{stm}]{f}. $$

*Proof.* The adequacy Theorem is a direct consequence of [5, Corollary 4.8], based on the observations that $\text{qwp}_{\text{stm}}(f)$ corresponds to the notion of expected value $\text{evalue}_{\text{stm}}(f)(\sigma)$ of [5] and that $\text{qet}[\text{stm}]{f}$ corresponds to the expected value transformer $\text{qev}_S[\cdot] \{ \cdot \}$ of [5] for the particular Kegelspitze $S = (\mathbb{R}^{+\infty}, +_f)$, with $+_f$ being the forgetful addition.

# D Proof of Theorem 4

**Theorem 4.** For any degree $d \in \mathbb{N}$, $d \geq 1$, the problem $\text{QINFER}(\mathbb{A}^d[\text{St}_{\text{CT}}])$ is decidable in time $2^{2^{d\text{O}(n)}}$, where $n$ is the size of the considered program.

*Proof.* Suppose $\text{qinf}[\text{stm}]{X} = G$, producing side-constraints $C$. By definition, every constraint in $C$ is of the form

$$ \Gamma \vdash F \leq X_{\ell} $$
for some $F \in \mathbf{ETerm}$, $X_\ell \in \mathbf{EVar}$ and where $\Gamma$ is wlog. either a Boolean Expression $b \in \mathbf{BExp}$, or a probability constraint, i.e., of the form $p_{i,k}(\rho) = 0$ or a conjunction thereof. Consider the following, semantic preserving, rewrite rules:

$$ (H_1 +_p H_2)[\mathbf{y} := \mathbf{e}] \rightarrow H_1[\mathbf{y} := \mathbf{e}] +_p H_2[\mathbf{y} := \mathbf{e}] \quad H[\mathbf{\chi}][\mathbf{y} := \mathbf{e}] \rightarrow H[\mathbf{y} := \mathbf{e}][\mathbf{\chi}] \\ (H_1 +_p H_2)[\mathbf{\psi}] \rightarrow H_1[\mathbf{\psi}] +_{p \circ \psi} H_2[\mathbf{\psi}] \quad H[\mathbf{\chi}][\mathbf{\psi}] \rightarrow H[\mathbf{\chi} \circ \mathbf{\psi}] $$

where $\circ$ denotes function composition. In particular, for $\chi = \lambda\rho \cdot \frac{M\rho M^\dagger}{\mathrm{tr}(N\rho N^\dagger)}$, $\psi = \lambda\rho \cdot \frac{O\rho O^\dagger}{\mathrm{tr}(P\rho P^\dagger)}$ and $p = \lambda\rho \cdot \frac{\mathrm{tr}(M\rho M^\dagger)}{\mathrm{tr}(N\rho N^\dagger)}$, we have $\chi \circ \psi = \lambda\rho \cdot \frac{(OM)\rho(OM)^\dagger}{\mathrm{tr}((ON)\rho(ON)^\dagger)}$ and $p \circ \psi = \lambda\rho \cdot \frac{\mathrm{tr}((MO)\rho(MO)^\dagger)}{\mathrm{tr}((NO)\rho(NO)^\dagger)}$. By exhaustively applying the above rewrite rules, the left-hand side $F$ normalizes to a barycentric sum over terms of the form $X_i[\mathbf{y}_{k_1} := \mathbf{e}_{k_1}, \dots, \mathbf{y}_{k_i} := \mathbf{e}_{k_i}; \chi_i]$, or $X_k[\mathbf{y}_i := \mathbf{e}_i; \chi_i]$ for short. Let us extend the syntax of terms as follows:

$$ P, Q ::= \lambda\rho.\mathrm{tr}(M\rho M^\dagger) \mid 1 - P \mid P \cdot Q \mid P/Q \quad F, G ::= \dots \mid P \cdot F \mid F + G, $$

where $M \in \mathcal{M}(\tilde{\mathcal{H}}_Q)$ is in the Clifford+T fragment, with the new connectives are interpreted in the expected way. Particularly, $\llbracket P \rrbracket : \mathfrak{D}(\tilde{\mathcal{H}}_Q) \rightarrow \mathbb{A}^+$. Together with $F_1 +_p F_2 \rightarrow p \cdot F_1 + (1-p) \cdot F_2$ the considered constraints are now equivalently defined through constraints

$$ \Gamma \vdash \sum_{1 \le i \le k} P_i \cdot X_i[\overline{\mathbf{y}_i := \mathbf{e}_i}, \chi_i] \le X_\ell. $$

Bringing all coefficients $P_i$ to a common denominator $Q$, i.e., $P_i = \frac{Q_i}{Q}$, and by multiplying the left- and right-hand side by $Q$, we finally arrive at a constraint of the form

$$ \Gamma \vdash \sum_{1 \le i \le k} Q_i \cdot X_i[\overline{\mathbf{y}_i := \mathbf{e}_i}, \chi_i] \le Q \cdot X_\ell. \qquad (8) $$

Since the denominator $Q$ is guaranteed non-zero under $\Gamma$, this constraint is, by construction, semantically equivalent to the initial constraint $\Gamma \vdash F \le X_\ell$. Moreover, all coefficients $Q_i$ and $Q$ are finite products of traces $\lambda\rho.\mathrm{tr}(M_j\rho M^\dagger)$, for some matrices $M_j$.

Recall the encoding of input states in the notion of polynomial expectation (7). Let $\vec{Y}$ collect the $n$ variables of $\mathbb{A}^d[\mathbf{St}_{\mathrm{CT}}]$ representing to the classical input, similar let $\vec{A}$ (resp. $\vec{B}$) collects the $2^m$ variables representing the real (resp.imaginary part) of the density matrix. Let $\vec{Z}$ abbreviate the sequence of all such variables, in total, $n + 2^{2m+1}$ many. Let $MS_d$ denote the set of monomials over $\vec{Z}$ of degree $d$. Thus, every polynomial in $\mathbb{A}^d[\mathbf{St}_{\mathrm{CT}}]$ can be written as $\sum_{t \in MS_d} c_t \cdot t$ for some coefficients $c_t \in \mathbb{A}$. In particular, this means that any polynomial solution $\alpha$ to $C$ maps variables to polynomials of this form. We now represent these polynomial expectations abstractly, introducing for each $X' \in \mathbf{EVar}$ and $t \in MS_d$ an indeterminate coefficient $c_{t,X'}$, thereby representing polynomial expectations $\alpha(X')$ as polynomials $P_{X'} \triangleq \sum_{t \in MS_d} c_{t,X'} \cdot t$.
Using this interpretation of variables, we now turn the constraints (8) into polynomial inequalities so as to employ Proposition 1. Let $\lceil \mathbf{e} \rceil$ be the translation of program expressions using indeterminates $Y \in \vec{Y}$. Clearly, $\lceil \mathbf{e} \rceil$ is a polynomial. Extending this encoding in the natural way, we obtain an encoding $\lceil \mathbf{b} \rceil$ of Boolean program expressions $\mathbf{b}$. Observe that any trace $\text{tr}(M\rho M^\dagger)$ is just an algebraic polynomial over the coefficients in $M$ and $M^\dagger$. As the probability functions $p_{i,k}$ just compute such a trace, the predicate $\Gamma$ is naturally modeled in the theory of real closed fields, using indeterminates $\vec{Y}$ to encode Boolean expressions, and indeterminates $\vec{A}$ and $\vec{B}$ the checks on $p_{i,k}$. Likewise, as we have eliminated divisions, the factors $Q_i$ and $Q$ in (8) become expressible as algebraic polynomials $\lceil Q_i \rceil$ and $\lceil Q \rceil$ over $\vec{A}$ and $\vec{B}$.

It remains to encode the terms $X_i[\vec{y}_i := \mathbf{e}_i, \chi_i]$, and $X_\ell$, taking into account their interpretation via $P_{X_i}$ and $P_{X_\ell}$, respectively. First, observe that using the encoding for expressions, the update $\vec{y}_i := \mathbf{e}_i$ on variable $y_j$ is expressible as a polynomial $E_j$, given by the composition of corresponding polynomials $\lceil \mathbf{e}_j \rceil$. Likewise, the real and imaginary parts of entries $(\chi_i(\rho))_{j,k}$ are expressible as polynomial fractions $\lceil \text{Re}(\chi_{j,k}) \rceil$ and $\lceil \text{Im}(\chi_{j,k}) \rceil$, respectively ($1 \le j, k \le 2^m$). Putting things together, the constraint (8), becomes expressible as

$$ \lceil \Gamma \rceil \Rightarrow \sum_{1 \le i \le k} \lceil Q_i \rceil \cdot P_{X_i}[(Y_i/E_i)_{1 \le i \le n}, (A_{j,k}/\lceil \text{Re}(\chi_{j,k}) \rceil, B_{j,k}/\lceil \text{Im}(\chi_{j,k}) \rceil)_{1 \le j,k \le 2^m}] \le \lceil Q \rceil \cdot P_{X_\ell}, $$

The substitution on polynomials $P_{X_i}$ are to be performed in parallel. All involved expressions are polynomials, except that the substitutions $\lceil \text{Re}(\chi_{j,k}) \rceil$ and $\lceil \text{Im}(\chi_{j,k}) \rceil$ introduce fractions of (non-negative) polynomials. Multiplying out via a common denominator and rewriting polynomial comparisons to the standard form $P \ge 0$ and $\neg(P \ge 0)$, results in a translation of $\lceil \Gamma \rceil \vdash F \le X_\ell$ of the initial constraint $\Gamma \vdash F \le X_\ell$. Universally quantifying over $\vec{Z}$, the formula becomes equi-satisfiable with $\Gamma \vdash F \le X_\ell$, in the sense that any assignment by $\gamma$ from variables $c_{t,X'}$ to $\mathcal{A}$ makes the corresponding assignment $\alpha(X') = P_{X'}[\gamma] = \sum_{t \in \mathcal{MS}_\alpha} \gamma(c_{t,X'}) \cdot t$ a solution to $\Gamma \vdash F \le X_\ell$, and vice versa.

For decidability, it is now sufficient to note that $(\text{stm}, f, \alpha) \in \text{QINF}(\mathbb{A}^d[\text{St}_{\text{CT}}])$ iff (i) $\alpha$ is a solution to the constraints $C$ generated by $\text{qinf}[\text{stm}]{X} = G$; (ii) $\alpha(X) = f$, and (iii) this solution falls into the class $\mathbb{A}^d[\text{St}_{\text{CT}}]$. This is an immediate consequence of Theorem 3. By the construction above, we have already seen that (i) is expressible within the theory of real closed fields. Point (ii) just means that the coefficients of the template $P_X$ assigned to the input variable $X$ coincides with that of $f \in \mathbb{A}^d[\text{St}_{\text{CT}}]$. Point (iii) just means that the polynomials $P_{X'}$ are non-negative. Naturally, these constraints have to be fulfilled only on admissible quantum inputs (self-adjointness, trace 1, positive eigenvalues), which is easily seen to be representable as a formula admissible($\vec{A}, \vec{B}$). Finally, let $\lceil P_X = f \rceil$ denote that the algebraic coefficients of $P_X$ and $f$ coincide, and let $\vec{c}$ collects all introduced coefficient variables $c_{m,X'}$ encoding the polynomial assignment $\alpha$. Summing up,

$$ \exists \vec{c}, \forall \vec{Y}, \forall \vec{A}, \forall \vec{B}, \text{admissible}(\vec{A}, \vec{B}) \Rightarrow \bigwedge_{(\Gamma \vdash F \le X_\ell) \in C} \lceil \Gamma \rceil \vdash F \le X_\ell \land \lceil P_X \rceil = f \land \bigwedge_{X' \in \text{EVar}} (P_{X'} \ge 0), $$
yields a formula in the theory of real closed fields that is valid iff (stm, f, α) ∈ QINFER($\mathbb{A}^d[\text{St}_{\text{CT}}]$). Through quantifier elimination (Proposition 1) this formula can be turned into an equivalent, quantifier free formula ψ. Atoms of ψ are just inequalities over finite sums and products in $\mathbb{A}$. Since the latter is decidable, we conclude decidability of QINFER($\mathbb{A}^d[\text{St}_{\text{CT}}]$).

*Complexity.* Let $|\text{stm}|$ be the size of the statement **stm**. Now we consider the bound $O(|\psi|) \cdot (jd)^{i^{O(l)}}$ in Proposition 1 wrt. the above formula:

- the number of alternations *l* is constant *l* = 1,

- the degree *d* of the polynomials is the one we have fixed in $\mathbb{A}^d[\text{St}_{\text{CT}}]$,

- the number of variables *i* is equal to the universally quantified variables (for classical and quantum data) $n + 2^{2m+1} = 2^{O(|\text{stm}|)}$ plus the number of existentially quantified variables, which bounded by $|\text{stm}|(n + 2^{2m+1} + 1)^d$, as the number of monomials in a polynomial of $l_1$ variables and degree $l_2$ is bounded by $(l_1 + 1)^{l_2}$ and the number of polynomials is bounded by the number of expectation variables (Hence the size of the program $|\text{stm}|$). Hence $i = 2^{dO(|\text{stm}|)}$,

- the number of polynomial inequalities *j* is bounded by $3|\text{stm}|$ (the inequalities added by Figure 7) plus the number of constraints added by the **admissible**($\vec{A}, \vec{B}$), which is in $2^{O(|\text{stm}|)}$. Hence $j = 2^{O(|\text{stm}|)}$,

- the size of the formula $|\psi|$ is also in $2^{O(|\text{stm}|)}$ as each polynomial inequality corresponds to a constant number of logical symbols.

Putting all together, the obtained bound is in $2^{2dO(|\text{stm}|)}$.

## E Example of applications of quantum weakest pre-expectation

*Example 7.* Consider the expectations $P: \text{St} \to \{0,1\}$ and $f: \text{St} \to \mathbb{R}^{+\infty}$.

1. If **stm** does not perform any measurement, then **stm** is deterministic, in the sense that either $\text{term}_{\text{stm}}(\sigma) = \{1: (\downarrow, \tau)\}$, in case **stm** is terminating on $\sigma$, or $\text{term}_{\text{stm}}(\sigma) = \emptyset$. Then $\text{qwp}_{\text{stm}}(P)(\sigma) \in \{0,1\}$ gives the (weakest) pre-condition for $\tau$ satisfying *P*, in the sense of classical (partial) program correctness.

2. If **stm** performs measurements, then $\text{term}_{\text{stm}}(\sigma)$ is a sub-distribution over terminal configurations of the shape $(\downarrow, \tau)$. In this case, $\text{qwp}_{\text{stm}}(P)(\sigma) \in [0, 1]$ is the probability that these terminal configurations satisfy *P*.

3. $\text{qwp}_{\text{stm}}(\underline{1})(\sigma)$ gives the probability that **stm** terminates on initial state $\sigma$. In particular, $\text{qwp}_{\text{stm}}(\underline{1}) = \underline{1}$ implies that **stm** is almost-surely terminating.

4. $\text{qwp}_{\text{stm}}(f)(\sigma)$ returns the value $\mathbb{E}_{\text{term}_{\text{stm}}(\sigma)}(f)$, that is, the mean value of the function *f* on the distribution $\text{term}_{\text{stm}}(\sigma)$.

5. Given the measurement operators $\{M_{k,i}\}_{k \in \{0,1\}}$, $\text{qwp}_{\text{stm}}(f)(\sigma)$, where $f(s, \rho) \triangleq \text{tr}(M_{k,i}\rho)$, represents the probability that the outcome of measuring the i-th qubit of $\rho$ is *k*.
6. Suppose the statement `stm` contains a cost counter `ct` (some particular variable), and let `ect_stm` ≜ `qwp_stm(cost)`, where the expectation `cost` is defined by `cost(s, ρ) ≜ max{0, s(ct)}`. Then `ect_stm(σ) : R<sup>+∞</sup>` yields the expected cost of running `stm` on input `σ`, *upon termination*. In contrast to [5], `ect_stm` can capture a variety of monotonic *and* non-monotonic cost models such as time, space usage, output sizes, bit entanglement, etc. Notice that `ect_stm` takes only terminating traces into account, in the sense of partial correctness. As such, `ect_stm` does not represent the *edge-case* of programs that are not almost-surely terminating but have finite cost.