# Reasoning about Recursive Quantum Programs

A new assertion logic for verifying quantum programs with probabilistic
control

Zhaowei Xu  Institute of Software, Chinese Academy of
SciencesHaidianBeijingChina Laboratoire de Recherche en Informatique,
Université Paris-SaclayOrsayFrance<EMAIL_ADDRESS>,  Mingsheng Ying  Institute
of Software, Chinese Academy of SciencesHaidianBeijingChina University of
Technology SydneyAustralia Tsinghua UniversityHaidianBeijingChina
<EMAIL_ADDRESS>and  Benoît Valiron  École CentraleSupélecOrsayFrance
Laboratoire de Recherche en Informatique, Université Paris-SaclayOrsayFrance
<EMAIL_ADDRESS>
(0000)

###### Abstract.

Most modern (classical) programming languages support recursion. Recursion has
also been successfully applied to the design of several quantum algorithms and
introduced in a couple of quantum programming languages. So, it can be
expected that recursion will become one of the fundamental paradigms of
quantum programming. Several program logics have been developed for
verification of quantum $\mathbf{while}$-programs. However, there are as yet
no general methods for reasoning about (mutual) recursive procedures and
ancilla quantum data structure in quantum computing (with measurement). We
fill the gap in this paper by proposing a parameterized quantum assertion
logic and, based on which, designing a quantum Hoare logic for verifying
parameterized recursive quantum programs with ancilla data and probabilistic
control. The quantum Hoare logic can be used to prove partial, total, and even
probabilistic correctness (by reducing to total correctness) of those quantum
programs. In particular, two counterexamples for illustrating incompleteness
of non-parameterized assertions in verifying recursive procedures, and, one
counterexample for showing the failure of reasoning with exact probabilities
based on partial correctness, are constructed. The effectiveness of our logic
is shown by three main examples — recursive quantum Markov chain (with
probabilistic control), fixed-point Grover’s search, and recursive quantum
Fourier sampling.

recursive quantum programming, quantum variable localization, quantum
assertion logic, program verification, probabilistic reasoning

††copyright: acmcopyright††journalyear: 0000††doi:
00.0000/0000000.0000000††journal: TOCL††journalvolume: 00††journalnumber:
0††article: 000††publicationmonth: 0††ccs: Computer systems organization
Embedded systems††ccs: Computer systems organization Redundancy††ccs: Computer
systems organization Robotics††ccs: Networks Network reliability

##  1\. Introduction

###  1.1. Background and motivation

Quantum computation nowadays has become a hot topic in computer science. One
of the fundamental incentives of this research direction is to have
successfully designed several quantum algorithms, particularly, Shor’s
algorithm (Shor, 1994) and Grover’s search algorithm (Grover, 1996), which by
employing the intriguing and unnatural effects of quantum mechanics, e.g.
superposition and entanglement, can obtain significant computational
advantages. The design of quantum algorithms is mainly based on the slogan
“quantum data and classical control”, that is, that the data could be
superposed and even entangled, which can be manipulated by basic quantum
operations — unitary evolution and measurement, but the high-level control is
still classical (either deterministic or probabilistic, e.g. case, loops,
etc). (For recent discussions about quantum control, i.e. superposition of
quantum programs or superposition of quantum processes, see, e.g., (Badescu
and Panangaden, 2015), (Chiribella, 2012; Chiribella et al., 2013), and Chaps.
6 and 7 of (Ying, 2016).)

#### Quantum programming with recursion.

Classical recursion, as a high-level control structure, has been applied to
quantum algorithm design, and brought substantial advantages to quantum
computation. Instead of speaking about quantum algorithms with while-loop
control (as examples of tail recursion, say, Shor’s algorithm (Shor, 1994) and
Grover’s search algorithm (Grover, 1996)), we shall exemplify quantum
algorithms with general recursion. The first representative is Grover’s fixed-
point search algorithm (Grover, 2005; Yoder et al., 2014), which, by applying
(mutual) recursion, provides his famous/popular original search algorithm
(Grover, 1996) with an advantage — converging monotonically to the target
state. As another typical example, recursive quantum Fourier sampling
(Bernstein and Vazirani, 1997) requires exponentially fewer queries than the
classical one, and has extensive applications in research on quantum
complexity theory (cf. the Introduction of (McKague, 2012)). This quantum
algorithm is described by a recursive procedure with pointer passing and
ancilla qubits. As a third example, recursive quantum Markov chain is a
quantum extension of Etessami and Yannakakis’s Recursive Markov chains
(Etessami and Yannakakis, 2009), and can be used to simulate a multi-player
game with probabilistic control (Feng et al., 2013b) (to be the running
example of this paper).

Implementation of quantum algorithms, i.e. quantum programming, has been
extensively investigated for the past two decades (also following the slogan
“quantum data and classical control”), including both high-level (imperative)
and low-level (functional) programming languages and their semantics
(Altenkirch and Grattage, 2005; Ömer, 2003; Sabry, 2003; Sanders and Zuliani,
2000; Selinger, 2004a), as surveyed in (Selinger, 2004a; Gay, 2006; Ying,
2016). In particular, recursive procedures with pointer passing have already
been introduced by Selinger in his high-level quantum programming language
$\mathrm{QPL}$ (Selinger, 2004a). The literature (Ying, 2016) defined a
quantum $\mathbf{while}$-language with recursion and local variables (to
describe ancilla quantum data). In the last few years, a number of mature low-
level quantum programming languages have been developed, e.g., Quipper (Green
et al., 2013), Scaffold (Abhari et al., 2012), LIQUi$|\rangle$ (Wecker and
Svore, 2014), Q$\\#$ (Svore et al., 2018), and QWIRE (Paykin et al., 2017).

#### Verification of quantum programs.

In view of counter-intuitiveness of quantum effects, quantum programming is an
inherently error-prone process. To ensure correctness and safety of quantum
systems, formal verification and formal program analysis (static approaches)
is a right choice (Baltag and Smets, 2011; Brunet and Jorrand, 2004; Ying et
al., 2017; Li and Ying, 2018; Liu et al., 2019), relative to running-time
(dynamic) approaches like testing and debugging, due to a series of
frustrating facts: quantum states fail to be directly observed before
measurement; the current state could be potentially destroyed after
measurement; and the measurement result is randomly distributed. Among those
formal methods on quantum programming, we prefer program-logic-based
approaches, e.g. quantum program logic (Baltag and Smets, 2011; Brunet and
Jorrand, 2004), compared with model-based methods, e.g. quantum model checking
(Gay et al., 2008; Feng et al., 2013a, 2015; Ying et al., 2014), since the
former is developed in a syntax-oriented style making it easily extensible to
various program features, e.g. recursion, non-determinism, parallelism, etc.

Hoare logic has been the fundamental method for formal program verification
(Apt et al., 2009). The basic idea of this logic is based on the intermediate
assertion method (Floyd, 1967; Hoare, 1969), which was originated with Alan
Turing (Apt and Olderog, 2019) (called Turing-Floyd-Hoare Principle). Hoare’s
approach makes (interactive) theorem proving for verifying high-level
algorithmic description language proceed at the same abstraction level as the
language itself. Thus verification using Hoare logic is more human-friendly
than low-level (machine-friendly) verification. Several Hoare-like logics for
reasoning about quantum programs have been developed (Chadha et al., 2006;
Feng et al., 2007; Kakutani, 2009; Ying, 2011; Unruh, 2019b, a; Barthe et al.,
2020). Among them, D’Hondt and Panangaden (D’Hondt and Panangaden, 2006)
proposed a notion of quantum weakest precondition for a general quantum
operation. The attractiveness of this approach is that quantum predicates,
used as preconditions and postconditions, are modelled by Hermitian operators
and thus have a natural interpretation as physical observables. Based on this,
a quantum Hoare-like logic for reasoning about quantum
$\mathbf{while}$-language was designed and its (relative) completeness was
established, by Ying in (Ying, 2011). In these quantum Hoare logics, we find
that

  1. (1)

Quantum predicate can merely describe a fixed property on quantum states, and
the mechanism for guaranteeing termination is not designed in a syntactical
style.

  2. (2)

These programming languages don’t support general recursion, and there is no
compositional inference rule for the structure of ancilla quantum variables.

  3. (3)

These logics are mainly for verifying deterministic properties of quantum
programs, and at most can do reasoning with approximate probabilities. In
other words, there is no axiomatic basis for reasoning about quantum programs
with exact probabilities.

###  1.2. Contributions of the Paper

The aim of this paper is to propose an assertion logic for verifying
parameterized recursive quantum programs with ancilla qubits or quints (the
abbreviation of quantum int). By using formulas of this assertion logic as
pre- and post-conditions, a quantum Hoare logic is designed for proving
partial correctness, total correctness, and even probabilistic correctness
(including probabilistic termination) of those quantum programs. The work
extends D’Hondt and Panangaden’s quantum predicates and quantum weakest
preconditions (D’Hondt and Panangaden, 2006), and Ying’s quantum Hoare logic
(Ying, 2011). Concretely speaking, five main contributions are highlighted:

  * •

We extends the syntax of quantum $\mathbf{while}$-language defined in (Ying,
2011) with general recursive procedures. For the formal semantics of the
extended quantum programming language, we define a nondeterministic
operational semantics by introducing the concept of labeled transition
relation, define a quantum-operation-directed denotational semantics
(independent of program states), and relate them to each other (cf. Thm. 3.7).
Note that the denotation of a recursive procedure can be defined as the least
fixed point of a function over quantum operations, making the representation
of this denotation have a closed form. The formal semantics can be used to
describe behaviors of quantum programs with probabilistic control (cf. Exams.
3.3 and 3.6).

  * •

By constructing two counterexamples (cf. Exm. 5.1 for partial correctness, and
Exam. 5.2 for total correctness), we illustrate the failure of Hoare’s
approach (i.e. intermediate assertion method) with quantum predicates as pre-
and post-conditions in verifying recursive procedures. To extend the
applicability of Hoare’s approach from while loops to general recursion (cf.
Rem. 5.7), we have to introduce a parameterized quantum assertion logic
extending quantum predicates by incorporating parameters. In the setting of
this assertion logic, we redefine the notion of Löwner order and upper (resp.
lower) limit of quantum predicates, quantum program correctness and
expressiveness of intermediate assertions developed in (D’Hondt and
Panangaden, 2006; Ying, 2011) (cf. Thms. 4.14 and 4.15).

  * •

We introduce inference rules for proving both partial and total correctness of
recursive procedures with formulas of the new assertion logic as pre- and
post-conditions. These rules usually should be used in combination with the
Substitution Rule, dealing with substitution for parameters in pre- and post-
conditions of a Hoare’s triple (cf. Exms. 5.1 and 5.2 for counterexamples).
The rules of proving total correctness can be adapted to proving probabilistic
correctness, i.e. reasoning with both approximate and exact probabilities (cf.
Thms. 5.4 and 5.6), based on the result of (general or compact) soundness and
completeness. However, the rules of proving partial correctness can’t be used
universally for reasoning with exact probabilities, even if the issue of
nontermination is involved (cf. Rem. 5.6 for a counterexample). Note that the
rule for proving total correctness is purely syntactic, and, as a special
case, we obtain a syntax-directed inference rule for proving total correctness
of while loops. We also discuss the issues of synthesizing intermediate
assertions and necessity of parameters in verifying recursive procedures and
while loops. These discussions reveal that recursion is generally more complex
than while loops in the setting of program logics.

  * •

Verification of some more sophisticated recursive quantum programs like the
example of recursive quantum Fourier sampling cannot be done by merely using
the above techniques; they further need the facilities of variable
localization and parameter passing. So, our fourth main contribution is to
develop inference rules for proving both partial and total correctness of
variable localization and recursive quantum procedures with pointer passing.
To this end, we propose two different but equivalent inference rules for
proving the two correctness of variable localization, and the Adaptation Rule
for dealing with the substitution of program variables in pointer passing.
Note that previous proof rules for recursive procedures should be used jointly
with Adaptation Rule in verifying parameterized recursive procedures. The
proof rule for variable localization endows the logic with the ability of
verifying a (general) quantum operation in a compositional way. Various
aforementioned results, like Thms. 3.7, 4.15, 5.4, 5.6 (and soundness and
completeness results), can be extended to covering these facilities.

  * •

The fifth and last main contribution is to present various examples and
related work. Among these examples, we adopt recursive quantum Markov chain as
the running example of the paper, since it can fully show the ability of our
logic in dealing with quantum programs with probabilistic control.
Specifically speaking, this example illustrates operational semantics,
denotational semantics, and reasoning with exact probability (including
probabilistic correctness and probabilistic termination). The examples of
Grover’s fixed-point search and recursive quantum Fourier sampling are used to
illustrate rules for proving partial and total correctness of recursive
quantum programs with deterministic control (containing auxiliary facilities).
We compare our quantum Hoare logic with other (deterministic, probabilistic or
quantum) Hoare-like logics, and discuss local and global reasoning in the
setting of quantum computing.

###  1.3. Organization of the Paper

We present preliminaries on quantum program verification in Sec. 2; syntax and
semantics of recursive quantum programs are defined in Sec. 3; quantum
assertion logic is presented in Sec. 4; starting proof systems are shown in
Sec. 5; expanded proof systems including auxiliary facilities are shown in
Sec. 6; Case studies of Grover’s fixed-point search and recursive quantum
Fourier sampling are presented in Sec. 7; Comparison with the related work is
given in Sec. 8; Sec. 9 concludes the paper with a discussion of the future
work.

The running example of recursive quantum Markov chain is throughout the paper
from Subsec. 3.1 through Subsecs. 3.2 and 3.3 to Subsec. 5.3. The proof (or
proof schetch) of various results, including proof for the two counterexamples
— Exms. 5.1 and 5.2, proof of soundness and completeness results, and a full
verification of Grover’s fixed-point search and recursive quantum Fourier
sampling, are put into the appendix.

##  2\. Preliminaries

For convenience of the reader, we briefly review the basics of quantum theory,
and fix the symbols and notations used in the subsequent sections.

###  2.1. Quantum states

#### Definition of linear operators

The state space of a quantum system is a Hilbert space $\mathcal{H}$. For any
positive integer $n$, an $n$-dimensional Hilbert space is essentially the
space $\mathbb{C}^{n}$ of complex vectors. We use Dirac’s notation,
$|\psi\rangle$, to denote a complex vector in $\mathbb{C}^{n}$. The inner
product (resp. outer product) of two vectors $|\psi\rangle$ and
$|\phi\rangle$, denoted $\langle\psi|\phi\rangle$ (resp.
$|\psi\rangle\langle\phi|$), is the product of
$\langle\psi|\triangleq(|\psi\rangle)^{{\dagger}}$ (i.e. the conjugate
transpose of $|\psi\rangle$) and $|\phi\rangle$ (resp. the product of
$|\psi\rangle$ and $\langle\phi|$). The norm of a vector $|\psi\rangle$ is
denoted by $||\psi||\triangleq\sqrt{\langle\psi|\psi\rangle}$. We say that a
set of vectors $\\{|\psi_{i}\rangle\\}_{i}$ is an orthonormal basis of
$\mathcal{H}$, if $\langle\psi_{i}|\psi_{j}\rangle=\delta_{i,j}$ for all $i,j$
(where $\delta_{i,j}=1$ if $i=j$, and $=0$ otherwise). Then every vector of
$\mathcal{H}$ can be represented as a linear combination of any orthonormal
basis of $\mathcal{H}$. We define (linear) operators over $\mathcal{H}$ as a
linear mapping. In the space $\mathbb{C}^{n}$, an operator $A$ is represented
by an $n\times n$ matrix. We say that $A$ is Hermitian, if $A=A^{\dagger}$
(where $A^{\dagger}$ denotes the conjugate transpose of $A$). Let
$I_{\mathcal{H}}$ (resp. $0_{\mathcal{H}}$) be the identity (resp. zero)
operator over $\mathcal{H}$. The trace of an operator $A$ is defined by
$\mathit{tr}(A)\triangleq\Sigma_{i}\langle i|A|i\rangle$ (the sum of entries
on the main diagonal of $A$ w.r.t. any orthonormal basis of $A$).

######  Lemma 2.0 (Spectral decomposition, cf. (Nielsen and Chuang, 2000, Box
2.2)).

Every linear operator $A$ of Hilbert space $\mathcal{H}$ is Hermitian, if, and
only if, it can be decomposed as $A=\sum
p_{i}|\psi_{i}\rangle\langle\psi_{i}|$, where $\\{p_{i}\\}_{i}$ are reals and
$\\{|\psi_{i}\rangle\\}_{i}$ is an orthonormal basis of $\mathcal{H}$.

#### Löwner order between linear operators

An operator $A$ is positive, if for all vectors $|\psi\rangle\in\mathcal{H}$,
$\langle\psi|A|\psi\rangle\geq 0$. Note that every positive operator is
Hermitian, and that every Hermitian operator of the form $\sum
p_{i}|\psi_{i}\rangle\langle\psi_{i}|$ is positive iff $p_{i}\geq 0,\forall i$
(cf. Lem. 2.1). The concept of positivity induces the Löwner order
$\sqsubseteq$ between operators:

  * •

$A\sqsubseteq B$, if $B-A$ is positive;

  * •

$A=B$, if $A\sqsubseteq B$ and $B\sqsubseteq A$.

By definition, it follows, for any operators $A$ and $B$, that

  * •

$0_{\mathcal{H}}\sqsubseteq A$ iff $A$ is positive;

  * •

$A\sqsubseteq B$ iff there is a positive operator $C$ s.t. $A+C=B$.

The least upper bound L. U. B. (resp. greatest lower bound G. L. B.) operator
in a complete partial order generated by Löwner comparison is denoted as
$\bigsqcup$ (resp. $\bigsqcap$). For example, the L. U. B. (resp. G. L. B.) of
a sequence of operators $\\{A_{n}\\}_{n\geq 0}$ with $\forall n\geq 0.\
A_{n}\sqsubseteq A_{n+1}$ (resp. $\forall n\geq 0.\ A_{n}\sqsupseteq A_{n+1}$)
will be denoted by $\bigsqcup_{n\geq 0}A_{n}$ (resp. $\bigsqcap_{n\geq
0}A_{n}$). For the existence of those bounds, the reader is referred to the
literature (Selinger, 2004a) and (Ying, 2016).

#### Pure quantum state

A pure quantum state is represented by a unit vector, i.e., a vector
$|\psi\rangle$ with $||\psi||=1$ (used to represent the data states of a
quantum circuit). For example, a qubit, or quantum bit, system refers to the
case when $\mathcal{H}=\mathbb{C}^{2}$. An important basis of a qubit system
is the computational basis with $|0\rangle\triangleq(1,0)^{\dagger}$ and
$|1\rangle\triangleq(0,1)^{\dagger}$, which corresponds to the $0/1$ in a
classical bit. Another important basis, called the $\pm$ basis, consists of
$|\pm\rangle\triangleq\frac{1}{\sqrt{2}}(|0\rangle\pm|1\rangle)$. One can
represent multi-qubits by tensor-producting each qubit. For instance, the
classical two-bit string $01$ can be represented by
$|0\rangle\otimes|1\rangle$ (or $|01\rangle$ for short). An $m$-qubit system
lives in the space $\mathbb{C}^{2^{m}}=(\mathbb{C}^{2})^{\otimes m}$ that is
the $m$-time tensor product of a single qubit system $\mathbb{C}^{2}$.

#### Mixed quantum state

However, after applying a quantum measurement, a (pure) quantum state is
possibly changed to a mixed state, i.e. a random distribution over an ensemble
of pure states $\mathbb{E}=\\{(p_{i},|\psi_{i}\rangle)\\}_{i}$, which states
that the system is in state $|\psi_{i}\rangle$ with probability $p_{i}$. One
can also use density operators to represent both pure and mixed quantum
states. Formally, a density operator is a positive operator $\rho$ whose trace
$\mathit{tr}(\rho)=1$. For example, the density operator $\rho$ for a mixed
state represented by the ensemble $\mathbb{E}$ is
$\rho=\sum_{i}p_{i}|\psi_{i}\rangle\langle\psi_{i}|$; in particular, a pure
state $|\psi\rangle$ can be identified with the density operator
$\rho=|\psi\rangle\langle\psi|$.

#### Representation of quantum states

If density operators are used directly to represent quantum states, we will
find that the resulting state after applying a quantum operation is probably
not a density operator but its sub-part. Note that the missing part of the
final state is due to non-termination. To cope with this issue, the concept of
partial density operator (abbr. $\mathrm{PDO}$) is introduced by Selinger
(Selinger, 2004b) to model a sub-part of a density operator. Strictly
speaking, a $\mathrm{PDO}$ is a positive operator $\rho$ with
$0\leq\mathit{tr}(\rho)\leq 1$ (Particularly, a density operator is a
$\mathrm{PDO}$ $\rho$ with $\mathit{tr}(\rho)=1$). Defining quantum states as
$\mathrm{PDO}$s ensures that quantum states are closed under quantum
operations. The set of $\mathrm{PDO}$s on $\mathcal{H}$ is denoted by
$\mathcal{D}(\mathcal{H})$.

###  2.2. Quantum operations

#### Definition of quantum operations

The evolution of an open quantum system $\mathcal{H}$ can be characterized by
an (admissible) quantum operation (abbr. $\mathrm{QOP}$) $\mathcal{E}$, which
is a linear, trace-non-increasing and completely positive super operator from
$\mathcal{D}(\mathcal{H})$ to $\mathcal{D}(\mathcal{H})$ (By complete
positivity of $\mathcal{E}$ on $\mathcal{H}$ is meant that for all linear
operators $A$ on $\mathcal{H}^{\prime}\supseteq\mathcal{H}$ with $A\sqsupseteq
0_{\mathcal{H}^{\prime}}$, $\mathcal{E}(A)\sqsupseteq
0_{\mathcal{H}^{\prime}}$). Namely, for any state
$\rho\in\mathcal{D}(\mathcal{H})$, the final state after the $\mathrm{QOP}$
$\mathcal{E}$ is $\mathcal{E}(\rho)\in\mathcal{D}(\mathcal{H})$ with
$\mathit{tr}(\mathcal{E}(\rho))\leq\mathit{tr}(\rho)$. For every
$\mathrm{QOP}$ $\mathcal{E}$, there exists a set of Kraus operators
$\\{E_{k}\\}_{k}$ s.t. $\mathcal{E}(\rho)=\sum_{k}E_{k}\rho
E_{k}^{\dagger},\forall\rho$ (See, e.g., (Nielsen and Chuang, 2000)). We
denote the Kraus form of $\mathcal{E}$ by writing
$\mathcal{E}=\sum_{k}E_{k}\diamond E_{k}^{\dagger}$. Since $\mathcal{E}$ is
positive and trace-non-increasing, it holds that
$0\sqsubseteq\sum_{k}E_{k}^{\dagger}E_{k}\sqsubseteq I$. For example, an
identity (resp. zero) operation refers to $I_{\mathcal{H}}\diamond
I_{\mathcal{H}}$ (resp. $0_{\mathcal{H}}\diamond 0_{\mathcal{H}}$).

#### Dual of quantum operation

The Schrödinger-Heisenberg dual of a $\mathrm{QOP}$ $\mathcal{E}$, denoted
$\mathcal{E}^{*}$, is defined as

  * •

$\mathit{tr}\big{(}A\mathcal{E}(\rho)\big{)}=\mathit{tr}\big{(}\mathcal{E}^{*}(A)\rho\big{)}$,
$\forall\rho$ and $\forall A$;

  * •

or, in the Kraus form,
$\mathcal{E}^{*}\triangleq\sum_{k}E_{k}^{\dagger}\diamond E_{k}$, if
$\mathcal{E}=\sum_{k}E_{k}\diamond E_{k}^{\dagger}$.

######  Lemma 2.0.

Let $\lambda\geq 0$, let $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ be respective
$\mathrm{QOP}$s on $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$, let $\mathcal{F}$,
$\mathcal{G}$ be $\mathrm{QOP}$s on $\mathcal{H}$, and let
$\\{\mathcal{F}_{n}\\}$ be a non-decreasing sequence of $\mathrm{QOP}$s on
$\mathcal{H}$. It is the case that

(1):

$(\mathcal{E}_{1}\otimes\mathcal{E}_{2})^{*}=\mathcal{E}_{1}^{*}\otimes\mathcal{E}_{2}^{*}$;

(2):

$(\lambda\mathcal{F})^{*}=\lambda\mathcal{F}^{*}$;

(3):

$(\mathcal{F}+\mathcal{G})^{*}=\mathcal{F}^{*}+\mathcal{G}^{*}$;

(4):

$(\mathcal{F}\circ\mathcal{G})^{*}=\mathcal{G}^{*}\circ\mathcal{F}^{*}$;

(5):

$(\bigsqcup_{n=0}^{\infty}\mathcal{F}_{n})^{*}=\bigsqcup_{n=0}^{\infty}\mathcal{F}_{n}^{*}$.

#### Representation of unitary operators

Operations (or evolutions) on (closed) quantum systems can be characterized by
a unitary operator. An operator $U$ is a unitary operator if its conjugate
transpose is its own inverse, i.e., $U^{\dagger}U=UU^{\dagger}=I$. Common
single-qubit unitary operators include the Hadamard operator $H$ and the Pauli
operator $X$:

$H\triangleq\frac{1}{\sqrt{2}}\left[\begin{array}[]{cc}1&1\\\
1&-1\end{array}\right],\quad X\triangleq\left[\begin{array}[]{cc}0&1\\\
1&0\end{array}\right]$

Intuitively, $H$ transforms between the computational and the $\pm$ basis,
i.e., $H|0\rangle=|+\rangle$ and $H|1\rangle=|-\rangle$, and $X$ is a bit
flip, i.e., $X|0\rangle=|1\rangle$ and $X|1\rangle=|0\rangle$. The evolution
of $\mathrm{PDO}$ $\rho$ under unitary operator $U$ is $\rho\rightarrow U\rho
U^{\dagger}$, and thus $U$ can be written as a $\mathrm{QOP}$
$\mathcal{E}=U\diamond U^{\dagger}$.

#### Representation of measurement

The way to extract information about a quantum system is called a quantum
measurement. Mathematically, a quantum measurement on a system over
$\mathcal{H}$ can be described by a set of linear operators $\\{M_{m}\\}_{m}$
with $\sum_{m}M_{m}^{\dagger}M_{m}=I_{\mathcal{H}}$. If we perform a
measurement $\\{M_{m}\\}_{m}$ on a state $\rho$, the outcome $m$ is observed
with probability $p_{m}\triangleq\mathit{tr}(M_{m}\rho M_{m}^{\dagger})$ for
each $m$, and, with the observation $m$, the state collapses to a post-
measurement state $M_{m}\rho M_{m}^{\dagger}/p_{m}$. To characterize the
evolution of a quantum measurement as a $\mathrm{QOP}$, we remark that the
probability $p_{m}$ can be encoded into the post-measurement state $M_{m}\rho
M_{m}^{\dagger}/p_{m}$, resulting in $M_{m}\rho M_{m}^{\dagger}$. So, such an
evolution can be written as the $\mathrm{QOP}$ $\mathcal{E}=M_{m}\diamond
M_{m}^{\dagger}$. One of the major differences between classical and quantum
computation is that a quantum measurement could potentially change the state
itself. For example, if we perform the standard (i.e. computational-basis)
measurement $M=\\{M_{0}\triangleq|0\rangle\langle
0|,M_{1}\triangleq|1\rangle\langle 1|\\}$ on state $\rho=|+\rangle\langle+|$,
then with probability $\frac{1}{2}$ the outcome is $0$ (resp. $1$), and the
final state becomes $|0\rangle\langle 0|$ (resp. $|1\rangle\langle 1|$).

#### Representation of open systems

Suppose that we have a joint quantum system $\mathcal{H}\triangleq Q\otimes R$
and wish to trace out system $R$ by using partial trace function
$\mathit{tr}_{R}$. Let $\\{|i\rangle\\}_{i}$ be an orthonormal basis for $R$.
Then $\mathit{tr}_{R}$ can be defined by the $\mathrm{QOP}$
$\mathit{tr}_{R}\triangleq\sum_{i}\langle i|\diamond|i\rangle$. We can
represent a (separable) joint $\mathrm{QOP}$ for quantum systems $Q$ and $R$
by the tensor product $\mathcal{E}_{Q}\otimes\mathcal{E}_{R}$ of
$\mathrm{QOP}$s $\mathcal{E}_{Q}$ for $Q$ and $\mathcal{E}_{R}$ for $R$. It is
a convention in the quantum information literature that when operations only
apply to part of a quantum system, one should assume that an identity
operation is applied on the rest. For example, applying $\mathcal{E}_{R}$
(resp. $\mathcal{E}_{Q}$) to $\rho\in\mathcal{D}(Q\otimes R)$ means applying
$(I_{Q}\diamond I_{Q})\otimes\mathcal{E}_{R}$ [resp.
$\mathcal{E}_{Q}\otimes(I_{R}\diamond I_{R})$] to $\rho$. Here the identity
operation is usually omitted for simplicity. Thus, writing $\mathcal{E}(\rho)$
with $\mathrm{QOP}$ $\mathcal{E}$ on $\mathcal{H}$ and $\mathrm{PDO}$
$\rho\in\mathcal{D}(\mathcal{H}^{\prime})$ will naturally imply that
$\mathcal{H}\subseteq\mathcal{H}^{\prime}$.

#### Löwner order between super operators

Define the Löwner order between $\mathrm{QOP}$s based on that between linear
operators:

  * •

$\mathcal{E}\sqsubseteq\mathcal{F}$, if
$\mathcal{E}(\rho)\sqsubseteq\mathcal{F}(\rho)$, $\forall\rho$;

  * •

$\mathcal{E}=\mathcal{F}$, if $\mathcal{E}\sqsubseteq\mathcal{F}$ and
$\mathcal{F}\sqsubseteq\mathcal{E}$.

By definition, we have, for any $\mathrm{QOP}$s $\mathcal{E}$ and
$\mathcal{F}$, that

  * •

$0\diamond 0\sqsubseteq\mathcal{E}$ iff $\mathcal{E}$ is completely positive;

  * •

$\mathcal{E}\sqsubseteq\mathcal{F}$ iff there is $\mathrm{QOP}$ $\mathcal{G}$
s.t. $\mathcal{E}+\mathcal{G}=\mathcal{F}$.

The least upper bound $\bigsqcup_{n\geq 0}\mathcal{E}_{n}$ (resp. greatest
lower bound $\bigsqcap_{n\geq 0}\mathcal{E}_{n}$) of a sequence of
$\mathrm{QOP}$s $\\{\mathcal{E}_{n}\\}_{n\geq 0}$ with $\forall n\geq 0.\
\mathcal{E}_{n}\sqsubseteq\mathcal{E}_{n+1}$ (resp. $\forall n\geq 0.\
\mathcal{E}_{n}\sqsupseteq\mathcal{E}_{n+1}$) is defined as

  * •

$\big{(}\bigsqcup_{n\geq
0}\mathcal{E}_{n}\big{)}(\rho)\triangleq\bigsqcup_{n\geq
0}\mathcal{E}_{n}(\rho)$, $\forall\rho$;

  * •

$\big{(}\bigsqcap_{n\geq
0}\mathcal{E}_{n}\big{)}(\rho)\triangleq\bigsqcap_{n\geq
0}\mathcal{E}_{n}(\rho)$, $\forall\rho$.

###  2.3. Quantum predicates

#### Definition of quantum predicates

As defined in (D’Hondt and Panangaden, 2006), a quantum predicate (abbr.
$\mathrm{QPRD}$) on a Hilbert space $\mathcal{H}$ is a Hermitian operator
$M_{\mathcal{H}}$ such that $0_{\mathcal{H}}\sqsubseteq
M_{\mathcal{H}}\sqsubseteq I_{\mathcal{H}}$. The satisfiability of a state
(i.e. $\mathrm{PDO}$) $\rho\in\mathcal{D}(\mathcal{H}^{\prime})$ in the
$\mathrm{QPRD}$ $M_{\mathcal{H}}$ with
$\mathcal{H}\subseteq\mathcal{H}^{\prime}$ is defined by the trace
$\mathit{tr}(M_{\mathcal{H}}\rho)$ if $\mathcal{H}=\mathcal{H}^{\prime}$, and
$\mathit{tr}\big{(}(M_{\mathcal{H}}\otimes
I_{\mathcal{H}^{\prime\prime}})\rho\big{)}$ if
$\mathcal{H}\otimes\mathcal{H}^{\prime\prime}=\mathcal{H}^{\prime}$.
Intuitively, $\mathit{tr}(M_{\mathcal{H}}\rho)$ [resp.
$\mathit{tr}\big{(}(M_{\mathcal{H}}\otimes
I_{\mathcal{H}^{\prime\prime}})\rho\big{)}$] is the expectation of the truth
value of predicate $M_{\mathcal{H}}$ in state $\rho$. Note that restricting
$M_{\mathcal{H}}$ to between $0_{\mathcal{H}}$ and $I_{\mathcal{H}}$ ensures
that $0\leq\mathit{tr}(M_{\mathcal{H}}\rho)\leq 1$ [resp.
$0\leq\mathit{tr}\big{(}(M_{\mathcal{H}}\otimes
I_{\mathcal{H}^{\prime\prime}})\rho\big{)}\leq 1$] for any
$\rho\in\mathcal{D}(\mathcal{H}^{\prime})$. We shall write
$\mathcal{P}(\mathcal{H})$ for the set of $\mathrm{QPRD}$s on $\mathcal{H}$.

#### How to use quantum predicates

By Lem. 2.1, every $\mathrm{PDO}$ $\rho$ has the spectral decomposition
$\rho\triangleq\sum_{i\in A}p_{i}|\varphi_{i}\rangle\langle\varphi_{i}|$,
where $\forall i\in A.\ 0\leq p_{i}\leq 1$, $\sum_{i\in A}p_{i}\leq 1$ and
$\sum_{i\in A}|\varphi_{i}\rangle\langle\varphi_{i}|=I$. In practice, we
prefer to use projection operators, e.g. $M\triangleq\sum_{i\in
B}|\varphi_{i}\rangle\langle\varphi_{i}|$, with $B\subseteq A$, to define the
(precise) properties of $\rho$. Intuitively speaking,
$\mathit{tr}(M\rho)=\sum_{i\in B}p_{i}$ is the probability of $\rho$ falling
into the subspace represented by $M$. In particular,
$\mathit{tr}(|\varphi_{i}\rangle\langle\varphi_{i}|\rho)=p_{i}$ is the
probability of $\rho$ in the state $|\varphi_{i}\rangle\langle\varphi_{i}|$,
which can be used to reveal internal ingredients of a quantum state;
$\mathit{tr}(I\rho)=\mathit{tr}(\rho)$ is the probability of $\rho$ falling
into the whole space, which is one of the usual statistical properties on
quantum states. For example, the $\mathrm{PDO}$
$\rho\triangleq\frac{|0\rangle\langle 0|+|1\rangle\langle 1|}{2}$ represents
the resulting state $\\{(\frac{1}{2},|0\rangle),(\frac{1}{2},|1\rangle)\\}$
after a standard measurement on $|+\rangle$. Note that
$\mathit{tr}(|0\rangle\langle 0|\rho)=\frac{1}{2}$ (resp.
$\mathit{tr}(|1\rangle\langle 1|\rho)=\frac{1}{2}$) is the probability of
$\rho$ in the state $|0\rangle\langle 0|$ (resp. $|1\rangle\langle 1|$),
$\mathit{tr}(I\rho)=1$ is the probability of $\rho$ falling into the whole
space.

#### Expressiveness of quantum predicates

$\mathrm{QPRD}$s can be used to describe classical properties (at the
propositional level). For example, we can use a main diagonal matrix – a kind
of $\mathrm{QPRD}$ – to express (probabilistic) boolean functions, if
classical information is encoded as (a random distribution of) states of a
computational basis. To sum up, the quantum counterpart of a classical
predicate is a main diagonal matrix that encodes its indicator function. The
strength of adopting $\mathrm{QPRD}$s as assertions, among many others, lies
in the fact that various properties of quantum effects can be represented
thereof. For example, the predicate $M=|+\rangle\langle+|$, i.e.

$\displaystyle M$ $\displaystyle=$ $\displaystyle\frac{|0\rangle\langle
0|+|0\rangle\langle 1|+|1\rangle\langle 0|+|1\rangle\langle 1|}{2}$

describes that a state $\rho$ is in the equal superposition $|+\rangle$ with
probability $\mathit{tr}(M\rho)$; the predicate
$N=\frac{|00\rangle+|11\rangle}{\sqrt{2}}\frac{\langle 00|+\langle
11|}{\sqrt{2}}$, i.e.

$\displaystyle N$ $\displaystyle=$ $\displaystyle\frac{|00\rangle\langle
00|+|00\rangle\langle 11|+|11\rangle\langle 00|+|11\rangle\langle 11|}{2}$

describes that a state $\rho$ is in the maximally entangled state
$\frac{|00\rangle+|11\rangle}{\sqrt{2}}$ with probability
$\mathit{tr}(N\rho)$.

#### Definition of quantum implication

The Löwner comparison $M\sqsubseteq N$ between $\mathrm{QPRD}$s $M$ and $N$ is
a quantum simulation of the classical implication “$F\rightarrow G$”. Recall
that the validity of $F\rightarrow G$, denoted $\models F\rightarrow G$, is
defined as: for any assignment $v$, $v\models F\implies v\models G$, where
$v\models F$ denotes the satisfiability (truth value) of $F$ under $v$. The
following lemma extends the semantics of classical implication into the
quantum case (To better see this, we remark that the less than or equal to
$\leq$ defined on the closed real interval $[0,1]$ can be seen as a
probabilistic extension of the classical implication $\implies$ on the set of
truth values $\\{0,1\\}$).

######  Lemma 2.0 (A semantic viewpoint of Löwner order (Ying, 2011, Lem.
2.1)).

Let $M,N\in\mathcal{P}(\mathcal{H})$. Then $M\sqsubseteq N$ if, and only if,
$\mathit{tr}(M\rho)\leq\mathit{tr}(N\rho)$ for all
$\rho\in\mathcal{D}(\mathcal{H})$.

##  3\. Recursive quantum programs

Recursive quantum programs can be viewed as a recursive procedural extension
of quantum base language $\mathit{qPL}$ — the non-while-loop part of quantum
$\mathbf{while}$-language introduced in (Ying, 2011, 2016). In this section,
we define its syntax and formal semantics, and introduce the example of
recursive quantum Markov chain as the running example of the paper.

###  3.1. Definition of the syntax

We assume a set $\mathit{Var}$ of quantum variables annotated with a type
$\mathbf{Bool}$ or $\mathbf{Int}$, and
$\bar{q}\triangleq(q_{1},\ldots,q_{n})\subseteq\mathit{Var}$. For each
$q\in\mathit{Var}$, its state Hilbert space is denoted by $\mathcal{H}_{q}$.
Then $\bar{q}$ is associated with the Hilbert space
$\mathcal{H}_{\bar{q}}\triangleq\bigotimes_{i=1}^{n}\mathcal{H}_{q_{i}}$. If
$\it type(q)=\mathbf{Bool}$, then $\mathcal{H}_{q}$ is a two-dimensional
Hilbert space with computational basis $\\{|0\rangle,|1\rangle\\}$ (i.e. the
space of a qubit). If $\it type(q)=\mathbf{Int}$, then $\mathcal{H}_{q}$ is an
infinite-dimensional Hilbert space with computational basis
$\\{|n\rangle\colon n\in\mathbb{Z}\\}$ (i.e. the space of a quint, e.g. the
space of a photon). Note that we are able to use multiple (e.g. $n$) qubits to
form any finite (e.g. $2^{n}$) dimensional Hilbert space, and usually use the
computational basis of an infinite-dimensional Hilbert space to simulate
integers $\mathbb{Z}$, which can be used to implement the classical
(deterministic) control of a quantum program (cf. Exm. 5.1). (Working with
infinite Hilbert space is as with finite space, see, e.g., (Prugovecki,
1982).)

Now we are able to define a (possibly recursive) procedural extension of
quantum base language $\mathit{qPL}$ (the non-while-loop part of quantum
$\mathbf{while}$-language (Ying, 2011, 2016)), denoted by $\mathit{RqPL}$ (We
can implement a while loop as a tail recursion, cf. Subsec. 5.4). A recursive
quantum program $P\in\mathit{RqPL}$ usually consists of a procedural
declaration $D$, associating some body with a procedure name, followed by some
statement $S$ possibly containing activation statements to declared
procedures. Formally, $\mathit{RqPL}$ is generated by the following grammar:

$\begin{array}[]{rcll}P&\triangleq&D::S&\mbox{Quantum program}\\\
D&\triangleq&\mathbf{Proc}\ \langle\mathit{proc}_{1}\rangle\colon
S_{1},\ldots,\mathbf{Proc}\ \langle\mathit{proc}_{n}\rangle\colon
S_{n}&\mbox{Procedure declaration}\\\
S&\triangleq&\mathbf{bot}&\mbox{Bottom}\\\ &\mid&\mathbf{skip}&\mbox{No
operation}\\\ &\mid&q:=|0\rangle&\mbox{Initialization}\\\
&\mid&\bar{q}\;{\ast}{=}\;U&\mbox{Unitary operation}\\\
&\mid&S_{1};S_{2}&\mbox{Sequential composition}\\\ &\mid&\mathbf{if}\ \Box
m\cdot M[\bar{q}]=m\rightarrow S_{m}\ \mathbf{fi}&\mbox{Probabilistic
branching}\\\ &\mid&\mathbf{call}\ \langle\mathit{proc}_{i}\rangle,\quad 1\leq
i\leq n&\mbox{Procedure call}\end{array}$

where for each declared (possibly recursive) procedure $\mathbf{Proc}\
\langle\mathit{proc}_{i}\rangle\colon S_{i}$, $1\leq i\leq n$,
$\mathit{proc}_{i}$ and $S_{i}$ are the name and body of the procedure. For
the follow-up development, we first assume that quantum programs have no local
variables, and that procedures $\mathit{proc}_{i}$ dispense with parameter
passing. The treatment of these auxiliary facilities is deferred to Sec. 6.

The intended semantics of language constructs above is similar to that of
their classical counterparts. To see the quantum features of those constructs,
we remark that:

(i):

for the initialization, the choice of the state $|0\rangle$ as the initial
value is due to the fact that any known quantum state can be prepared by
applying a unitary operator to $|0\rangle$;

(ii):

for the probabilistic branching, different branches $\\{S_{m}\\}_{m}$ are
chosen according to (randomly distributed) outcomes of the measurement
$M\triangleq\\{M_{m}\\}_{m}$ on the qubits $\bar{q}$, and the measurement
process could possibly destroy the current state.

###### Example 3.0 (Alternative definition of $\mathbf{bot}$).

Quantum program $\mathbf{bot}$, as a basic program construct, can also be
implemented as the call statement $\mathbf{call}\ P_{\mathbf{bot}}$ with
$P_{\mathbf{bot}}$ declared by

$\mathbf{Proc}\ P_{\mathbf{bot}}\colon\mathbf{call}\ P_{\mathbf{bot}}$

###### Remark 3.1.

For the syntax of $\mathit{RqPL}$, we choose $\mathbf{bot}$ as a basic program
construct, rather than as in Exm. 3.1, because the denotational semantics of
recursive procedures and its derivatives (e.g. formal weakest preconditions)
will need to be defined on the “absolute” semantics of $\mathbf{bot}$ as a
meta-symbol, otherwise a circular reasoning will occur.

#### Running example of the paper.

To illustrate that our method has the capacity for dealing with probabilistic
control, we adopt the example of recursive quantum Markov chains (abbr.
$\mathrm{RQMC}$) (Feng et al., 2013b) as the running example of the paper.

###### Example 3.0 (Syntax of $\mathrm{RQMC}$).

Let us introduce a modified version of Exm. 1 in the literature (Feng et al.,
2013b). This is a two-player (Alice and Bob) game of first tossing a dice,
simulated by a qubit system $q$, and then making a decision for either being
the final winner, flagged as $|\pm\rangle$, or transferring $q$ to the other.
The protocol of Alice goes as follows. She first measures $q$ immutably by the
observable

$\displaystyle M$ $\displaystyle\triangleq$
$\displaystyle\bigg{\\{}M_{0}\triangleq\sqrt{\frac{1}{4}}I,\
M_{1}\triangleq\sqrt{\frac{1}{2}}I,\
M_{2}\triangleq\sqrt{\frac{1}{4}}I\bigg{\\}}$

If the outcome $0$ is observed, then she sets $q$ to be $|+\rangle$ and
terminates; if $1$ is observed, then she transfers $q$ to the Bob and lets him
play; if $2$ is observed, the game will get stuck. The protocol of Bob goes
similarly except that he will use the following observable

$\displaystyle M^{\prime}$ $\displaystyle\triangleq$
$\displaystyle\bigg{\\{}M_{0}^{\prime}\triangleq\sqrt{\frac{1}{2}}I,\
M_{1}^{\prime}\triangleq\sqrt{\frac{1}{2}}I\bigg{\\}}$

instead, and if the measurement outcome $0$ is observed, he sets $q$ to be
$|-\rangle$ and terminates. After Bob wins, Alice will do nothing and
terminate immediately. The game starts with Alice. The core of the game is
mutually recursive procedures $\mathit{Alice}$ and $\mathit{Bob}$ programmed
as

$\begin{array}[]{c}\mathbf{Proc}\ \mathit{Alice}\colon\mathbf{if}\ \Box m\cdot
M[q]=m\rightarrow S_{m}\ \mathbf{fi}\\\ \mathbf{Proc}\
\mathit{Bob}\colon\mathbf{if}\ \Box m\cdot M^{\prime}[q]=m\rightarrow
S_{m}^{\prime}\ \mathbf{fi}\end{array}$

where $\\{S_{m}\\}_{m=0,1,2}$ and $\\{S_{m}^{\prime}\\}_{m=0,1}$ are defined
as

$\begin{array}[]{lll}S_{0}\triangleq
q\;{\ast}{=}\;H&S_{1}\triangleq\mathbf{call}\
\mathit{Bob}&S_{2}\triangleq\mathbf{bot}\\\
S_{0}^{\prime}\triangleq\mathbf{call}\ \mathit{Alice}&S_{1}^{\prime}\triangleq
q\;{\ast}{=}\;HX&\end{array}$

The main program $\mathrm{RQMC}$ of the game is as follows.

$\displaystyle\mathrm{RQMC}$ $\displaystyle\triangleq$ $\displaystyle q:=0;\
\mathbf{call}\ \mathit{Alice}$

###  3.2. Nondeterministic operational semantics

(Bot) | $\langle\mathbf{bot},\rho\rangle\xrightarrow{\epsilon}\langle E,0\rangle$ |  | (Skip) | $\langle\mathbf{skip},\rho\rangle\xrightarrow{\epsilon}\langle E,\rho\rangle$
---|---|---|---|---
(Init) | $\dfrac{\sum_{i}|i\rangle_{q}\langle i|=I_{q}}{\langle q:=|0\rangle,\rho\rangle\xrightarrow{\epsilon}\langle E,\sum_{i}|0\rangle_{q}\langle i|\rho|i\rangle_{q}\langle 0|\rangle}$ |  | (Unit) | $\dfrac{UU^{\dagger}=U^{\dagger}U=I_{\bar{q}}}{\langle\bar{q}\;{\ast}{=}\;U,\rho\rangle\xrightarrow{\epsilon}\langle E,U\rho U^{\dagger}\rangle}$
(Comp1) | $\dfrac{\langle S_{1},\rho\rangle\xrightarrow{l}\langle S_{1}^{\prime},\rho^{\prime}\rangle\mbox{ and }S_{1}^{\prime}\neq E}{\langle S_{1};S_{2},\rho\rangle\xrightarrow{l}\langle S_{1}^{\prime};S_{2},\rho^{\prime}\rangle}$ |  | (Comp2) | $\dfrac{\langle S_{1},\rho\rangle\xrightarrow{l}\langle E,\rho^{\prime}\rangle}{\langle S_{1};S_{2},\rho\rangle\xrightarrow{l}\langle S_{2},\rho^{\prime}\rangle}$
(Case) | $\dfrac{M=\\{M_{m}\\}_{m}\mbox{ and }\sum_{m}M_{m}^{\dagger}M_{m}=I_{\bar{q}}}{\langle\mathbf{if},\rho\rangle\xrightarrow{m}\langle S_{m},M_{m}\rho M_{m}^{\dagger}\rangle}$ |
(Proc) | $\dfrac{\mathbf{Proc}\ \mathit{proc}\colon S\in D}{\langle\mathbf{call}\ \mathit{proc},\rho\rangle\xrightarrow{\epsilon}\langle S,\rho\rangle}$ |  | (Except) | $\dfrac{\mbox{Other cases of $S$ and $l$}}{\langle S,\rho\rangle\xrightarrow{l}\bot}$
Table 1. Labeled transition relation $\xrightarrow{l}$ with
$l\triangleq\epsilon\mid m$.

The operational semantics of quantum programs can be defined as a
nondeterministic transition relation $\rightarrow$ between quantum
configurations $\langle S,\rho\rangle$ — a global description for quantum
program $S\in\mathit{RqPL}$ on the current state represented as a
$\mathrm{PDO}$ $\rho$. For the well-definedness of $\langle S,\rho\rangle$, it
is required that $\mathit{Var}(S)\subseteq\mathit{Var}(\rho)$. Note that $S$
could be the empty statement $E$ indicating that $\rho$ is the final output.
By a labeled transition

$\langle S,\rho\rangle\xrightarrow{l}\langle S^{\prime},\rho^{\prime}\rangle$

we mean that program $S$ on input state $\rho$ is evaluated in one step with
label $l$ to program $S^{\prime}$ with output state $\rho^{\prime}$. The
transition relation $\xrightarrow{l}$ for $\mathit{RqPL}$ is defined in Tab.
1.

To better understand the relation $\xrightarrow{l}$, we remark that

  * •

The transition relation $\xrightarrow{l}$ is defined in a nondeterministic
manner. The unique source of nondeterminism is execution of a case statement,
and each measurement outcome $m$ corresponds to a different path of execution.
For those deterministic one-step executions, we use $\xrightarrow{\epsilon}$
instead ($\epsilon$ means there are no other choices). Otherwise (when the
cases of $S$ and $l$ mismatch), the execution will fail and fall into a bottom
state $\bot$.

  * •

The annotated outer product $|\psi\rangle_{\bar{q}}\langle\phi|$ and identity
operator $I_{\bar{q}}$ mean that
$|\psi\rangle\langle\phi|,I\in\mathcal{H}_{\bar{q}}$.

  * •

Here, and in the sequel, the statement $\mathbf{if}\ \Box m\cdot
M[\bar{q}]=m\rightarrow S_{m}\ \mathbf{fi}$ is shortened with $\mathbf{if}$.

###### Example 3.0 (Operational semantics of $\mathrm{RQMC}$).

Let $\mathrm{RQMC}$ be the quantum program defined in Exm. 3.2. Let annotated
$\mathrm{PDO}$ $\rho_{q}\in\mathcal{D}(\mathcal{H}_{q})$ with
$\mathit{tr}(\rho_{q})=1$. Then part of the operational semantics of
$\mathrm{RQMC}$ (Alice wins after two rounds) can be developed step by step as
follows.

$\begin{array}[]{rl}&\langle q:=0;\mathbf{call}\
\mathit{Alice},\rho_{q}\rangle\\\ \xrightarrow{\epsilon}&\langle\mathbf{call}\
\mathit{Alice},|0\rangle_{q}\langle 0|\rangle\\\
\xrightarrow{\epsilon}&\langle\mathbf{if}\ \Box m\cdot M[q]=m\rightarrow
S_{m}\ \mathbf{fi},|0\rangle_{q}\langle 0|\rangle\\\
\xrightarrow{1}&\langle\mathbf{call}\
\mathit{Bob},\frac{1}{2}|0\rangle_{q}\langle 0|\rangle\\\
\xrightarrow{\epsilon}&\langle\mathbf{if}\ \Box m\cdot
M^{\prime}[q]=m\rightarrow S_{m}^{\prime}\
\mathbf{fi},\frac{1}{2}|0\rangle_{q}\langle 0|\rangle\\\
\xrightarrow{0}&\langle\mathbf{call}\
\mathit{Alice},\frac{1}{4}|0\rangle_{q}\langle 0|\rangle\\\
\xrightarrow{\epsilon}&\langle\mathbf{if}\ \Box m\cdot M[q]=m\rightarrow
S_{m}\ \mathbf{fi},\frac{1}{4}|0\rangle_{q}\langle 0|\rangle\\\
\xrightarrow{0}&\langle q\;{\ast}{=}\;H,\frac{1}{16}|0\rangle_{q}\langle
0|\rangle\\\ \xrightarrow{\epsilon}&\langle
E,\frac{1}{16}|+\rangle_{q}\langle+|\rangle\end{array}$

The last configuration shows that Alice wins after two rounds with probability
$\frac{1}{16}$.

To extend the one-step labeled transition relation $\xrightarrow{l}$ to a
multi-step labeled transition relation $\xrightarrow{\alpha}$ with
$\alpha\triangleq l\mid\alpha_{1}\alpha_{2}$, we define $\langle
S,\rho\rangle\xrightarrow{\alpha}C$ ($C$ is either $\langle
S^{\prime},\rho^{\prime}\rangle$ or $\bot$) as $\xrightarrow{l}$, defined in
Tab. 1, if $\alpha=l$; or as $\langle
S,\rho\rangle\xrightarrow{\alpha_{1}}\langle
S^{\prime\prime},\rho^{\prime\prime}\rangle$ and $\langle
S^{\prime\prime},\rho^{\prime\prime}\rangle\xrightarrow{\alpha_{2}}C$ for some
$S^{\prime\prime}$ and $\rho^{\prime\prime}$ otherwise.

###### Remark 3.2 (Comparison with Ying’s operational semantics).

Ying’s original operational semantics (Ying, 2011, 2016) is defined in a
nondeterministic way without resorting to the concept of labels, and there is
only one rule (followed by the side condition $E;S_{2}\triangleq S_{2}$) for
the case of composition, which is able to combine together the (Comp1, Comp2)
rules of Tab. 1. In other words, in order to define a more fine-grained
operational semantics, we have to introduce the concept of labeled transition
relation, at the price of introducing an extra rule (Except) dealing with the
case of exception.

###  3.3. $\mathrm{QOP}$-directed denotational semantics

(Param) | $\llbracket\Omega_{\bar{q}}\rrbracket=\omega_{\bar{q}}$ | (Bot) | $\llbracket\mathbf{bot}\rrbracket=0\diamond 0$
---|---|---|---
(Skip) | $\llbracket\mathbf{skip}\rrbracket=I\diamond I$ | (Init) | $\llbracket q:=|0\rangle\rrbracket=\sum_{i}|0\rangle_{q}\langle i|\diamond|i\rangle_{q}\langle 0|$
(Unit) | $\llbracket\bar{q}\;{\ast}{=}\;U\rrbracket=U\diamond U^{\dagger}$ | (Comp) | $\llbracket S_{1};S_{2}\rrbracket=\llbracket S_{2}\rrbracket\circ\llbracket S_{1}\rrbracket$
(Case) | $\llbracket\mathbf{if}\rrbracket=\sum_{m}\llbracket S_{m}\rrbracket\circ(M_{m}\diamond M_{m}^{\dagger})$ | (Proc) | $\llbracket\mathbf{call}\ \mathit{proc}_{i}\rrbracket=\bigsqcup_{n=0}^{\infty}\llbracket S_{i}^{(n)}\rrbracket$
Table 2. Denotational semantics of $\mathit{RqPL}[\Omega]$.

The denotational semantics of a quantum program, denoted
$\llbracket\cdot\rrbracket$, is defined as a super operator (i.e.
$\mathrm{QOP}$). The semantics of each term is given in a compositional way,
except for the case of call statements. To handle this case, we need to define
the syntactic approximation (i.e., unrolling) of the bodies of mutually
recursive procedures.

###### Definition 3.0 (Syntactic approximation).

For declared recursive procedures $\mathit{proc}_{i}$ with body $S_{i}$,
$1\leq i\leq n$, the $k$th syntactic approximation $S_{i}^{(k)}$ is defined
as:

$\displaystyle S_{i}^{(0)}$ $\displaystyle\triangleq$
$\displaystyle\mathbf{bot}$ $\displaystyle S_{i}^{(k+1)}$
$\displaystyle\triangleq$ $\displaystyle
S_{i}\big{[}\ldots,\big{(}\mathbf{skip};S_{j}^{(k)}\big{)}\big{/}\mathbf{call}\
\mathit{proc}_{j},\ldots\big{]}$

where
$S_{i}\big{[}\ldots,\big{(}\mathbf{skip};S_{j}^{(k)}\big{)}\big{/}\mathbf{call}\
\mathit{proc}_{j},\ldots\big{]}$ stands for simultaneous substitution of
$\mathbf{skip};S_{j}^{(k)}$ for $\mathbf{call}\ \mathit{proc}_{j}$, for all
$1\leq j\leq n$, occurring inside $S_{i}$ (Here $\mathbf{skip}$ is used to
simulate the first-step transition $\xrightarrow{\epsilon}$ for the statement
$\mathbf{call}\ \mathit{proc}_{j}$, cf. the (Skip, Proc) rules of Tab. 1).

The denotational semantics $\llbracket\cdot\rrbracket$ for $\mathit{RqPL}$
with parameters $\Omega$ (denoted $\mathit{RqPL}[\Omega]$) is defined in Tab.
2, where the quantum program parameter $\Omega_{\bar{q}}$, ranging over the
set of all quantum programs for quantum variables $\bar{q}$, is interpreted as
the corresponding quantum operation parameter $\omega_{\bar{q}}$, ranging over
the set of all $\mathrm{QOP}$s on $\mathcal{H}_{\bar{q}}$. This is justified
by the fact that any $\mathrm{QOP}$ can be simulated by a non-parameterized
quantum program.

######  Lemma 3.0 (Well-definedness of $\llbracket\cdot\rrbracket$).

Let $S_{i}^{\prime}$ be a parameterized adaptation of $S_{i}$, the body of
$\mathbf{call}\ \mathit{proc}_{i}$, with $1\leq i\leq n$, by substituting
parameterized quantum program $\mathbf{skip};\Omega_{j}$ for each call-
statement $\mathbf{call}\ \mathit{proc}_{j}$ with $1\leq j\leq n$ occurring
inside $S_{i}$:

$\displaystyle S_{i}^{\prime}$ $\displaystyle\triangleq$ $\displaystyle
S_{i}\big{[}\big{(}\mathbf{skip};\Omega_{1}\big{)}\big{/}\mathbf{call}\
\mathit{proc}_{1},\ldots,\big{(}\mathbf{skip};\Omega_{j}\big{)}\big{/}\mathbf{call}\
\mathit{proc}_{j},\ldots,\big{(}\mathbf{skip};\Omega_{n}\big{)}\big{/}\mathbf{call}\
\mathit{proc}_{n}]$

Let $\mathcal{F}(\omega_{1},\ldots,\omega_{n})$ be a vectorial function on
$\mathrm{QOP}$s defined by

$\displaystyle\mathcal{F}$ $\displaystyle\triangleq$
$\displaystyle\big{(}\llbracket S_{1}^{\prime}\rrbracket,\ldots,\llbracket
S_{j}^{\prime}\rrbracket,\ldots,\llbracket S_{n}^{\prime}\rrbracket\big{)}$

Define the least sequence of $\mathrm{QOP}$s
$\big{\\{}\mathcal{F}_{i}^{k}(\bar{0})\triangleq\mathcal{E}_{i}^{(k)}\big{\\}}_{k\geq
0}$, $0\leq i\leq n$, generated by $\mathcal{F}$ as follows.

$\displaystyle\big{(}\mathcal{E}_{1}^{(0)},\ldots,\mathcal{E}_{j}^{(0)},\ldots,\mathcal{E}_{n}^{(0)}\big{)}$
$\displaystyle\triangleq$ $\displaystyle\big{(}0,\ldots,0,\ldots,0\big{)}$
$\displaystyle\big{(}\mathcal{E}_{1}^{(k+1)},\ldots,\mathcal{E}_{j}^{(k+1)},\ldots,\mathcal{E}_{n}^{(k+1)}\big{)}$
$\displaystyle\triangleq$
$\displaystyle\mathcal{F}\big{(}\mathcal{E}_{1}^{(k)},\ldots,\mathcal{E}_{j}^{(k)},\ldots,\mathcal{E}_{n}^{(k)}\big{)}$

It is the case that

(i):

$\llbracket S_{i}^{(k)}\rrbracket=\mathcal{F}_{i}^{k}(\bar{0})$ for all $k\geq
0$;

(ii):

$\llbracket S_{i}^{(k)}\rrbracket\sqsubseteq\llbracket
S_{i}^{(k+1)}\rrbracket$ for all $k\geq 0$.

###### Proof.

By definition of $\llbracket\cdot\rrbracket$ and
$\big{\\{}\mathcal{F}_{i}^{k}(\bar{0})\big{\\}}_{k\geq 0}$, Stat. (i) follows.
To show Stat. (ii), we remark that $\mathcal{F}$ is monotone, i.e. for any
$\mathrm{QOP}$s $\mathcal{E}_{j}$ and $\mathcal{F}_{j}$ with
$\mathcal{E}_{j}\sqsubseteq\mathcal{F}_{j}$,

$\displaystyle\mathcal{F}(\ldots,\mathcal{E}_{j},\ldots)$
$\displaystyle\sqsubseteq$
$\displaystyle\mathcal{F}(\ldots,\mathcal{F}_{j},\ldots)$

(Note that $\sqsubseteq$ distributes over components of the vector.) This is
the case due to linearity of (super operators) $\mathcal{F}$, together with
the fact that $\mathcal{E}_{j}+\mathcal{G}_{j}=\mathcal{F}_{j}$ for some
$\mathrm{QOP}$ $\mathcal{G}_{j}$. Then Stat. (ii) follows by induction on $k$,
together with monotonicity of $\mathcal{F}$. ∎

###### Remark 3.3 (Comparison with Ying’s denotational semantics).

The denotational semantics $\llbracket\cdot\rrbracket$ of Table 2 is defined
as a composition of $\mathrm{QOP}$s independent of the input $\rho$, which can
be seen as a parameterized extension of Ying’s original denotational semantics
(Ying, 2011, 2016). The parameterized version of denotational semantics helps
to explain that

  * •

$\big{\\{}\llbracket S_{i}^{(k)}\rrbracket\big{\\}}_{k\geq 0}$, $0\leq i\leq
n$, is the least sequence of $\mathrm{QOP}$s generated by $\mathcal{F}$;

  * •

$\big{\\{}\llbracket\mathbf{call}\ \mathit{proc}_{i}\rrbracket\big{\\}}_{0\leq
i\leq n}$ is the least fixed point of the vectorial function $\mathcal{F}$,
i.e.

    * –

$(\ldots,\llbracket\mathbf{call}\
\mathit{proc}_{j}\rrbracket,\ldots)=\mathcal{F}(\ldots,\llbracket\mathbf{call}\
\mathit{proc}_{j}\rrbracket,\ldots)$, and

    * –

for any $\mathrm{QOP}$s $\\{\mathcal{E}_{i}\\}_{0\leq i\leq n}$ with
$(\mathcal{E}_{1},\ldots,\mathcal{E}_{j},\ldots,\mathcal{E}_{n})=\mathcal{F}(\mathcal{E}_{1},\ldots,\mathcal{E}_{j},\ldots,\mathcal{E}_{n})$,
we have that $\llbracket\mathbf{call}\
\mathit{proc}_{j}\rrbracket\sqsubseteq\mathcal{E}_{j}$ for all $0\leq j\leq
n$.

as implied by Lem. 3.5.

###### Example 3.0 (Denotational semantics of $\mathrm{RQMC}$).

Let $\mathrm{RQMC}$ be the quantum program defined in Exm. 3.2. Let $S_{a}$
and $S_{b}$ denote the bodies of procedures $\mathit{Alice}$ and
$\mathit{Bob}$. Then $S_{a}^{\prime}\triangleq S_{a}[\Omega_{b}/\mathbf{call}\
\mathit{Bob}]$ and $S_{b}^{\prime}\triangleq S_{b}[\Omega_{a}/\mathbf{call}\
\mathit{Alice}]$. Thus we have that

$\displaystyle\mathcal{F}$ $\displaystyle\triangleq$ $\displaystyle(\llbracket
S_{a}^{\prime}\rrbracket,\llbracket
S_{b}^{\prime}\rrbracket)=(\frac{1}{4}H\diamond
H+\frac{1}{2}\omega_{b},\frac{1}{2}\omega_{a}+\frac{1}{2}HX\diamond XH)$

This implies that

$\displaystyle\mathcal{F}_{1}^{n}(\bar{0})$ $\displaystyle=$
$\displaystyle\Big{(}\sum_{k\geq 1}^{2k-1\leq
n}\frac{1}{4^{k}}\Big{)}H\diamond H+\Big{(}\sum_{k\geq 1}^{2k\leq
n}\frac{1}{4^{k}}\Big{)}HX\diamond XH$
$\displaystyle\mathcal{F}_{2}^{n}(\bar{0})$ $\displaystyle=$
$\displaystyle\Big{(}\sum_{k\geq 1}^{2k\leq n}\frac{1}{2\cdot
4^{k}}\Big{)}H\diamond H+\Big{(}\sum_{k\geq 1}^{2k-1\leq n}\frac{1}{2\cdot
4^{k-1}}\Big{)}HX\diamond XH$

By the (Proc) rule of Tab. 2, it follows that

$\displaystyle\llbracket\mathbf{call}\ \mathit{Alice}\rrbracket$
$\displaystyle=$
$\displaystyle\bigsqcup_{n=0}^{\infty}\mathcal{F}_{1}^{n}(\bar{0})=\frac{1}{3}H\diamond
H+\frac{1}{3}HX\diamond XH$

Finally, for any $\mathrm{PDO}$ $\rho$ with $\mathit{tr}(\rho)=1$, we have
that

$\displaystyle\llbracket\mathrm{RQMC}\rrbracket(\rho)$ $\displaystyle=$
$\displaystyle\llbracket q:=0;\mathbf{call}\ \mathit{Alice}\rrbracket(\rho)$
$\displaystyle=$ $\displaystyle(\llbracket\mathbf{call}\
\mathit{Alice}\rrbracket\circ\llbracket q:=0\rrbracket)(\rho)$
$\displaystyle=$ $\displaystyle\llbracket\mathbf{call}\
\mathit{Alice}\rrbracket\big{(}\llbracket q:=0\rrbracket(\rho)\big{)}$
$\displaystyle=$ $\displaystyle\llbracket\mathbf{call}\
\mathit{Alice}\rrbracket(|0\rangle\langle 0|)$ $\displaystyle=$
$\displaystyle\frac{1}{3}H|0\rangle\langle 0|H+\frac{1}{3}HX|0\rangle\langle
0|XH$ $\displaystyle=$
$\displaystyle\frac{1}{3}|+\rangle\langle+|+\frac{1}{3}|-\rangle\langle-|=\frac{1}{3}I$

###### Remark 3.4.

After round $n=2k-1$ ($k\geq 1$) of the two-player game (cf. Exm. 3.3), there
is a computed result $\frac{1}{4^{k}}|+\rangle\langle+|$, but the resulting
state as a whole (for all $k\geq 0$) should include the sum of all, i.e.,
$\sum_{k=1}^{\infty}\frac{1}{4^{k}}|+\rangle\langle+|=\frac{1}{3}|+\rangle\langle+|$
(cf. Exm. 3.6).

The following Theorem reveals the connection between operational and
denotational semantics. Namely, the meaning of running program $S$ on input
state $\rho$ is the sum of all possible output states $\rho^{\prime}$ (Note
that $\mathit{tr}(\rho^{\prime})$ denotes the probability of reaching
$\rho^{\prime}/\mathit{tr}(\rho^{\prime})$).

######  Theorem 3.7.

For any quantum program $S\in\mathit{RqPL}$, we have that

(1) $\displaystyle\llbracket S\rrbracket(\rho)$ $\displaystyle=$
$\displaystyle\sum_{\langle S,\rho\rangle\xrightarrow{\alpha}\langle
E,\rho^{\prime}\rangle}\rho^{\prime}$

where the summation of $\rho^{\prime}$ is taken for every possible $\alpha$
s.t. $\langle S,\rho\rangle\xrightarrow{\alpha}\langle
E,\rho^{\prime}\rangle$.

###### Proof.

See the proof of Thm. A.3. ∎

###### Remark 3.5.

To the right-hand side of Eq. (1) in Thm. 3.7, the summation should act upon
any (possibly overlapping) $\rho^{\prime}$, as long as $\langle
S,\rho\rangle\xrightarrow{\alpha}\langle E,\rho^{\prime}\rangle$ holds for a
different $\alpha$. For instance, there are two branches of a program each
having the computed result $\frac{1}{4}|0\rangle\langle 0|$, then the
resulting state as a whole should include the sum of both, i.e.,
$\frac{1}{4}|0\rangle\langle 0|+\frac{1}{4}|0\rangle\langle
0|=\frac{1}{2}|0\rangle\langle 0|$. By comparison, Ying’s original treatment
of this issue (Ying, 2011, 2016), due to lack of labels in transition rules,
is to use a multi-set instead to collect up all possible outputs.

##  4\. Quantum assertion logic

$\mathrm{QPRD}$s are simply employed in (D’Hondt and Panangaden, 2006; Ying,
2011) as pre- and post-conditions of quantum Hoare’s triples. However, to
achieve an effectively checkable (symbolic) Löwner comparison between
parameterized quantum predicates, we have to first define a parameterized
symbolic abstraction for $\mathrm{QPRD}$s — Parameterized Quantum Predicate
Terms (abbr. $\mathrm{PQPT}$), whose definition should be a trade off between
simplicity and expressibility so that we make a minimal use of parameters
ranging over a continuous space, and at the same time, make sure both
$\mathrm{QPRD}$s and all (possibly parameterized) intermediate assertions,
e.g. weakest (liberal) preconditions, in quantum program verification can be
expressed thereof.

####  $\mathrm{QOP}$’s dual as predicate transformer

To see the role of a $\mathrm{QOP}$’s dual in defining its weakest
precondition (i.e. $\mathrm{QPRD}$), note that every $\mathrm{QOP}$
$\mathcal{E}$ can be seen as a mapping over $\mathrm{PDO}$s $\rho$ and its
dual $\mathcal{E}^{*}$ as a mapping over $\mathrm{QPRD}$s $M$, i.e.

$\begin{array}[]{rlccc}\mathcal{E}&\colon&\rho&\mapsto&\mathcal{E}(\rho)\\\
\mathcal{E}^{*}&\colon&\mathcal{E}^{*}(M)&\mapsfrom&M\end{array}$

By definition of Schrödinger-Heisenberg dual, we have that

$\displaystyle\mathit{tr}\big{(}\mathcal{E}^{*}(M)\rho\big{)}$
$\displaystyle=$ $\displaystyle\mathit{tr}\big{(}M\mathcal{E}(\rho)\big{)}$

Intuitively, the truth value of $\mathcal{E}^{*}(M)$ at $\rho$ is equal to the
truth value of $M$ at $\mathcal{E}(\rho)$. That is that, $\mathcal{E}^{*}(M)$
is the weakest precondition of $\mathcal{E}$ w.r.t. the postcondition $M$
(D’Hondt and Panangaden, 2006). The beautiful duality between state-
transformer (forwards) and predicate-transformer (backwards) semantics plays a
key role in defining quantum assertion logic using the predicate transform
$\mathcal{E}^{*}$.

###  4.1. Parameterized quantum predicate terms

###### Definition 4.0 (Syntax of $\mathrm{PQPT}$s).

Let $\bar{q}$, $\bar{r}$ and $\bar{s}$ be lists of pairwise distinct quantum
variables with $\bar{q}=(\bar{r},\bar{s})$ (if any). Let $I_{\bar{q}}$ be the
constant symbol denoting the identity operator on $\mathcal{H}_{\bar{q}}$,
$\mathcal{X}_{\bar{q}}$ a metavariable for all first-order variables ranging
over $\mathcal{P}(\mathcal{H}_{\bar{q}})$ with
$\mathcal{X}_{\bar{q}}^{\dagger}=\mathcal{X}_{\bar{q}}$ (i.e. quantum
predicate variables), and $\mathcal{E}_{\bar{q}},\mathcal{F}_{\bar{q}}$
$\mathrm{QOP}$s on $\mathcal{H}_{\bar{q}}$ with
$\mathcal{E}_{\bar{q}}+\mathcal{F}_{\bar{q}}\sqsubseteq I_{\bar{q}}\diamond
I_{\bar{q}}$.

A parameterized base $\mathcal{B}_{\bar{q}}$ of $\mathrm{PQPT}$s on $\bar{q}$
(and its set of parameters $\mathit{Prmt}(\mathcal{B}_{\bar{q}})$) is defined
as

$\mathcal{B}_{\bar{q}}\
\big{(}\mathit{Prmt}(\mathcal{B}_{\bar{q}})\big{)}\quad\triangleq\quad\left\\{\begin{array}[]{ll}\mathcal{X}_{\bar{q}}&\big{(}\\{\mathcal{X}_{\bar{q}}\\}\big{)}\\\
I_{\bar{r}}\otimes\mathcal{B}_{\bar{s}}&\big{(}\mathit{Prmt}(\mathcal{B}_{\bar{s}})\big{)}\\\
\mathcal{B}_{\bar{r}}\otimes
I_{\bar{s}}&\big{(}\mathit{Prmt}(\mathcal{B}_{\bar{r}})\big{)}\\\
\mathcal{B}_{\bar{r}}\otimes\mathcal{B}_{\bar{s}}&\big{(}\mathit{Prmt}(\mathcal{B}_{\bar{r}})\uplus\mathit{Prmt}(\mathcal{B}_{\bar{r}})\big{)}\end{array}\right.$

A $\mathrm{PQPT}$ $P_{\bar{q}}$ on $\bar{q}$ (and its set of parameters
$\mathit{Prmt}(P_{\bar{q}})$) is defined as

$P_{\bar{q}}\
\big{(}\mathit{Prmt}(P_{\bar{q}})\big{)}\quad\triangleq\quad\mathcal{E}_{\bar{q}}^{*}(\mathcal{B}_{\bar{q}})+\mathcal{F}_{\bar{q}}^{*}(I_{\bar{q}})\
\big{(}\mathit{Prmt}(\mathcal{B}_{\bar{q}})\big{)}$

Note that a $\mathrm{PQPT}$ $P_{\bar{q}}$ is usually composed of two parts:
the parameterized part $\mathcal{E}_{\bar{q}}^{*}(\mathcal{B}_{\bar{q}})$ and
the non-parameterized part $\mathcal{F}_{\bar{q}}^{*}(I_{\bar{q}})$, which can
also be written as

$\displaystyle P_{\bar{q}}$ $\displaystyle\triangleq$
$\displaystyle\mathcal{E}_{\bar{q}}^{*}\bigg{(}\bigotimes_{\mathcal{X}\in\mathit{Prmt}(\mathcal{B}_{\bar{q}})}\mathcal{X}\bigg{)}+\mathcal{F}_{\bar{q}}^{*}(I_{\bar{q}})$

due to the convention that the identity operators in $\mathcal{B}_{\bar{q}}$
can be omitted.

Semantics of $\mathrm{PQPT}$s. Let $\mathbb{I}$ be the standard interpretation
of nonlogical symbols in the syntax of $\mathrm{PQPT}$s to the semantic
counterparts. Let $v$ be a mapping (i.e. assignment) from variables
$\mathcal{X}_{\bar{q}}$ to $\mathrm{QPRD}$s
$\mathcal{P}(\mathcal{H}_{\bar{q}})$, i.e.
$v(\mathcal{X}_{\bar{q}})\in\mathcal{P}(\mathcal{H}_{\bar{q}})$. The
denotation of a $\mathrm{PQPT}$ $P_{\bar{q}}$ under interpretation
$\mathbb{I}$ and assignment $v$, denoted $P_{\bar{q}}^{\mathbb{I},v}$, can be
defined as usual (cf., e.g., Def. B.1).

To see well-definedness of $\mathrm{PQPT}$s, i.e.
$P_{\bar{q}}^{\mathbb{I},v}\in\mathcal{P}(\mathcal{H}_{\bar{q}})$, we note
that $P_{\bar{q}}^{\mathbb{I},v}$ is Hermitian and

$0_{\bar{q}}=0_{\bar{q}}\mathcal{B}_{\bar{q}}^{\mathbb{I},v}0_{\bar{q}}+0_{\bar{q}}I_{\bar{q}}0_{\bar{q}}\sqsubseteq
P_{\bar{q}}^{\mathbb{I},v}=\mathcal{E}_{\bar{q}}^{*}(\mathcal{B}_{\bar{q}}^{\mathbb{I},v})+\mathcal{F}_{\bar{q}}^{*}(I_{\bar{q}})\sqsubseteq\big{(}\mathcal{E}_{\bar{q}}+\mathcal{F}_{\bar{q}}\big{)}^{*}(I_{\bar{q}})\sqsubseteq
I_{\bar{q}}$

The set of $\mathrm{PQPT}$s on $\bar{q}$ is denoted $\mathcal{T}(\bar{q})$. We
shall write $P_{\bar{q}}$ as $P$ if $\bar{q}$ is clear from the context.

######  Lemma 4.0 (From $\mathrm{QPRD}$s to $\mathrm{PQPT}$s).

For every $\mathrm{QPRD}$ $M\in\mathcal{P}(\mathcal{H}_{\bar{q}})$, there is a
$\mathrm{PQPT}$ $P_{\bar{q}}$ of the form
$0_{\bar{q}}\mathcal{B}_{\bar{q}}0_{\bar{q}}+\mathcal{F}_{\bar{q}}^{*}(I_{\bar{q}})=\mathcal{F}_{\bar{q}}^{*}(I_{\bar{q}})$
such that $M=P_{\bar{q}}$.

###### Proof.

By Lem. 2.1, $\mathrm{QPRD}$ $M$ has the spectral decomposition
$M=\sum_{k}a_{k}|\varphi_{k}\rangle\langle\varphi_{k}|$. Then the lemma
follows by defining $\mathcal{F}_{\bar{q}}$ as
$\mathcal{F}_{\bar{q}}\triangleq\sum_{k}\big{(}\sqrt{a_{k}}|\varphi_{k}\rangle\langle\varphi_{k}|\big{)}\diamond\big{(}\sqrt{a_{k}}|\varphi_{k}\rangle\langle\varphi_{k}|\big{)}^{\dagger}$.
∎

###### Remark 4.1.

The quantum tautology $I$, quantum absurdity $0$, quantum predicate variable
$\mathcal{X}$, and the negation $I-P$ of $\mathrm{PQPT}$ $P$ with
$\mathit{Prmt}(P)=\emptyset$ are $\mathrm{PQPT}$s of the form
$0(\mathcal{B})0+I(I)I$, $0(\mathcal{B})0+0(I)0$, $I(\mathcal{X})I+0(I)0$, and
$\mathcal{F}_{\bar{q}}^{*}(I_{\bar{q}})$ (cf. Lem. 4.2), respectively.

###### Definition 4.0 (Operations on $\mathrm{PQPT}$s).

Let $P$, $\\{P_{m}\\}_{m}$ (resp. $Q_{i},\mathcal{X}_{i}$ with $1\leq i\leq
l$) be $\mathrm{PQPT}$s on quantum variables $\bar{q}$ (resp. $\bar{q}_{i}$
s.t. $\biguplus_{1\leq i\leq l}\bar{q}_{i}$ exists), $P_{\bar{r}},P_{\bar{s}}$
$\mathrm{PQPT}$s on $\bar{r},\bar{s}$, and $\\{\mathcal{E}_{m}\\}_{m}$
$\mathrm{QOP}$s on $\bar{q}$ with $\sum_{m}\mathcal{E}_{m}\sqsubseteq
I_{\bar{q}}\diamond I_{\bar{q}}$. Define operations on $\mathrm{PQPT}$s as
follows.

(Substitution).:

$P[Q_{1}/\mathcal{X}_{1},\ldots,Q_{i}/\mathcal{X}_{i},\ldots,Q_{l}/\mathcal{X}_{l}]$
is the result of (simultaneously) substituting $Q_{i}$ for the (at most one)
occurrence of $\mathcal{X}_{i}$ in $P$ for all $1\leq i\leq l$, if

  * •:

$|\mathit{Prmt}(P)|\leq 1$ with
$\big{\\{}Q_{i}\triangleq\mathcal{E}_{\bar{q}_{i}}^{*}(\mathcal{X}_{i})+\mathcal{F}_{\bar{q}_{i}}^{*}(I_{\bar{q}_{i}})\big{\\}}_{1\leq
i\leq l}$, or

  * •:

$|\mathit{Prmt}(P)|\geq 2$ with
$\big{\\{}Q_{i}\triangleq\mathcal{E}_{\bar{q}_{i}}^{*}(\mathcal{X}_{i})\mid\mathcal{F}_{\bar{q}_{i}}^{*}(I_{\bar{q}_{i}})\big{\\}}_{1\leq
i\leq l}$.

(Conjunction).:

$P_{\bar{r}}\otimes P_{\bar{s}}$ is the quantum conjunction of $P_{\bar{r}}$
and $P_{\bar{s}}$, if

  * •:

$P_{\bar{r}}\triangleq\mathcal{E}_{\bar{r}}^{*}(\mathcal{B}_{\bar{r}})$ and
$P_{\bar{s}}\triangleq\mathcal{E}_{\bar{s}}^{*}(\mathcal{B}_{\bar{s}})$, or

  * •:

$\mathit{Prmt}(P_{\bar{r}})=\emptyset$ or
$\mathit{Prmt}(P_{\bar{s}})=\emptyset$.

(Disjunction).:

$\sum_{m}\mathcal{E}_{m}^{*}(P_{m})$ is the quantum disjunction of
$\\{P_{m}\\}_{m}$ under the exclusive case selection
$\\{\mathcal{E}_{m}\\}_{m}$, if

  * •:

$\big{\\{}\mathit{Prmt}(P_{m})\big{\\}}_{m}$ is a singleton.

######  Lemma 4.0.

$\mathrm{PQPT}$s are closed under those operations defined in Def. 4.3.

###### Proof.

By Def. 4.1, together with Lem. 2.2. ∎

###### Example 4.0 (Quantum predicate variables).

  * •

The $\mathrm{PQPT}$ $P_{q}\otimes\mathcal{X}_{r}\otimes\mathcal{X}_{s}$ can
induce, by substitution for $\mathcal{X}_{r}$ and $\mathcal{X}_{s}$, any
$\mathrm{PQPT}$ of the form $P_{q}\otimes Q_{r}\otimes R_{s}$ (no entanglement
between $r$ and $s$).

  * •

$P_{q}\otimes\mathcal{X}_{r,s}$ can produce any $\mathrm{PQPT}$ of the form
$P_{q}\otimes Q_{r,s}$ (where $Q_{r,s}$ possibly expresses an entanglement
between $r$ and $s$).

###### Example 4.0 (Modeling classical predicates).

Let quantum variable $q$ be such that $\mathcal{H}_{q}$ has the computational
basis $\\{|i\rangle\\}_{i}$ (i.e., $I_{q}=\sum_{i}|i\rangle_{q}\langle i|$).
Then the $\mathrm{PQPT}$

$\displaystyle\sum_{i}|i\rangle_{q}\langle
i|\mathcal{X}_{q}|i\rangle_{q}\langle i|$ $\displaystyle=$
$\displaystyle\sum_{i}\langle i|\mathcal{X}_{q}|i\rangle|i\rangle_{q}\langle
i|$

(By comparison, $\mathcal{X}_{q}$ has the outer product representation
$\mathcal{X}_{q}=\sum_{i,j}\langle
i|\mathcal{X}_{q}|j\rangle|i\rangle_{q}\langle j|$) can be used to simulate a
classical first-order variable $x$ over the domain $\\{(\langle
i|\mathcal{X}_{q}|i\rangle,i)\\}_{i}$, each element $i$ occurring with
probability $\langle i|\mathcal{X}_{q}|i\rangle$. Based on this, the classical
parameterized predicate $\varphi(x)$ can be simulated by $\sum_{i}\langle
i|\mathcal{X}_{q}|i\rangle|i\rangle_{q}\langle
i|\otimes\ulcorner\varphi(i)\urcorner$, where $\ulcorner\varphi(i)\urcorner$
is the $\mathrm{PQPT}$ for simulating the closed predicate $\varphi(i)$. For
illustrating examples, see, e.g., case studies.

###### Remark 4.2 (Discretization).

Every $\mathrm{PQPT}$ can be defined in a discrete space up to approximation.
To see this, it suffices to show that $\mathrm{QOP}$s can be discretized in
the sense of approximation. This is the case due to the fact that any
$\mathrm{QOP}$ can be obtained by tracing out the environmental part of a
global unitary operation, and any unitary operation can be approximated to
arbitrary accuracy by a quantum circuit composed of a (fixed) finite set of
gates, e.g. Hadamard, CNOT and $\pi/8$ (Nielsen and Chuang, 2000).

###  4.2. Parameterized orders and limits

#### Parameterized order.

In our quantum program logic, we shall use $\mathrm{PQPT}$s as pre- and post-
conditions in place of $\mathrm{QPRD}$s. In accordance with this change, the
Löwner comparison between $\mathrm{QPRD}$s will be replaced by a Löwner
ordering formula for $\mathrm{PQPT}$s, and quantum assertion theories will be
redefined so as to provide these Löwner ordering formulas.

###### Definition 4.0 (Löwner order between $\mathrm{PQPT}$s).

Let $P$ and $Q$ be $\mathrm{PQPT}$s on quantum variables $\bar{q}$. A
(legitimate) Löwner ordering formula is of the form $P\sqsubseteq Q$ or $P=Q$
with $\mathit{Prmt}(P)=\mathit{Prmt}(Q)$, and its formal semantics (i.e. truth
value) is defined as follows.

  * •

$\models_{\mathbb{I}}P\sqsubseteq Q$, if $P^{\mathbb{I},v}\sqsubseteq
Q^{\mathbb{I},v},\forall v$.

  * •

$\models_{\mathbb{I}}P=Q$, if $\models_{\mathbb{I}}P\sqsubseteq Q$ and
$\models_{\mathbb{I}}Q\sqsubseteq P$.

###### Example 4.0.

We illustrate valid (parameterized) Löwner ordering formulas by two items.

  * •

$\langle 0|\mathcal{X}|0\rangle|0\rangle\langle 0|\sqsubseteq\langle
0|\mathcal{X}|0\rangle|0\rangle\langle 0|+\langle
1|\mathcal{X}|1\rangle|1\rangle\langle 1|$;

  * •

$X|0\rangle\langle 0|\mathcal{X}|0\rangle\langle 0|X=|+\rangle\langle
0|\mathcal{X}|0\rangle\langle+|$.

###### Definition 4.0 (Quantum assertion theories).

  * •

The set of true $\sqsubseteq$-ordered $\mathrm{PQPT}$s under $\mathbb{I}$,
denoted ${\mathbb{I}}_{\mathit{\sqsubseteq}}$, is defined as

${\mathbb{I}}_{\mathit{\sqsubseteq}}\quad\triangleq\quad\bigcup_{\bar{q}}\big{\\{}P\sqsubseteq
Q\colon P,Q\in\mathcal{T}(\bar{q}),\mathit{Prmt}(P)=\mathit{Prmt}(Q),\textup{
and }\models_{\mathbb{I}}P\sqsubseteq Q\big{\\}}$

  * •

The set of true $=$-ordered $\mathrm{PQPT}$s under $\mathbb{I}$, denoted
${\mathbb{I}}_{\mathit{=}}$, is defined as

${\mathbb{I}}_{\mathit{=}}\quad\triangleq\quad\bigcup_{\bar{q}}\big{\\{}P=Q\colon
P,Q\in\mathcal{T}(\bar{q}),\mathit{Prmt}(P)=\mathit{Prmt}(Q),\textup{ and
}\models_{\mathbb{I}}P=Q\big{\\}}$

Note that ${\mathbb{I}}_{\mathit{\sqsubseteq}}$ provides all (true) formal
assertions on $\mathrm{PQPT}$s needed in this paper; in the sequel,
${\mathbb{I}}_{\mathit{=}}$, as a subset of
${\mathbb{I}}_{\mathit{\sqsubseteq}}$, can be used to reason with exact
probabilities.

######  Lemma 4.0.

Let $P\triangleq\mathcal{C}^{*}(\mathcal{B})+\mathcal{D}^{*}(I)$ and
$Q\triangleq\mathcal{E}^{*}(\mathcal{B})+\mathcal{F}^{*}(I)$ be
$\mathrm{PQPT}$s with the same base $\mathcal{B}$. Suppose that
$\mathcal{C}\sqsubseteq\mathcal{E}$ or $\mathcal{C}\sqsupset\mathcal{E}$ (i.e.
$\mathcal{C}$ and $\mathcal{E}$ are Löwner comparable). Then we have that

(1):

$\models_{\mathbb{I}}P\sqsubseteq Q$ if, and only if,

  * •:

$\mathcal{C}\sqsubseteq\mathcal{E}$ and
$\mathcal{D}^{*}(I)\sqsubseteq\mathcal{F}^{*}(I)$, or

  * •:

$\mathcal{C}\sqsupset\mathcal{E}$ and
$\mathcal{C}^{*}(I)+\mathcal{D}^{*}(I)\sqsubseteq\mathcal{E}^{*}(I)+\mathcal{F}^{*}(I)$.

(2):

$\models_{\mathbb{I}}P=Q$ if, and only if, $\mathcal{C}=\mathcal{E}$ and
$\mathcal{D}^{*}(I)=\mathcal{F}^{*}(I)$.

###### Proof.

For the proof of Stat. (1), $\mathcal{B}$ is taken to be $0$ if
$\mathcal{C}\sqsubseteq\mathcal{E}$, and $I$ otherwise. For the proof of Stat.
(2), first take $\mathcal{B}$ to be $0$; then use the fact that $\mathcal{C}$,
$\mathcal{E}$ are Löwner comparable. ∎

###### Remark 4.3.

The decision of $\models_{\mathbb{I}}P\sqsubseteq Q$ (resp.
$\models_{\mathbb{I}}P=Q$) will have to resort to positivity (resp. equality)
of super operators on separable states, which is beyond the scope of the
current paper. However, as Lem. 4.10 entails, a restricted semantics of
$P\sqsubseteq Q$ (resp. $P=Q$) independent of parameters can be defined based
on Löwner order of $\mathrm{QOP}$s and $\mathrm{QPRD}$s, in case that
$\mathcal{C}$ and $\mathcal{E}$ are comparable. In what follows, we shall
adopt the standard semantics of a Löwner ordering formula, but the restricted
semantics applies too.

#### Parameterized limits.

For the definition of necessary intermediate assertions in verifying recursive
procedures, we need to introduce the concept of the L. U. B. (i.e. upper
limit) and G. L. B. (i.e. lower limit) of an infinite sequence of
$\mathrm{PQPT}$s.

###### Definition 4.0 (The upper and lower limits).

Let $I$ and $P$ be $\mathrm{PQPT}$s, $\mathcal{E}$ and
$\\{\mathcal{E}_{n}\\}_{n\geq 0}$ $\mathrm{QOP}$s with $\forall n\geq 0.\
\mathcal{E}_{n}\sqsubseteq\mathcal{E}_{n+1}$ and
$\mathcal{E}=\lim\limits_{n\to\infty}\mathcal{E}_{n}$ (For the existence of
$\lim\limits_{n\to\infty}\mathcal{E}_{n}$, cf. Sec. 2).

  * •

Define the upper limit $\bigsqcup_{n=0}^{\infty}P_{n}$ of the sequence of
$\mathrm{PQPT}$s
$\big{\\{}P_{n}\triangleq\mathcal{E}_{n}^{*}(P)\big{\\}}_{n\geq 0}$ by

$\displaystyle\bigsqcup_{n=0}^{\infty}P_{n}$ $\displaystyle\triangleq$
$\displaystyle\lim\limits_{n\to\infty}P_{n}=\mathcal{E}^{*}(P)$

  * •

Define the lower limit $\bigsqcap_{n=0}^{\infty}Q_{n}$ of the sequence of
$\mathrm{PQPT}$s
$\big{\\{}Q_{n}\triangleq\mathcal{E}_{n}^{*}(P)+\big{(}I-\mathcal{E}_{n}^{*}(I)\big{)}\big{\\}}_{n\geq
0}$ by

$\displaystyle\bigsqcap_{n=0}^{\infty}Q_{n}$ $\displaystyle\triangleq$
$\displaystyle\lim\limits_{n\to\infty}Q_{n}=\mathcal{E}^{*}(P)+\big{(}I-\mathcal{E}^{*}(I)\big{)}$

######  Lemma 4.0 (Well-definedness of the limits).

Let $\\{P_{n}\\}_{n\geq 0}$ and $\\{Q_{n}\\}_{n\geq 0}$ be as in Def. 4.11.
Then we have that

  * •

$\\{P_{n}\\}_{n\geq 0}$ are $\mathrm{PQPT}$s with
$\models_{\mathbb{I}}P_{n}\sqsubseteq P_{n+1}$ for all $n\geq 0$ (thus denoted
$\\{P_{n}\\}_{n\geq 0}^{\sqsubseteq}$);

  * •

$\\{Q_{n}\\}_{n\geq 0}$ are $\mathrm{PQPT}$s with
$\models_{\mathbb{I}}Q_{n}\sqsupseteq Q_{n+1}$ for all $n\geq 0$ (thus denoted
$\\{Q_{n}\\}_{n\geq 0}^{\sqsupseteq}$).

###### Proof.

By Lem. 4.4 (closure of $\mathrm{PQPT}$s under disjunction), together with
Lem. 4.10. ∎

###### Remark 4.4.

We define the L. U. B. and G. L. B. of a sequence of $\mathrm{PQPT}$s as a
specialized $\mathrm{PQPT}$ (i.e. the limit of a restricted sequence of
$\mathrm{PQPT}$s), rather than directly introducing their general form into
the syntax of a $\mathrm{PQPT}$, due to the fact that the current one is
enough for the follow-up development while keeping a simple form of
$\mathrm{PQPT}$s.

###  4.3. Program correctness and expressiveness

$\mathit{wp}.(\mathbf{call}\ \mathit{proc}_{i}).P=\bigsqcup_{n=0}^{\infty}\mathit{wp}.S_{i}^{(n)}.P$ |  | $\mathit{wlp}.(\mathbf{call}\ \mathit{proc}_{i}).P=\bigsqcap_{n=0}^{\infty}\mathit{wlp}.S_{i}^{(n)}.P$
---|---|---
$\mathit{wp}.\mathbf{bot}.P=0$ |  | $\mathit{wlp}.\mathbf{bot}.P=I$
$\mathit{xp}.\mathbf{skip}.P=P$ |  | $\mathit{xp}.(q:=|0\rangle).P=\sum_{i}|i\rangle_{q}\langle 0|P|0\rangle_{q}\langle i|$
$\mathit{xp}.(\bar{q}\;{\ast}{=}\;U).P=U^{\dagger}PU$ |  | $\mathit{xp}.(S_{1};S_{2}).P=\mathit{xp}.S_{1}.(\mathit{xp}.S_{2}.P)$
$\mathit{xp}.\mathbf{if}.P=\sum_{m}M_{m}^{\dagger}(\mathit{xp}.S_{m}.P)M_{m}$
Table 3. Definition of formal weakest (liberal) preconditions —
$\mathit{xp}\in\\{\mathit{wp},\mathit{wlp}\\}$.

For now, a (legitimate) quantum partial (resp. total) correctness formula can
be defined as a quantum Hoare’s triple $\\{P\\}\,S\,\\{Q\\}$ (resp. $\langle
P\rangle\,S\,\langle Q\rangle$), where $S$ is a quantum program, and $P,Q$ are
$\mathrm{PQPT}$s with $\mathit{Prmt}(P)=\mathit{Prmt}(Q)$. Since quantum
programs can be viewed semantically as a $\mathrm{QOP}$, to define the
semantics of a quantum Hoare’s triple, we first need to define the correctness
semantics of a $\mathrm{QOP}$.

###### Definition 4.0 (Correctness of $\mathrm{QOP}$s).

Let $M$, $N$ be $\mathrm{QPRD}$s and $\mathcal{E}$ a $\mathrm{QOP}$. We say
that

(Partial correctness).:

$\mathcal{E}$ is partially correct w.r.t. precondition $M$ and postcondition
$N$, written $\\{M\\}\,\mathcal{E}\,\\{N\\}$, if

(2) $\displaystyle\mathit{tr}(M\rho)$ $\displaystyle\leq$
$\displaystyle\mathit{tr}\big{(}N\mathcal{E}(\rho)\big{)}+\big{[}\mathit{tr}(\rho)-\mathit{tr}\big{(}\mathcal{E}(\rho)\big{)}\big{]},\quad\forall\rho.$

(Total correctness).:

$\mathcal{E}$ is totally correct w.r.t. precondition $M$ and postcondition
$N$, written $\langle M\rangle\,\mathcal{E}\,\langle N\rangle$, if

(3) $\displaystyle\mathit{tr}(M\rho)$ $\displaystyle\leq$
$\displaystyle\mathit{tr}\big{(}N\mathcal{E}(\rho)\big{)},\quad\forall\rho.$

###### Remark 4.5.

Eq. (2) can be seen as a probabilistic version of the following statement: if
state $\rho$ satisfies predicate $M$, then, applying operation $\mathcal{E}$
to $\rho$, either $\mathcal{E}$ fails to terminate or the resulting state
$\mathcal{E}(\rho)$ satisfies predicate $N$; and total correctness is a
stronger version of partial correctness by guaranteeing termination once the
precondition is satisfied. For more information on classical partial and total
correctness, the reader is referred to (Francez, 1992).

As in classical Hoare logic, the notion of weakest (liberal) precondition can
be a candidate for the definition of intermediate assertions involved in
proving quantum program correctness. The semantical weakest (liberal)
preconditions (for a $\mathrm{QOP}$) can be defined as:

######  Theorem 4.14 (Quantum duality theorem).

Let $N$ be a $\mathrm{QPRD}$ and $\mathcal{E}$ a $\mathrm{QOP}$. Define the
semantical weakest (resp., liberal) precondition $\mathit{WP}(\mathcal{E},N)$
(resp., $\mathit{WLP}(\mathcal{E},N)$) of $\mathcal{E}$ w.r.t. $N$ by

  * •

$\mathit{WP}(\mathcal{E},N)\triangleq\mathcal{E}^{*}(N)$

  * •

$\mathit{WLP}(\mathcal{E},N)\triangleq I-\mathit{WP}(\mathcal{E},I-N)$

It is the case, for any $\mathrm{QPRD}$ $M$, that

(a):

$\langle M\rangle\,\mathcal{E}\,\langle N\rangle$ if, and only if,
$M\sqsubseteq\mathit{WP}(\mathcal{E},N)$; and

(b):

$\\{M\\}\,\mathcal{E}\,\\{N\\}$ if, and only if,
$M\sqsubseteq\mathit{WLP}(\mathcal{E},N)$.

###### Proof.

By Lem. 2.3, together with definition of Schrödinger-Heisenberg dual. ∎

Quantum duality theorem implies that: (a) $\mathit{WP}$ of a $\mathrm{QOP}$
can be represented by its Schrödinger-Heisenberg dual; (b) $\mathit{WP}$ and
$\mathit{WLP}$ are logically dual to each other.

######  Theorem 4.15 (Quantum expressiveness theorem).

Let quantum program $S\in\mathit{RqPL}$, and $P$ a $\mathrm{PQPT}$. Define the
formal weakest (resp. liberal) precondition $\mathit{wp}.S.P$ (resp.,
$\mathit{wlp}.S.P$) of $S$ w.r.t. $P$ in Tab. 3. It is the case that

(a):

$\models_{\mathbb{I}}\mathit{wp}.S.P=\llbracket S\rrbracket^{*}(P)$;

(b):

$\models_{\mathbb{I}}\mathit{wlp}.S.P=I-\mathit{wp}.S.(I-P)$
$\big{(}\triangleq\mathit{wp}.S.P+(I-\mathit{wp}.S.I)\big{)}$.

###### Proof.

See App. B.2. ∎

######  Lemma 4.0 (Well-definedness of $\mathit{wp}$ and $\mathit{wlp}$).

Let quantum program $S\in\mathit{RqPL}$, and $P$ a $\mathrm{PQPT}$. It is the
case that

(a):

$\models_{\mathbb{I}}\mathit{wp}.S_{i}^{(n)}.P\sqsubseteq\mathit{wp}.S_{i}^{(n+1)}.P$,
for all $n\geq 0$;

(b):

$\models_{\mathbb{I}}\mathit{wlp}.S_{i}^{(n)}.P\sqsupseteq\mathit{wlp}.S_{i}^{(n+1)}.P$,
for all $n\geq 0$.

###### Proof.

By Lems. 3.5, 4.12, and Thm. 4.15. ∎

###### Definition 4.0 (Correctness of quantum programs).

Let $P$, $Q$ be $\mathrm{PQPT}$s with $\mathit{Prmt}(P)=\mathit{Prmt}(Q)$, and
$S$ a quantum program. We say that

(Partial correctness).:

$S$ is partially correct w.r.t. precondition $P$ and postcondition $Q$ under
interpretation $\mathbb{I}$, denoted
$\models_{\mathbb{I}}\\{P\\}\,S\,\\{Q\\}$, if
$\models_{\mathbb{I}}P\sqsubseteq\mathit{wlp}.S.Q$;

(Total correctness).:

$S$ is totally correct w.r.t. precondition $P$ and postcondition $Q$ under
interpretation $\mathbb{I}$, denoted $\models_{\mathbb{I}}\langle
P\rangle\,S\,\langle Q\rangle$, if
$\models_{\mathbb{I}}P\sqsubseteq\mathit{wp}.S.Q$.

###### Remark 4.6.

Quantum duality and expressiveness theorems together entail that
$\mathit{wp}.S.Q$ (resp. $\mathit{wlp}.S.Q$) is the weakest $\mathrm{PQPT}$
$R$ s.t. $\models_{\mathbb{I}}\langle R\rangle\,S\,\langle Q\rangle$ (resp.
$\models_{\mathbb{I}}\\{R\\}\,S\,\\{Q\\}$). This justifies the well-
definedness of correctness of quantum programs (cf. Def. 4.17), which can be
seen as a parameterized extension of correctness of $\mathrm{QOP}$s (cf. Def.
4.13).

##  5\. Starting proof systems

(A Bot) |  $\\{I\\}\,\mathbf{bot}\,\\{P\\}$ (resp. $\langle 0\rangle\,\mathbf{bot}\,\langle P\rangle$) |  | (A Skip) | $\\{P\\}\,\mathbf{skip}\,\\{P\\}$
---|---|---|---|---
(A Init) | $\dfrac{\sum_{i}|i\rangle_{q}\langle i|=I_{q}}{\\{\sum_{i}|i\rangle_{q}\langle 0|P|0\rangle_{q}\langle i|\\}\,q:=|0\rangle\,\\{P\\}}$ |  | (A Unit) | $\dfrac{UU^{\dagger}=U^{\dagger}U=I_{\bar{q}}}{\\{U^{\dagger}PU\\}\,\bar{q}\;{\ast}{=}\;U\,\\{P\\}}$
(R Comp) | $\dfrac{\\{P\\}\,S_{1}\,\\{Q\\}\quad\\{Q\\}\,S_{2}\,\\{R\\}}{\\{P\\}\,S_{1};S_{2}\,\\{R\\}}$ |  | (R Case) | $\dfrac{\\{P_{m}\\}\,S_{m}\,\\{Q\\}\mbox{ \small for each }m}{\\{\sum_{m}M_{m}^{\dagger}P_{m}M_{m}\\}\,\mathbf{if}\,\\{Q\\}}$
(R Order) | $\dfrac{P\sqsubseteq P^{\prime}\quad\\{P^{\prime}\\}\,S\,\\{Q^{\prime}\\}\quad Q^{\prime}\sqsubseteq Q}{\\{P\\}\,S\,\\{Q\\}}$ |  | (R Subst) | $\dfrac{\\{P\\}\,S\,\\{Q\\}}{\\{P[R/\mathcal{X}]\\}\,S\,\\{Q[R/\mathcal{X}]\\}}$
Table 4. Base proof system $\mathit{qBS}$.

This section is devoted to presenting different axiom systems for proving
partial, total and even probabilistic correctness of recursive quantum
programs $\mathit{RqPL}$.

#### Base proof system.

The first step is to present an extension $\mathit{qBS}$ (quantum Base System)
to part of proof system $\mathit{qPD}$ of (Ying, 2011) for both partial and
total correctness of quantum base language $\mathit{qPL}$, so that we can deal
with syntactic pre- and post-conditions (i.e. $\mathrm{PQPT}$s). Every formula
of $\mathit{qBS}$ is either a legitimate quantum Hoare’s triple
$\\{P\\}\,S\,\\{Q\\}$ or $\langle P\rangle\,S\,\langle Q\rangle$ (where $P,Q$
are $\mathrm{PQPT}$s with $\mathit{Prmt}(P)=\mathit{Prmt}(Q)$), or a
legitimate Löwner ordering formula $P\sqsubseteq Q$ or $P=Q$ (where $P,Q$ are
$\mathrm{PQPT}$s with $\mathit{Prmt}(P)=\mathit{Prmt}(Q)$).

Proof system $\mathit{qBS}$ features the newly added inference rule — (R
Subst) — handling the substitution in $\mathrm{PQPT}$s, where $R$ (resp.
$\mathcal{X}$) is an arbitrary $\mathrm{PQPT}$ (resp. quantum predicate
variable), and $P[R/\mathcal{X}]$ stands for the result of simultaneously
substituting $R$ for each occurrence of $\mathcal{X}$ in $P$. For the
presentation of $\mathit{qBS}$, the reader is referred to Tab. 4.

###### Remark 5.1.

Every proof rule of $\mathit{qBS}$ except for (A Bot) is only presented in the
form of partial correctness formulas, but nevertheless, applies to proving
total correctness. To see this, we note that partial and total correctness are
distinguished by whether terminating almost surely (cf. Rem. 4.5). This
justifies why $\mathbf{bot}$ and recursive procedures need a distinguish
between partial and total correctness proof rules, because they are sources of
non-termination.

Intuition behind $\mathit{qBS}$. To see the intuition of proof rules in
$\mathit{qBS}$, we remark that

  * •

(A Bot, A Skip, A Init, A Unit) have the form
$\\{\mathit{xp}.S.P\\}\,S\,\\{P\\}$;

  * •

(R Comp, R Case, R Subst) preserve the form
$\\{\mathit{xp}.S.P\\}\,S\,\\{P\\}$ (bidirectionally);

  * •

(R Order) can be used to relax $\\{\mathit{xp}.S.P\\}\,S\,\\{P\\}$ to
$\\{Q\\}\,S\,\\{P\\}$ with $\models_{\mathbb{I}}Q\sqsubseteq\mathit{xp}.S.P$.

For the proof rule (R Case), the annotated $\mathbf{if}$-statement is
illustrated as follows.

$\\{l_{1}:P\\}\,\mathbf{if}\ \Box m\cdot
M[\bar{q}]=m\rightarrow\\{l_{2}^{m}:P_{m}\\}\,S_{m}\
\mathbf{fi}\,\\{l_{3}:Q\\}$

Fix the input $\rho$ (at program point $l_{1}$). By semantics of the
$\mathbf{if}$-statement, every post-measurement state $M_{m}\rho
M_{m}^{{\dagger}}$ (containing the probability of observing outcome $m$) will
go to the corresponding branch labeled by $l_{2}^{m}$ in which $P_{m}$ should
be satisfied and $S_{m}$ will be executed. By the Turing-Floyd-Hoare
principle, we have that

$\displaystyle\mathit{tr}(P\rho)$ $\displaystyle\leq$
$\displaystyle\sum_{m}\mathit{tr}(P_{m}M_{m}\rho M_{m}^{{\dagger}})$

Due to the arbitrariness of $\rho$, by properties of $\mathit{tr}$ and
$\sqsubseteq$, it follows that
$P\sqsubseteq\sum_{m}M_{m}^{{\dagger}}P_{m}M_{m}$. Note that after the
execution of each $S_{m}$, the program point $l_{3}$ is reached and the
attached assertion $Q$ is satisfied. By weakening $P$ to
$\sum_{m}M_{m}^{{\dagger}}P_{m}M_{m}$ and lifting the above reasoning process
into a proof rule, the inference rule (R Case) follows. Weakening $P$ to
$\sum_{m}M_{m}^{{\dagger}}P_{m}M_{m}$ guarantees that (R Case) preserves the
form $\\{\mathit{xp}.S.P\\}\,S\,\\{P\\}$ forward (i.e. compact soundness). To
make (R Case) preserve the form $\\{\mathit{xp}.S.P\\}\,S\,\\{P\\}$ backward
(i.e. compact completeness), we have to choose $P_{m}$ as
$\mathit{xp}.S_{m}.Q$ for each $m$.

#### Soundness and Completeness.

Of not only theoretical but also practical interest is the question of
soundness and completeness of proof systems presented as before or after. The
question of soundness concerns the correctness of the method, whereas the
question of completeness concerns the scope of its applicability (under what
circumstances it can be successfully applied). (For a systematic introduction
to the soundness and completeness issues of classical Hoare logic, the reader
is referred to the famous survey paper (Apt, 1981).)

For presentational convenience in what follows, assume that all formulas $F$
are legitimate quantum Hoare’s triples or Löwner ordering formulas. For sets
of formulas $A$ and $B$,

$\displaystyle A$ $\displaystyle\models_{\mathbb{I}}$ $\displaystyle B$

means that if $\models_{\mathbb{I}}A$ then $\models_{\mathbb{I}}B$, where by
$\models_{\mathbb{I}}A$ is meant that for all formulas $F$ of $A$,
$\models_{\mathbb{I}}F$. Let $T$ be a quantum assertion theory (e.g.
${\mathbb{I}}_{\mathit{\sqsubseteq}}$). For a proof system $\mathbf{H}$, e.g.
$\mathit{qPD}$, by

$\displaystyle T,A$ $\displaystyle\vdash_{\mathbf{H}}$
$\displaystyle\bigwedge_{F\in B}F$

is meant that every formula of $B$ can be deduced from $T$, $A$, or axioms of
$\mathbf{H}$ by finitely applying inference rules of $\mathbf{H}$. (We can
replace $\vdash_{\mathbf{H}}$ by $\vdash$, if $\mathbf{H}$ is clear from the
context.) Note that the assertion theory $T$ is used to provide Löwner
ordering formulas as antecedents of the inference rule (R Order). Let
$\mathbf{H}$ be for the programming language $L$. We say that

  * •

$\mathbf{H}$ is sound, if for all Hoare’s triples $F$ of $L$ with
${\mathbb{I}}_{\mathit{\sqsubseteq}}\vdash_{\mathbf{H}}F$, we have
$\models_{\mathbb{I}}F$;

  * •

$\mathbf{H}$ is (relatively) complete, if for all Hoare’s triples $F$ of $L$
with $\models_{\mathbb{I}}F$, we have
${\mathbb{I}}_{\mathit{\sqsubseteq}}\vdash_{\mathbf{H}}F$.

Note that ${\mathbb{I}}_{\mathit{\sqsubseteq}}$ provides all true Löwner
ordering formulas for (R Order), which, together with the condition of
expressiveness (cf. Subsec. 4.3), is sufficient to make $\mathbf{H}$ complete
(Cook, 1978; Bergstra and Tucker, 1982) ($\mathrm{QPRD}$s are enough for while
loops (Ying, 2011); while general recursive procedures need $\mathrm{PQPT}$s).
As with $\mathit{qPD}$, the proof system $\mathit{qBS}$ (for the base language
$\mathit{qPL}$) is sound and complete.

Not to mention it explicitly, various proof systems presented in the sequel
are sound and complete in the above sense (e.g. Lem. 5.3), except that a
compact version of soundness and completeness is introduced for exact
probabilistic reasoning (cf. Lem. 5.5). For a complete proof of these
soundness and completeness results, the reader is referred to App. D.

###### Remark 5.2.

The above discussion on soundness and completeness issues is purely
theoretical, because we adopt the assertion theory as an oracle (rather than
as a recursively axiomatizable theory), following the technical line of
classical Hoare logic (Cook, 1978). In practice, as discussed in Rem. 4.3, a
restricted Löwner comparison between $\mathrm{PQPT}$s independent of
parameters is enough to cover the correctness checking of Löwner ordering
formulas.

###  5.1. Partial correctness

$\dfrac{\\{P\\}\,\mathbf{call}\
\mathit{proc}\,\\{Q\\}\vdash_{\mathit{\mathit{qBS}}}\\{P\\}\,S\,\\{Q\\}}{\\{P\\}\,\mathbf{call}\
\mathit{proc}\,\\{Q\\}}$ (a) ($\rm{Rp}$ Rec).

$\dfrac{\big{\\{}\\{P_{i}\\}\,\mathbf{call}\
\mathit{proc}_{i}\,\\{Q_{i}\\}\big{\\}}_{1\leq i\leq
n}\vdash_{\mathit{\mathit{qBS}}}\bigwedge_{1\leq i\leq
n}\\{P_{i}\\}\,S_{i}\,\\{Q_{i}\\}}{\bigwedge_{1\leq i\leq
n}\\{P_{i}\\}\,\mathbf{call}\ \mathit{proc}_{i}\,\\{Q_{i}\\}}$ (b) ($\rm{Rp}$
gRec).

Table 5. Proof rules for partial correctness.

We are now in a position to present inference rules for proving partial
correctness of recursive procedures. We begin with the case of simple
recursion.

#### Simple recursion.

Consider first the case of simple recursion, that is that, the body $S$ of
recursive quantum procedure $\mathit{proc}$ should itself contain the re-
invocation statement $\mathbf{call}\ \mathit{proc}$, but retain the exclusion
of invoking other recursive quantum procedures. The proof rule — ($\rm{Rp}$
Rec) — for proving partial correctness of $\mathbf{call}\ \mathit{proc}$ is
shown in Tab. 5.

$\begin{array}[]{c}\\{l_{0}:P\\}\,\mathbf{call}\
\mathit{proc}\,\\{l_{1}:Q\\}\end{array}$ (a) Annotated program for
$\mathbf{call}\ \mathit{proc}$.

$\\{l_{2}:P\\}\cdots\\{l_{3}:P^{\prime}\\}\,\mathbf{call}\
\mathit{proc}\,\\{l_{4}:Q^{\prime}\\}\cdots\\{l_{5}:P^{\prime\prime}\\}\,\mathbf{call}\
\mathit{proc}\,\\{l_{6}:Q^{\prime\prime}\\}\cdots\\{l_{7}:Q\\}$ (b) Annotated
program for the body $S$.

Table 6. Intermediate assertion method — labels ($l_{0}$ \- $l_{7}$) are used
to indicate different program points; and each program point is annotated with
a $\mathrm{PQPT}$.

Intuition of (Rp Rec). To derive the correctness formula
$\\{P\\}\,\mathbf{call}\ \mathit{proc}\,\\{Q\\}$ about $\mathbf{call}\
\mathit{proc}$, it suffices to derive $\\{P\\}\,S\,\\{Q\\}$ for its body $S$
(cf. Tab. 6); since $S$ itself contains the re-invocation statement (or inner)
$\mathbf{call}\ \mathit{proc}$, it suffices to derive correctness formulas
about the inner $\mathbf{call}\ \mathit{proc}$, say
$\\{P^{\prime}\\}\,\mathbf{call}\ \mathit{proc}\,\\{Q^{\prime}\\}$; by the
Turing-Floyd-Hoare Principle, $\\{P^{\prime}\\}\,\mathbf{call}\
\mathit{proc}\,\\{Q^{\prime}\\}$ should be adapted from the premise
$\\{P\\}\,\mathbf{call}\ \mathit{proc}\,\\{Q\\}$ possibly by using (R Subst).
(In this case, data flow goes first from $l_{3}$ to $l_{0}$; and then from
$l_{1}$ to $l_{4}$. The case of $\\{P^{\prime\prime}\\}\,\mathbf{call}\
\mathit{proc}\,\\{Q^{\prime\prime}\\}$ can be analyzed similarly.) This
reveals the reason for introducing (R Subst): without it the above derivation
might not proceed as desired.

###### Example 5.0 (Counterexample, cf. App. C.1).

Let $q$ be a quantum variable with $\it type(q)=\mathbf{Int}$. We define the
$(+i)$-operator $U_{+i}$ over the computational basis of $\mathcal{H}_{q}$ by

$U_{+i}\colon|x\rangle\rightarrow|x+i\rangle$

and similarly for the $(-i)$-operator $U_{-i}$. Declare the procedure
$\mathit{t}oy$ by

$\mathbf{Proc}\ \langle\mathit{t}oy\rangle\colon\mathbf{if}\ \Box m\cdot
M[q]=m\rightarrow S_{m}\ \mathbf{fi}$

with $M\triangleq\big{\\{}M_{0}=\sum_{i\leq 0}|i\rangle\langle i|,\
M_{1}=\sum_{i\geq 1}|i\rangle\langle i|\big{\\}}$ and $\\{S_{m}\\}_{m=0,1}$
defined by

$S_{0}\triangleq\mathbf{skip},\quad S_{1}\triangleq q\;{\ast}{=}\;U_{-1};\
\mathbf{call}\ \mathit{t}oy;\ q\;{\ast}{=}\;U_{+1}$

Fix $n\geq 0$. We can derive the partial correctness formula

$\\{|n\rangle_{q}\langle n|\\}\,\mathbf{call}\
\mathit{t}oy\,\\{|n\rangle_{q}\langle n|\\}$

by using ($\rm{Rp}$ Rec). However, this is not the case if the use of (R
Subst) is disallowed.

#### General recursion.

We now extend (Rp Rec) for simple recursion to the general case. For (mutual)
recursive procedures $\mathit{proc}_{i}$ with body $S_{i}$, $1\leq i\leq n$,
the inference rule (Rp gRec) is introduced to prove their partial correctness
in a simultaneous way (cf. Tab. 5).

###### Remark 5.3.

Suppose that the procedure $\mathit{proc}$ with body $S$ has no re-invocation,
then the inference rule (Rp Rec) will be degenerated to

$\mbox{(R Proc)}\quad\dfrac{\\{P\\}\,S\,\\{Q\\}}{\\{P\\}\,\mathbf{call}\
\mathit{proc}\,\\{Q\\}}$

which is precisely the inference rule for non-recursive procedures. In other
words, the proof rule (R Proc) for non-recursive procedures is a special case
of (Rp Rec) for recursive procedures. Also, the proof rule (Rp Rec) for simple
recursion can be seen as a special case of (Rp gRec) for general recursion, if
the index variable $i$ is required to range over a singleton.

#### Synthesis of recursive invariants.

When proof rule (Rp gRec) is successfully applied to proving partial
correctness formula $\\{P_{i}\\}\,\mathbf{call}\
\mathit{proc}_{i}\,\\{Q_{i}\\}$ for recursive procedures $\mathit{proc}_{i}$,
$1\leq i\leq n$, we call $(P_{i},Q_{i})$ a recursive invariant of
$\mathit{proc}_{i}$, where $\mathrm{PQPT}$ $P_{i}$ can be replaced by
$\mathit{wlp}.(\mathbf{call}\ \mathit{proc}_{i}).Q_{i}$ (cf. Tab. 3), which
has the following form

$\displaystyle\mathit{wlp}.(\mathbf{call}\ \mathit{proc}_{i}).Q_{i}$
$\displaystyle=$ $\displaystyle\llbracket\mathbf{call}\
\mathit{proc}_{i}\rrbracket^{*}(Q_{i})+\big{(}I-\llbracket\mathbf{call}\
\mathit{proc}_{i}\rrbracket^{*}(I)\big{)}$

where $\big{\\{}\llbracket\mathbf{call}\
\mathit{proc}_{i}\rrbracket\big{\\}}_{1\leq i\leq n}$ is the least fixed point
of $\mathcal{F}$ (cf. Rem. 3.3 and Thm. 4.15). However, $\mathrm{PQPT}$
$Q_{i}$ sometimes should be parameterized, and the substitution for parameters
will highly depend on $\mathit{proc}_{i}$ itself (cf. Exm. 5.1), which means
that there is no uniform characterization, say fixed-point characterization,
for the recursive invariant $\big{(}\mathit{wlp}.(\mathbf{call}\
\mathit{proc}_{i}).Q_{i},Q_{i}\big{)}$. In other words, the synthesis of
recursive invariants is generally not purely automatic, yet
$\mathit{wlp}.(\mathbf{call}\ \mathit{proc}_{i}).Q_{i}$ can be automatically
synthesised provided $Q_{i}$ is given.

#### The scope of applicability.

Recalling the semantical base of a partial-correctness formula, i.e. Eq. (2)
in Def. 4.13, one can see that it is a straightforward extension of classical
partial-correctness semantics for deterministic programs. Thus, (Rp gRec) is
applicable to reasoning about programs with “deterministic control and quantum
data”. For this purpose, we typically use quantum variables to model classical
variables, i.e. encode classical values as states of a computational basis.
See, e.g., case studies.

On the other hand, our programming language should include nondeterministic
quantum programs (i.e. those branched by non-deterministic quantum
observations), where each nondeterministic branch is associated with an exact
probability (encoded into states). For these quantum programs (with
“probabilistic control and quantum data”), we need to do reasoning with exact
probability, say, given a precondition, with what probability a program will
output a particular state (or a particular class of states) or terminate?
E.g., quantum program $\mathrm{RQMC}$ on any input always outputs $|+\rangle$
with probability $\frac{1}{3}$ (cf. Exm. 3.6), i.e.

(4) $\displaystyle\forall\rho.\ \mathit{tr}(I\rho)=1$ $\displaystyle\implies$
$\displaystyle\mathit{tr}\big{(}|+\rangle\langle+|\llbracket\mathrm{RQMC}\rrbracket(\rho)\big{)}=\frac{1}{3}$

Unfortunately, interfered by probability of nontermination, i.e.
$\mathit{tr}(\rho)-\mathit{tr}\big{(}\llbracket\mathrm{RQMC}\rrbracket(\rho)\big{)}$,
partial-correctness semantics fails to fully express Ass. (4). Therefore, (Rp
gRec) is not very suitable for reasoning about programs with “probabilistic
control and quantum data”.

###  5.2. Total correctness

$\dfrac{\begin{array}[]{c}\exists\ \\{P_{n}\\}_{n\geq 0}^{\sqsubseteq}\mbox{
with }P_{0}=0\mbox{ s.t.}\\\ \langle P_{n}\rangle\,\mathbf{call}\
\mathit{proc}\,\langle Q\rangle\vdash_{\mathit{\mathit{qBS}}}\langle
P_{n+1}\rangle\,S\,\langle Q\rangle\mbox{ for all }n\geq 0,\\\
P\sqsubseteq\bigsqcup_{n=0}^{\infty}P_{n}\end{array}}{\langle
P\rangle\,\mathbf{call}\ \mathit{proc}\,\langle Q\rangle}$ (a) ($\rm{Rt}$
Rec).

$\dfrac{\begin{array}[]{c}\mbox{for }1\leq i\leq n,\ \exists\
\\{P_{i}^{j}\\}_{j\geq 0}^{\sqsubseteq}\mbox{ with }P_{i}^{0}=0\mbox{ s.t.}\\\
\big{\\{}\langle P_{i}^{j}\rangle\,\mathbf{call}\ \mathit{proc}_{i}\,\langle
Q_{i}\rangle\big{\\}}_{1\leq i\leq
n}\vdash_{\mathit{\mathit{qBS}}}\bigwedge_{1\leq i\leq n}\langle
P_{i}^{j+1}\rangle\,S_{i}\,\langle Q_{i}\rangle\mbox{ for all }j\geq 0,\\\
P_{i}\sqsubseteq\bigsqcup_{j=0}^{\infty}P_{i}^{j}\end{array}}{\bigwedge_{1\leq
i\leq n}\langle P_{i}\rangle\,\mathbf{call}\ \mathit{proc}_{i}\,\langle
Q_{i}\rangle}$ (b) ($\rm{Rt}$ gRec).

Table 7. Proof rules for total correctness.

We are now positioned to present inference rules for proving total correctness
of recursive procedures. To begin with, recall from Lem. 4.12 that
$\\{P_{n}\\}_{n\geq 0}^{\sqsubseteq}$ is an increasing sequence of
$\mathrm{PQPT}$s (ordered by $\sqsubseteq$) defined by
$\big{\\{}P_{n}\triangleq\mathcal{E}_{n}^{*}(R)\big{\\}}_{n\geq 0}$, where $R$
is a $\mathrm{PQPT}$ and $\\{\mathcal{E}_{n}\\}_{n\geq 0}$ is an increasing
sequence of $\mathrm{QOP}$s (also ordered by $\sqsubseteq$).

#### Simple recursion.

To deal with the termination problem of recursive procedure $\mathit{proc}$
(cf. Tab. 6), introduce a sequence of $\mathrm{PQPT}$s $\\{P_{n}\\}_{n\geq
0}^{\sqsubseteq}$ with $P_{0}=0$. Intuitively, if the entry point of
$\mathit{proc}$ (say $l_{0}$) is attached currently with assertion $P_{n+1}$,
then, upon re-invocation in the body $S$ of $\mathit{proc}$, the data flow at
entry points of inner $\mathbf{call}\ \mathit{proc}$ (e.g., $l_{3}$ or
$l_{5}$) needs to be constrained by a stronger assertion, namely $P_{n}$, or
its substitution by using (R Subst). Finally, to cease re-invocation, i.e.
treating inner $\mathbf{call}\ \mathit{proc}$ as $\mathbf{bot}$, the attached
assertion at entry points should be $0$, namely $P_{0}$. Combining this idea
with (Rp Rec), we thus obtain the inference rule (Rt Rec) for proving total
correctness of $\mathbf{call}\ \mathit{proc}$ (cf. Tab. 7).

###### Example 5.0 (Counterexample, cf. App. C.2).

Let the recursive procedure $\mathit{t}oy$ be as defined in Exm. 5.1. Fix
$n\geq 0$. We can derive the total correctness formula

$\langle|n\rangle_{q}\langle n|\rangle\,\mathbf{call}\
\mathit{t}oy\,\langle|n\rangle_{q}\langle n|\rangle$

by using (Rt Rec). However, this is not the case if the use of (R Subst) is
disallowed.

#### General recursion.

We now extend the (Rt Rec) for simple recursion to the general case. For
recursive procedures $\mathit{proc}_{i}$ with body $S_{i}$, $1\leq i\leq n$,
the inference rule (Rt gRec) is introduced to simultaneously prove their total
correctness (cf. Tab. 7). Note that (Rt Rec) can be seen as a special case of
(Rt gRec), if the index $i$ is required to range over a singleton.

###### Remark 5.4.

In applications, sequences of $\mathrm{PQPT}$s
$\\{P_{i}^{j}\\}^{\sqsubseteq}_{j\geq 0}$ with $P_{i}^{0}=0$ in (Rt gRec) (or,
equivalently, sequences of $\mathrm{QOP}$s
$\\{\mathcal{E}_{i}^{j}\\}^{\sqsubseteq}_{j\geq 0}$ with
$\mathcal{E}_{i}^{0}=0\diamond 0$, cf. Lem. 4.12) usually have a closed form
with $j$ as an (index) variable or are defined by induction on $j$, thus the
statement

$\displaystyle\big{\\{}\big{\langle}P_{i}^{j}\big{\rangle}\,\mathbf{call}\
\mathit{proc}_{i}\,\big{\langle}Q_{i}\big{\rangle}\big{\\}}_{1\leq i\leq n}$
$\displaystyle\vdash_{\mathit{\mathit{qBS}}}$ $\displaystyle\bigwedge_{1\leq
i\leq
n}\big{\langle}P_{i}^{j+1}\big{\rangle}\,S_{i}\,\big{\langle}Q_{i}\big{\rangle},\quad\mbox{
for all }j\geq 0$

can be proved either for one pass by treating $j$ as an arbitrary (but fixed)
variable, or for two passes by induction on $j$ (one for the basis and the
other for the inductive step).

#### Synthesis of intermediate assertions.

To make (Rt gRec) be successfully applied to proving total correctness of
recursive procedures $\mathit{proc}_{i}$, $1\leq i\leq n$, we need to provide
the intermediate assertions $\\{P_{i}^{j}\\}_{j\geq 0}^{\sqsubseteq}$ and
$Q_{i}$ involved. To this end, $P_{i}^{j}$ can be replaced by
$\mathit{wp}.S_{i}^{(j)}.Q_{i}$ (in this case $P_{i}$ can be selected as
$\mathit{wp}.(\mathbf{call}\ \mathit{proc}_{i}).Q_{i}$), which has the
following form

$\displaystyle\mathit{wp}.S_{i}^{(j)}.Q_{i}$ $\displaystyle=$
$\displaystyle\llbracket S_{i}^{(j)}\rrbracket^{*}(Q_{i})$

where $\big{\\{}\llbracket S_{i}^{(j)}\rrbracket\big{\\}}_{j\geq 0}$ with
$1\leq i\leq n$ is the least sequence of $\mathrm{QOP}$s generated by
$\mathcal{F}$ (cf. Rem. 3.3 and Thm. 4.15). As in the case of recursive
invariants, there is no uniform (fixed-point) characterization for the
$\mathrm{PQPT}$s $\big{\\{}\mathit{wp}.S_{i}^{(j)}.Q_{i}\big{\\}}_{j\geq 0}$
and $Q_{i}$ (entailed by Exm. 5.2). Therefore, the synthesis of these
intermediate assertions is semi-automatic, that is to say that, the assertions
$\big{\\{}\mathit{wp}.S_{i}^{(j)}.Q_{i}\big{\\}}_{j\geq 0}$ can be
automatically synthesised provided that $Q_{i}$ is given.

#### The scope of applicability.

Recalling Ass. (3) in Def. 4.13, one can see that the total-correctness
semantics for quantum programs is a natural extension of classical counterpart
for deterministic programs. Thus, (Rt gRec) is applicable to reasoning about
programs with “deterministic control and quantum data”. See, for example, case
studies.

However, due to inequality in Ass. (3), this (general) version of total-
correctness semantics can merely be used for reasoning with approximate
probabilities, and thus fails to support precise probabilistic reasoning, e.g.
precisely describing Ass. (4), as in the case of partial correctness.
Fortunately, a restrictive use of (Rt gRec) applies to reasoning with exact
probabilities about programs with “probabilistic control and quantum data”. We
shall develop an axiomatic basis for (approximate or exact) probabilistic
reasoning as follows.

###  5.3. Probabilistic correctness

#### Reasoning with approximate probabilities

As discussed above, Ass. (3) can be used for the semantical basis of reasoning
with approximate probabilities. Then an axiomatic basis of the (approximate)
probabilistic correctness follows from the soundness and completeness lemma.

######  Lemma 5.0 (Soundness and completeness).

For any quantum program $S\in\mathit{RqPL}$ and any $\mathrm{PQPT}$s $P,Q$, it
is the case that

${\mathbb{I}}_{\mathit{\sqsubseteq}}\vdash\langle P\rangle\,S\,\langle
Q\rangle\mbox{ if and only if
}\models_{\mathbb{I}}P\sqsubseteq\mathit{wp}.S.Q$

###### Proof.

By Def. 4.17 and Thm. D.5. ∎

######  Theorem 5.4 (Reasoning with approximate probabilities).

For any quantum program $S\in\mathit{RqPL}$, any $\mathrm{QPRD}$s $P,Q$ and
any $\delta\in[0,1]$, it is the case that

${\mathbb{I}}_{\mathit{\sqsubseteq}}\vdash\langle\delta P\rangle\,S\,\langle
Q\rangle\mbox{ if and only if }\forall\rho.\
\mathit{tr}(P\rho)=1\implies\mathit{tr}\big{(}Q\llbracket
S\rrbracket(\rho)\big{)}\geq\delta$

###### Proof.

Contained in the proof of Thm. D.6. ∎

#### Reasoning with exact probabilities

A semantical basis of (exact) probabilistic reasoning can be adapted from Eq.
(3) with $=$ in place of $\leq$ (for approximate reasoning). Based on this,
the semantics of a total-correctness formula $\langle P\rangle\,S\,\langle
Q\rangle$ has the following property

$\models_{\mathbb{I}}\langle P\rangle\,S\,\langle Q\rangle\mbox{ if and only
if }\models_{\mathbb{I}}P=\mathit{wp}.S.Q$

To build an axiomatic basis of this (exact) probabilistic correctness, we
propose the concept of compact soundness and completeness in Lem. 5.5, and, as
a consequence, a (syntactically checkable) condition for exact probabilistic
reasoning is identified in Thm. 5.6.

######  Lemma 5.0 (Compact soundness and completeness).

For any quantum program $S\in\mathit{RqPL}$ and any $\mathrm{PQPT}$s $P,Q$, it
is the case that

${\mathbb{I}}_{\mathit{=}}\vdash\langle P\rangle\,S\,\langle Q\rangle\mbox{ if
and only if }\models_{\mathbb{I}}P=\mathit{wp}.S.Q$

###### Proof.

Contained in the proof of Thm. D.5. ∎

######  Theorem 5.6 (Reasoning with exact probabilities).

For any quantum program $S\in\mathit{RqPL}$, any $\mathrm{QPRD}$s $P,Q$ and
any $\delta\in[0,1]$, it is the case that

${\mathbb{I}}_{\mathit{=}}\vdash\langle\delta P\rangle\,S\,\langle
Q\rangle\mbox{ if and only if }\forall\rho.\
\mathit{tr}(P\rho)=1\implies\mathit{tr}\big{(}Q\llbracket
S\rrbracket(\rho)\big{)}=\delta$

###### Proof.

Contained in the proof of Thm. D.6. ∎

###### Remark 5.5.

Thm. 5.6 (resp. Thm. 5.4) establishes an axiomatic basis for reasoning with
exact (resp. approximate) probabilities. Concretely speaking, if
$\mathrm{PQPT}$s $P$ and $Q$ are chosen as projection operators, then Hoare’s
triple $\langle\delta P\rangle\,S\,\langle Q\rangle$ is able to express that
“In case the inputs of $S$ fall into the subspace $P$, the outputs will fall
into $Q$ with probability $=\delta$ (resp. $\leq\delta$)”. In particular, when
$P,Q$ are the identity operator $I$, Hoare’s triple $\langle\delta
I\rangle\,S\,\langle I\rangle$ represents termination on any input with
probability $=\delta$ (resp. $\leq\delta$); and $\langle I\rangle\,S\,\langle
I\rangle$ almost-sure termination in both cases. Note that during the
reasoning with exact probabilities, the necessary Löwner ordering formulas are
of the form $P=P^{\prime}$, provided by ${\mathbb{I}}_{\mathit{=}}$.

###### Example 5.0 (Reasoning about $\mathrm{RQMC}$ with exact probabilities).

Recall the game $\mathrm{RQMC}$ from Exms. 3.2, 3.3 and 3.6. We illustrate how
to do reasoning with exact probabilities by showing probabilistic correctness
and probabilistic termination of $\mathrm{RQMC}$.

(i) (Probabilistic correctness). To formally prove that Alice wins with
probability $\frac{1}{3}$, it suffices to prove the total correctness formula

$\Big{\langle}\frac{1}{3}I\Big{\rangle}\,\mathrm{RQMC}\,\Big{\langle}|+\rangle\langle+|\Big{\rangle}$

By (A Init, R Comp), it suffices to prove

$\Big{\langle}\frac{|0\rangle\langle 0|+|1\rangle\langle
1|}{3}\Big{\rangle}\,\mathbf{call}\
\mathit{Alice}\,\Big{\langle}|+\rangle\langle+|\Big{\rangle}\mbox{ and
}\Big{\langle}\frac{|0\rangle\langle 0|+4|1\rangle\langle
1|}{6}\Big{\rangle}\,\mathbf{call}\
\mathit{Bob}\,\Big{\langle}|+\rangle\langle+|\Big{\rangle}$

simultaneously. Defining $P_{A}^{n}$, $P_{B}^{n}$ by

$P_{A}^{n}\triangleq\Big{(}\sum_{k\geq 1}^{2k-1\leq
n}\frac{1}{4^{k}}\Big{)}|0\rangle\langle 0|+\Big{(}\sum_{k\geq 1}^{2k\leq
n}\frac{1}{4^{k}}\Big{)}|1\rangle\langle 1|,\quad
P_{B}^{n}\triangleq\frac{1}{2}P_{A}^{n-1}+\frac{1}{2}|1\rangle\langle 1|$

and $\mathit{Prem}_{A}^{n}$, $\mathit{Prem}_{B}^{n}$ by

$\mathit{Prem}_{A}^{n}\triangleq\langle P_{A}^{n}\rangle\,\mathbf{call}\
\mathit{Alice}\,\langle|+\rangle\langle+|\rangle,\quad\mathit{Prem}_{B}^{n}\triangleq\langle
P_{B}^{n}\rangle\,\mathbf{call}\
\mathit{Bob}\,\langle|+\rangle\langle+|\rangle$

by ($\rm{Rt}$ gRec), it suffices to prove, for all $n\geq 0$, that

$\displaystyle\mathit{Prem}_{A}^{n},\mathit{Prem}_{B}^{n}$
$\displaystyle\vdash$ $\displaystyle\langle P_{A}^{n+1}\rangle\,\mathbf{if}\
\Box m\cdot M[q]=m\rightarrow S_{m}\
\mathbf{fi}\,\langle|+\rangle\langle+|\rangle$
$\displaystyle\mathit{Prem}_{A}^{n},\mathit{Prem}_{B}^{n}$
$\displaystyle\vdash$ $\displaystyle\langle P_{B}^{n+1}\rangle\,\mathbf{if}\
\Box m\cdot M^{\prime}[q]=m\rightarrow S_{m}^{\prime}\
\mathbf{fi}\,\langle|+\rangle\langle+|\rangle$

The proof is done by applying (R Case) to Hoare’s triples (1-3) and (4,5)
respectively.

$\begin{array}[]{clr}(1)&\langle|0\rangle\langle
0|\rangle\,q\;{\ast}{=}\;H\,\langle|+\rangle\langle+|\rangle&\mbox{(A
Unit)}\\\ (2)&\langle P_{B}^{n}\rangle\,\mathbf{call}\
\mathit{Bob}\,\langle|+\rangle\langle+|\rangle&\mathit{Prem}_{B}^{n}\\\
(3)&\langle 0\rangle\,\mathbf{bot}\,\langle|+\rangle\langle+|\rangle&\mbox{(A
Bot)}\\\ (4)&\langle P_{A}^{n}\rangle\,\mathbf{call}\
\mathit{Alice}\,\langle|+\rangle\langle+|\rangle&\mathit{Prem}_{A}^{n}\\\
(5)&\langle|1\rangle\langle
1|\rangle\,q\;{\ast}{=}\;HX\,\langle|+\rangle\langle+|\rangle&\mbox{(A
Unit)}\end{array}$

(ii) (Probabilistic termination). To formally prove that $\mathrm{RQMC}$
terminates with probability $\frac{2}{3}$, it suffices to prove the total
correctness formula

$\Big{\langle}\frac{2}{3}I\Big{\rangle}\,\mathrm{RQMC}\,\Big{\langle}I\Big{\rangle}$

By (A Init, R Comp), it suffices to prove

$\Big{\langle}\frac{2}{3}I\Big{\rangle}\,\mathbf{call}\
\mathit{Alice}\,\Big{\langle}I\Big{\rangle}\mbox{ and
}\Big{\langle}\frac{5}{6}I\Big{\rangle}\,\mathbf{call}\
\mathit{Bob}\,\Big{\langle}I\Big{\rangle}$

simultaneously. The proof proceeds as above, by redefining $P_{A}^{n}$,
$P_{B}^{n}$ by

$P_{A}^{n}\triangleq\Big{(}\sum_{k\geq 1}^{2k-1\leq
n}\frac{1}{4^{k}}\Big{)}I+\Big{(}\sum_{k\geq 1}^{2k\leq
n}\frac{1}{4^{k}}\Big{)}I,\quad
P_{B}^{n}\triangleq\frac{1}{2}P_{A}^{n-1}+\frac{1}{2}I$

and $\mathit{Prem}_{A}^{n}$, $\mathit{Prem}_{B}^{n}$ by

$\mathit{Prem}_{A}^{n}\triangleq\langle P_{A}^{n}\rangle\,\mathbf{call}\
\mathit{Alice}\,\langle I\rangle,\quad\mathit{Prem}_{B}^{n}\triangleq\langle
P_{B}^{n}\rangle\,\mathbf{call}\ \mathit{Bob}\,\langle I\rangle$

###### Remark 5.6 (Counterexample, cf. Thm. D.3).

The proof system for partial correctness of $\mathit{RqPL}$ has no compact
soundness. To see this, suppose that $S\triangleq\mathbf{call}\
P_{\mathbf{bot}}$ (cf. Exam. 3.1), and $P,Q$ are $\mathrm{PQPT}$s with
$\models_{\mathbb{I}}P\sqsubset I$. Then, by definition of $\mathit{wlp}$ (cf.
Tab. 3), we have that

$\displaystyle\models_{\mathbb{I}}$ $\displaystyle P\sqsubset
I=\mathit{wlp}.(\mathbf{call}\ P_{\mathbf{bot}}).Q$

However, by (Rp pRec), it follows that

$\displaystyle{\mathbb{I}}_{\mathit{=}}$ $\displaystyle\vdash$
$\displaystyle\\{P\\}\,\mathbf{call}\ P_{\mathbf{bot}}\,\\{Q\\}$

This reveals that the standard intermediate assertion method for partial
correctness (i.e. the Turing-Floyd-Hoare Principle, cf. Tab. 6) can’t be used
universally for reasoning about recursive procedures with exact probabilities
(even if involving nontermination).

###  5.4. Proof rules for while loops

$\dfrac{\\{P\\}\,S\,\\{M_{0}^{{\dagger}}QM_{0}+M_{1}^{{\dagger}}PM_{1}\\}}{\\{M_{0}^{{\dagger}}QM_{0}+M_{1}^{{\dagger}}PM_{1}\\}\,\mathbf{while}\
M[\bar{q}]=1\ \mathbf{do}\ S\ \mathbf{od}\,\\{Q\\}}$ (a) ($\rm{Rp}$ Loop).

$\dfrac{\begin{array}[]{c}\exists\ \\{P_{n}\\}_{n\geq 0}^{\sqsubseteq}\mbox{
with }P_{0}=0\mbox{ s.t.}\\\ \langle P_{n+1}\rangle\,S\,\langle
M_{0}^{\dagger}QM_{0}+M_{1}^{\dagger}P_{n}M_{1}\rangle\mbox{ for all }n\geq
0,\\\ P\sqsubseteq\bigsqcup_{n=0}^{\infty}P_{n}\end{array}}{\langle
M_{0}^{\dagger}QM_{0}+M_{1}^{\dagger}PM_{1}\rangle\,\mathbf{while}\
M[\bar{q}]=1\ \mathbf{do}\ S\ \mathbf{od}\,\langle Q\rangle}$ (b) ($\rm{Rt}$
Loop).

Table 8. Proof rules for while loops.

The while-loop program $\mathbf{while}\triangleq\mathbf{while}\ M[\bar{q}]=1\
\mathbf{do}\ S\ \mathbf{od}$ with $M\triangleq\\{M_{0},M_{1}\\}$, can be
defined as a call of tail recursion $\mathbf{call}\ T_{\mathbf{while}}$, where
$T_{\mathbf{while}}$ has the body

$\displaystyle\mathbf{if}$ $\displaystyle\triangleq$
$\displaystyle\mathbf{if}\ \Box m\cdot M[\bar{q}]=m\rightarrow S_{m}\
\mathbf{fi},$

with $S_{0}\triangleq\mathbf{skip}$ and $S_{1}\triangleq S;\mathbf{call}\
T_{\mathbf{while}}$.

Partial correctness. To derive $\\{R\\}\,\mathbf{call}\
T_{\mathbf{while}}\,\\{Q\\}$, by ($\rm{Rp}$ Rec), it suffices to show

$\displaystyle\\{R\\}\,\mathbf{call}\ T_{\mathbf{while}}\,\\{Q\\}$
$\displaystyle\vdash$ $\displaystyle\\{R\\}\,\mathbf{if}\,\\{Q\\}$

By (R Case), together with (A Skip) $\\{Q\\}\,\mathbf{skip}\,\\{Q\\}$, it
suffices to show

$\displaystyle\\{R\\}\,\mathbf{call}\ T_{\mathbf{while}}\,\\{Q\\}$
$\displaystyle\vdash$ $\displaystyle\\{P\\}\,S;\mathbf{call}\
T_{\mathbf{while}}\,\\{Q\\}$

Here we let $R\triangleq M_{0}^{{\dagger}}QM_{0}+M_{1}^{{\dagger}}PM_{1}$. By
(R Comp), it suffices to derive

$\\{P\\}\,S\,\\{M_{0}^{{\dagger}}QM_{0}+M_{1}^{{\dagger}}PM_{1}\\}$

Thus, the proof rule (Rp Loop) for partial correctness of $\mathbf{while}$ is
designed in Tab. 8.

Total correctness. To prove total correctness of $\mathbf{while}$, by
($\rm{Rt}$ Rec), we need to introduce a sequence of assertions at the same
program point, in which $R=M_{0}^{{\dagger}}QM_{0}+M_{1}^{{\dagger}}PM_{1}$
lies, each with a different time point. Instead of doing so, introduce
$\\{P_{n}\\}_{n\geq 0}^{\sqsubseteq}$ with $P_{0}=0$ at the program point
where $P$ lies. (We remark that each time the data flow enters the loop body,
the assertion $P_{n}$ will be encountered; yet only after exiting the loop,
should $Q$ be met.) Thus, the proof rule ($\rm{Rt}$ Loop) for total
correctness of $\mathbf{while}$ can be designed in Tab. 8.

Ying’s rules revisited. Ying’s proof rule for partial correctness of while
loops is the same as ($\rm{Rp}$ Loop) (Ying, 2011). However, his solution to
solving the issue of termination is based on a (semantical) notion of
$(P,\epsilon)$-boundedness, where $\epsilon$ bounds the trace of the diverging
computation. If, for any $\epsilon>0$, there is a
$(M_{1}^{\dagger}QM_{1},\epsilon)$-bound function of a while loop starting in
$Q$, then the loop terminates. Thus, ($\rm{Rp}$ Loop) is used there jointly
with the above condition to prove total correctness of while loops (Ying,
2011).

###### Remark 5.7.

Illustrated by the process of deducing proof rules for while loops from those
for recursive procedures (and also by Exm. 5.7), one can see that reasoning
about a tail recursion doesn’t necessarily require (R Subst), since the
Hoare’s triple on a call statement as premise can directly provide all the
needed triples of that call statement in the body.

######  Lemma 5.0 (Cf. Props. 4.2.2 and 4.2.3 of (Ying, 2016)).

Let

$\displaystyle\mathbf{while}$ $\displaystyle\triangleq$
$\displaystyle\mathbf{while}\ M[\bar{q}]=1\ \mathbf{do}\ S\ \mathbf{od}$

with $M\triangleq\\{M_{0},M_{1}\\}$, and $Q$ a (non-parameterized)
$\mathrm{PQPT}$. Define the $\mathrm{PQPT}$
$\mathcal{F}_{\mathit{xp}}^{Q}(\mathcal{X})$ by

$\displaystyle\mathcal{F}_{\mathit{xp}}^{Q}(\mathcal{X})$
$\displaystyle\triangleq$ $\displaystyle
M_{0}^{{\dagger}}QM_{0}+M_{1}^{{\dagger}}(\mathit{xp}.S.\mathcal{X})M_{1}$

where $\mathit{xp}\in\\{\mathit{wp},\mathit{wlp}\\}$. It is the case that

(i):

$\mathit{wlp}.\mathbf{while}.Q=\bigsqcap_{n=0}^{\infty}Q_{n}$, where
$Q_{0}\triangleq I$ and
$Q_{n+1}\triangleq\mathcal{F}_{\mathit{wlp}}^{Q}(Q_{n})$, for all $n\geq 0$;

(ii):

$\mathit{wp}.\mathbf{while}.Q=\bigsqcup_{n=0}^{\infty}P_{n}$, where
$P_{0}\triangleq 0$ and
$P_{n+1}\triangleq\mathcal{F}_{\mathit{wp}}^{Q}(P_{n})$, for all $n\geq 0$.

Synthesis of intermediate assertions. When applying (Rp Loop) to proving
partial correctness of a while loop, we have to provide the loop invariant
$M_{0}^{{\dagger}}QM_{0}+M_{1}^{{\dagger}}PM_{1}$, which can be selected as
$\mathit{wlp}.\mathbf{while}.Q$. Note that $\mathit{wlp}.\mathbf{while}.Q$ is
the greatest fixed point of $\mathcal{F}_{\mathit{wlp}}^{Q}(\mathcal{X})$.
Similarly, in case of applying (Rt Loop), we need to provide the intermediate
assertions $\\{P_{n}\\}_{n\geq 0}$, which can be the lease sequence of
assertions generated by $\mathcal{F}_{\mathit{wp}}^{Q}(\mathcal{X})$.

###### Example 5.0 (Almost-sure termination).

The following while loop

$\mathbf{while}\ M[q]=1\ \mathbf{do}\ \mathbf{skip}\ \mathbf{od}$

with $M\triangleq\\{M_{0}=M_{1}\triangleq\frac{1}{\sqrt{2}}I_{q}\\}$ is
abstracted from quantum random walks with absorbing boundaries (modeled by
quantum measurements) (Bach et al., 2004) and quantum Bernoulli factory for
random number generation (Dale et al., 2015). To show its almost-sure
termination, it suffices to prove the total correctness formula

$\langle I\rangle\,\mathbf{while}\ M[q]=1\ \mathbf{do}\ \mathbf{skip}\
\mathbf{od}\,\langle I\rangle$

by using (Rt Loop), where the assertions
$\\{P_{n}\triangleq\sum_{i=1}^{n}\frac{1}{2^{i}}I_{q}\\}_{n\geq 0}$ is
generated by

$\mathcal{F}_{\mathit{wp}}^{I}(\mathcal{X})=M_{0}^{{\dagger}}IM_{0}+M_{1}^{{\dagger}}(\mathit{wp}.\mathbf{skip}.\mathcal{X})M_{1}=\frac{1}{2}I_{q}+\frac{1}{2}\mathcal{X}$

###### Remark 5.8.

Observe that the necessary intermediate assertions in proving correctness of
while loops have a uniform (fixed-point) characterization, yet this is not
always the case for (non-tail) recursion. This observation, jointly with Rem.
5.7, entails that recursion is essentially more complex than while loops in
the setting of program logics.

##  6\. Expanded proof systems

$P$ | $\triangleq$ | $D;S$
---|---|---
$D$ | $\triangleq$ | $\mathbf{Proc}\ \langle\mathit{proc}\rangle(\bar{y})\colon S$
$S$ | $\triangleq$ | $\mathbf{Loc}\ \bar{q};S;\mathbf{Rel}\ \bar{q}\mid\mathbf{call}\ \langle\mathit{proc}\rangle(\bar{p})\mid\mathbf{bot}\mid\mathbf{skip}$
|  | $\mid q:=|0\rangle\mid\bar{q}\;{\ast}{=}\;U\mid S_{1};S_{2}\mid\mathbf{if}\ \Box m\cdot M[\bar{q}]=m\rightarrow S_{m}\ \mathbf{fi}$
(a) Syntax of $\mathit{eRqPL}$.

(Loc) | $\dfrac{\bar{r}\cap\mathit{Var}(\rho)=\emptyset,\ |\bar{r}|=|\bar{q}|,\ \it type(r_{i})=\it type(q_{i})\ \forall\ i}{\langle\mathbf{Loc}\ \bar{q};S;\mathbf{Rel}\ \bar{q},\rho\rangle\xrightarrow{\epsilon}\langle S[\bar{r}/\bar{q}];\mathbf{Rel}\ \bar{r},\rho\otimes|0\rangle_{\bar{r}}\langle 0|\rangle}$
---|---
(Rel) | $\dfrac{tr_{\bar{r}}\triangleq\sum_{i}\langle i|\diamond|i\rangle\mbox{ with }\sum_{i}|i\rangle\langle i|=I_{\bar{r}}}{\langle\mathbf{Rel}\ \bar{r},\rho\rangle\xrightarrow{\epsilon}\langle E,tr_{\bar{r}}(\rho)\rangle}$ |  | (Proc) | $\dfrac{\mathbf{Proc}\ \mathit{proc}(\bar{y})\colon S\in D}{\langle\mathbf{call}\ \mathit{proc}(\bar{p}),\rho\rangle\xrightarrow{\epsilon}\langle S[\bar{p}/\bar{y}],\rho\rangle}$
(b) Labeled transition rules for auxiliary facilities.

(Loc) | $\llbracket\mathbf{Loc}\ \bar{q};S;\mathbf{Rel}\ \bar{q}\rrbracket=\mathit{tr}_{\bar{r}}\circ\llbracket S[\bar{r}/\bar{q}]\rrbracket\circ(|0\rangle_{\bar{r}}\diamond\langle 0|_{\bar{r}})$
---|---
(Proc) | $\llbracket\mathbf{call}\ \mathit{proc}_{i}(\bar{a}_{i})\rrbracket=\bigsqcup_{n=0}^{\infty}\llbracket S_{i}^{(n)}[\bar{a}_{i}/\bar{y}_{i}]\rrbracket$
(c) Denotational semantics for auxiliary facilities.

$\mathit{wp}.\big{(}\mathbf{call}\ \mathit{proc}_{i}(\bar{a}_{i})\big{)}.P$ | = | $\bigsqcup_{n=0}^{\infty}\mathit{wp}.S_{i}^{(n)}[\bar{a}_{i}/\bar{y}_{i}].P$
---|---|---
$\mathit{wlp}.\big{(}\mathbf{call}\ \mathit{proc}_{i}(\bar{a}_{i})\big{)}.P$ | = | $\bigsqcap_{n=0}^{\infty}\mathit{wlp}.S_{i}^{(n)}[\bar{a}_{i}/\bar{y}_{i}].P$
$\mathit{xp}(\mathbf{Loc}\ \bar{q};S;\mathbf{Rel}\ \bar{q}).P$ | = | $\langle 0|_{\bar{r}}\big{(}\mathit{xp}.S[\bar{r}/\bar{q}].(P\otimes I_{\bar{r}})\big{)}|0\rangle_{\bar{r}}$
(d) $\mathit{wp}$ and $\mathit{wlp}$ for auxiliary facilities —
$\mathit{xp}\in\\{\mathit{wp},\mathit{wlp}\\}$.

(R Loc) | $\dfrac{\\{P\otimes I_{\bar{r}}\\}\,\bar{r}:=|0\rangle;S[\bar{r}/\bar{q}]\,\\{Q\otimes I_{\bar{r}}\\}}{\\{P\\}\,\mathbf{Loc}\ \bar{q};S;\mathbf{Rel}\ \bar{q}\,\\{Q\\}}$ |  | (R Adap) | $\dfrac{\\{P\\}\,S\,\\{Q\\}}{\\{P[\bar{p}/\bar{q}]\\}\,S[\bar{p}/\bar{q}]\,\\{Q[\bar{p}/\bar{q}]\\}}$
---|---|---|---|---
(Rp pRec) | $\dfrac{\big{\\{}\\{P_{i}\\}\,\mathbf{call}\ \mathit{proc}_{i}(\bar{y}_{i})\,\\{Q_{i}\\}\big{\\}}_{1\leq i\leq n}\vdash_{\mathit{\mathit{qBE}}}\bigwedge_{1\leq i\leq n}\\{P_{i}\\}\,S_{i}\,\\{Q_{i}\\}}{\bigwedge_{1\leq i\leq n}\\{P_{i}\\}\,\mathbf{call}\ \mathit{proc}_{i}(\bar{y}_{i})\,\\{Q_{i}\\}}$
(Rt pRec) | $\dfrac{\begin{array}[]{c}\mbox{for }1\leq i\leq n,\ \exists\ \\{P_{i}^{j}\\}_{j\geq 0}^{\sqsubseteq}\mbox{ with }P_{i}^{0}=0\mbox{ s.t.}\\\ \big{\\{}\big{\langle}P_{i}^{j}\big{\rangle}\,\mathbf{call}\ \mathit{proc}_{i}(\bar{y}_{i})\,\big{\langle}Q_{i}\big{\rangle}\big{\\}}_{1\leq i\leq n}\vdash_{\mathit{\mathit{qBE}}}\bigwedge_{1\leq i\leq n}\big{\langle}P_{i}^{j+1}\big{\rangle}\,S_{i}\,\big{\langle}Q_{i}\big{\rangle}\mbox{ for all }j\geq 0,\\\ P_{i}\sqsubseteq\bigsqcup_{j=0}^{\infty}P_{i}^{j}\end{array}}{\bigwedge_{1\leq i\leq n}\langle P_{i}\rangle\,\mathbf{call}\ \mathit{proc}_{i}(\bar{y}_{i})\,\langle Q_{i}\rangle}$
(e) Proof rules for auxiliary facilities.

Table 9. QHL for $\mathit{eRqPL}$ —
$\mathit{qBE}\triangleq\mathit{qBS}+\mbox{(R Loc)}+\mbox{(R Adap)}$.

In this section we augment the language $\mathit{RqPL}$ with facilities of
variable localization and parameter passing, with which the applicability
scope of recursive quantum programs will be broadened. This argumentation is
also in line with the spirit of $\mathrm{QPL}$ (Selinger, 2004a).

###  6.1. Quantum variable localization

#### Definition of the syntax.

The construct of variable localization allows variables whose value is
accessible only in a specified program fragment. The syntax of such a
construct with header $\mathbf{Loc}\ \langle\mathit{qvar\\_list}\rangle$, body
$S$ and tailer $\mathbf{Rel}\ \langle\mathit{qvar\\_list}\rangle$ is given by

$\mathbf{Loc}\ \langle\mathit{qvar\\_list}\rangle;\ S;\ \mathbf{Rel}\
\langle\mathit{qvar\\_list}\rangle$

###### Example 6.0 (The system-environment model of a $\mathrm{QOP}$).

The dynamics of an open quantum system (modeled by quantum variables
$\bar{q}$), interacted by a unitary interaction $U$ with an environment
(modeled by $\bar{p}$ with initial state $|0\rangle$), can be programmed as a
structure of quantum variable localization:

$\mathbf{Loc}\ \bar{p};\ (\bar{p},\bar{q})\;{\ast}{=}\;U;\ \mathbf{Rel}\
\bar{p}$

For instance, we can use this structure to program a circuit implementation
for the controlled operation $C^{n}(U)$ in Fig. 4.10 of (Nielsen and Chuang,
2000). The circuit makes use of a small number $(n-1)$ of working qubits,
which all start and end in the state $|0\rangle$.

#### Definition of the semantics.

The intended meaning of the construct of variable localization is first
expanding the state with the default value $|0\rangle$ of local variables
$\mathit{qvar\\_list}$ declared by the header, then executing the body
possibly accessing $\mathit{qvar\\_list}$, and finally releasing
$\mathit{qvar\\_list}$ by the tailer. Since the names of local variables, say
$\bar{q}$, may conflict with those of state variables outside the structure,
to define the formal semantics of variable localization, we need a reservoir
of fresh quantum variables, say $\bar{r}$ (of the same length and of the same
componentwise type as $\bar{q}$), to be used to express different instances of
the local variables before binding them to values. We can use partial trace
function, say $tr_{\mathcal{H}_{\bar{r}}}$ (abbr. $tr_{\bar{r}}$), to define
the formal semantics of quantum variable localization (cf. Tabs. 9 and 9).

#### Proof rules for the correctness.

We invent the proof rule — (R Loc) — for proving both partial and total
correctness of variable localization (cf. Tab. 9). Here, by convention,
$P\otimes I_{\bar{r}}$ and $Q\otimes I_{\bar{r}}$ can be simplified to $P$ and
$Q$ respectively.

Intuition of (R Loc). Note that $\mathbf{Loc}\ \bar{q};S;\mathbf{Rel}\
\bar{q}$ is semantically equivalent to
$\bar{r}:=|0\rangle;S[\bar{r}/\bar{q}]$, if the local variables $\bar{q}$ are
thought of as the fresh global variables $\bar{r}$. Under this assumption,
Hoare’s triple $\\{P\\}\,\mathbf{Loc}\ \bar{q};S;\mathbf{Rel}\
\bar{q}\,\\{Q\\}$ is semantically equivalent to

(5) $\\{P\otimes
I_{\bar{r}}\\}\,\bar{r}:=|0\rangle;S[\bar{r}/\bar{q}]\,\\{Q\otimes
I_{\bar{r}}\\}$

By lifting this semantical equivalence to the syntactical case, (R Loc)
follows naturally.

If, on the other hand, we choose to substitute $\bar{r}$ for $\bar{q}$ in
assertions instead of in programs, then we find that Hoare’s triple
$\\{P\\}\,\mathbf{Loc}\ \bar{q};S;\mathbf{Rel}\ \bar{q}\,\\{Q\\}$ is
semantically equivalent to

(6) $\\{P[\bar{r}/\bar{q}]\otimes|0\rangle_{\bar{q}}\langle
0|\\}\,S\,\\{Q[\bar{r}/\bar{q}]\otimes I_{\bar{q}}\\}$

By elevating this semantical deduction to an inference rule, we obtain

$\mbox{(R'
Loc)}\quad\dfrac{\\{P[\bar{r}/\bar{q}]\otimes|0\rangle_{\bar{q}}\langle
0|\\}\,S\,\\{Q[\bar{r}/\bar{q}]\otimes I_{\bar{q}}\\}}{\\{P\\}\,\mathbf{Loc}\
\bar{q};S;\mathbf{Rel}\ \bar{q}\,\\{Q\\}}$

Comparison of (R Loc) and (R’ Loc). To show the (syntactic) equivalence of the
two proof rules, it suffices to show Hoare’s triples (5) and (6) can be
transformed to each other. This is the case by using (R Adap) (cf. Tab. 9), (A
Init) and (R Order).

To see the difference of the two proof rules, we remark that (R Loc) is more
in line with the formal semantics and weakest (liberal) preconditions of
variable localization (cf. Tabs. 9 and 9), but (R’ Loc) is purely inductive
and thus more applicable in practice.

###### Example 6.0 (Grover’s search).

In Grover’s original search algorithm (cf. Chap. 6 of (Nielsen and Chuang,
2000)), we can use a (unitary) oracle $O$, defined by its action on the
computational basis:

$\displaystyle|x\rangle|y\rangle$ $\displaystyle\overset{O}{\longrightarrow}$
$\displaystyle|x\rangle|y\oplus f(x)\rangle$

to check whether an item $x$ is a solution to the search problem. Note that
$f$ is the characteristic function of the search problem, and the oracle
ancilla $|y\rangle$ is a single qubit which is flipped if $f(x)=1$, and is
unchanged otherwise. It is useful to initialize the oracle ancilla in state
$|-\rangle$, in which case the state of the ancilla is not changed, and $f(x)$
will occur as the exponent of a factor $(-1)^{f(x)}$ of relative phases. Thus
the action of the oracle can be rewritten:

$\displaystyle|\varphi\rangle\triangleq\sum_{x}\alpha_{x}|x\rangle$
$\displaystyle\overset{O}{\longrightarrow}$
$\displaystyle|\psi\rangle\triangleq\sum_{x}(-1)^{f(x)}\alpha_{x}|x\rangle$

Let quantum variables $q$, $p$ denote resp. $|x\rangle$, $|y\rangle$. The