ar
X
iv
:0
90
6.
45
86
v1
[
qu
an
t-p
h]
2
5 J
un
20
09
Hoare Logic for Quantum Programs∗
Mingsheng Ying
University of Technology, Sydney and Tsinghua University†
June 25, 2009
Abstract
Hoare logic is a foundation of axiomatic semantics of classical programs and
it provides effective proof techniques for reasoning about correctness of classical
programs. To offer similar techniques for quantum program verification and to
build a logical foundation of programmingmethodology for quantum computers,
we develop a full-fledged Hoare logic for both partial and total correctness of
quantum programs. It is proved that this logic is (relatively) complete by
exploiting the power of weakest preconditions and weakest liberal preconditions
for quantum programs.
Keywords : Quantum computation, programming language, axiomatic se-
mantics, Hoare logic, completeness
1 Introduction
Even though quantum hardware is still in its infancy, people widely believe that
building a large-scale and functional quantum computer is merely a matter of time
and concentrated effort. The history of classical computing arouses that once quan-
tum computers come into being, quantum programming languages and quantum
software development techniques will play a key role in exploiting the power of
quantum computers. With expectation of offering effective programming techniques
for quantum computers, several quantum programming languages have already been
designed in recent years. The earliest proposal for quantum programming language
was made by Knill [13]. The first real quantum programming language, QCL, was
∗This work was partly supported the National Natural Science Foundation of China (Grant No:
60736011, 60621062) and the National Key Project for Fundamental Research of China (Grant No:
2007CB807901)
†Author’s address: Mingsheng Ying, Center of Quantum Computation and Intelligent Systems,
Faculty of Engineering and Information Technology, University of Technology, Sydney, City Cam-
pus, 15 Broadway, Ultimo, NSW 2007, Australia, and State Key Laboratory of Intelligent Tech-
nology and Systems, Tsinghua National Laboratory for Information Science and Technology, De-
partment of Computer Science and Technology, Tsinghua University, Beijing 100084, China, email:
mying@it.uts.edu.au or yingmsh@tsinghua.edu.cn
1

proposed by O¨mer [16]; he also implemented a simulator for this language. A quan-
tum programming language in the style of Dijkstra’s guarded-command language,
qGCL, was presented by Sanders and Zuliani [18]. A quantum extension of C++
was proposed by Bettelli et al [6], and it was implemented in the form of a C++
library. The first and very influential quantum language of the functional program-
ming paradigm, QFC, was defined by Selinger [19] based on the idea of classical
control and quantum data. In [2], Altenkirch and Grattage defined another func-
tional programming language for quantum computing, QML, in which both control
and data may be quantum. For excellent survey of quantum programming languages,
see [20, 12].
The fact that human intuition is much better adapted to the classical world than
the quantum world is one of the major reasons that it is difficult to find efficient
quantum algorithms. It also implies that programmers will commit much more faults
in designing programs for quantum computers than programming classical comput-
ers. Thus, it is even more critical than in classical computing to give clear and
formal semantics to quantum programming languages and to provide formal meth-
ods for reasoning about quantum programs. Indeed, various semantic approaches to
quantum programs have been proposed in recent literatures. For example, an opera-
tional semantics was given to Sanders and Zuliani’s language qGCL [18] by treating
an observation (quantum measurement) procedure as a probabilistic choice; a de-
notational semantics was defined for Selinger’s language QPL [19] by interpreting
quantum programs as super-operators; and a denotational semantics of Altenkirch
and Grattage’s language QML [2] was described in category-theoretic terms. In
addition, a language-independent approach to semantics of quantum programs was
proposed by D’Hondt and Panangaden [10] who introduced an intrinsic notion of
quantum weakest precondition and established a beautiful Stone-type duality be-
tween state transition semantics and predicate transformer semantics for quantum
programs.
As to proof systems for reasoning about quantum programs, Baltag and Smets [4,
5, 1] presented a dynamic logic formalism of information flows in quantum systems,
which is capable of describing various quantum operations such as unitary evolu-
tions and quantum measurements, and particularly entanglements in multi-partite
quantum systems. Brunet and Jorrand [8] introduced a way of applying Birkhoff
and von Neumann’s quantum logic [7] to the study of quantum programs by ex-
panding the usual propositional languages with new primitives representing unitary
transformations and quantum measurements. In [9], Chadha, Mateus and Sernadas
proposed a Hoare-style proof system for reasoning about imperative quantum pro-
grams using a quantitative state logic, but only bounded iterations are allowed in
their programming language. Feng et al [11] found some useful proof rules for reason-
ing about quantum loops, generalizing some of Morgan’s proof rules for probabilistic
loops [14]. To the author’s best knowledge, however, no complete Hoare logic for
quantum programs has been reported in the literature.
The main contribution of the present paper is the establishment of a full-fledged
2

Hoare logic for deterministic quantum programs based on Selinger’s idea of model-
ing quantum programs as super-operators and D’Hondt and Panangaden’s notion of
quantum predicate as an Hermitian operator [10]. This logic includes a proof sys-
tem for partial correctness and a proof system for total correctness of deterministic
quantum programs. In particular, we are able to prove its (relative) completeness
by exploiting the power of weakest preconditions and weakest liberal preconditions
for quantum programs.
The paper is organized as follows: For convenience of the reader, we recall some
basic concepts of Hilbert spaces as well as the fundamental postulates of quantum
mechanics in Section 2. Another aim of Section 2 is to fix notation used in the sequel
sections. In Section 3, we define the syntax of deterministic quantum programs about
which the Hoare logic presented in this paper is designed to reason. Such quantum
programs are quantum extension of classical while-programs (cf. [3], Chapter 3).
In Section 4, an operational semantics of quantum programs is given in terms of
transitions between quantum configurations, which consist of a quantum program
still to be executed and a (partial) density operator expressing the current state of
program variables. In Section 5, we are able to introduce a denotational semantics
of quantum programs based on the operational semantics. A denotational semantics
of a quantum program is defined to be a function from partial density operators to
themselves. In Section 6, we adopt D’Hondt and Panangaden’s definition of quan-
tum predicates as Hermitian operators. Then a correctness formula is defined to
be a quantum extension of Hoare triple, which consists of two quantum predicates,
namely precondition and postcondition, as well as a quantum program. Further-
more, the notions of partial and total correctness can be introduced for quantum
programs using their denotational semantics. In Section 7, weakest precondition
and weakest liberal precondition for quantum programs are defined in terms of total
and partial correctness, respectively, in a familiar way. With the long preparation
of the previous sections, the Hoare logic for quantum programs is finally established
in Sections 8 and 9. In Section 8, a proof system for partial correctness of quantum
programs is presented, and its (relative) completeness is proved, and in Section 9,
after introducing the notion of bound function for quantum loops, a proof system
for total correctness of quantum programs is given, and its (relative) completeness is
also proved. A brief conclusion is drawn and some open problems for further studies
are pointed out in Section 10.
2 Preliminaries
2.1 Hilbert Spaces
We write C for the set of complex numbers. For each complex number λ ∈ C, λ∗
stands for the conjugate of λ. A (complex) vector space is a nonempty set H together
with two operations: vector addition + : H × H → H and scalar multiplication
· : C ×H → H, satisfying the following conditions:
3

1. (H,+) is an abelian group, its zero element 0 is called the zero vector;
2. 1|ϕ〉 = |ϕ〉;
3. λ(µ|ϕ〉) = λµ|ϕ〉;
4. (λ+ µ)|ϕ〉 = λ|ϕ〉 + µ|ϕ〉; and
5. λ(|ϕ〉 + |ψ〉) = λ|ϕ〉+ λ|ψ〉
for any λ, µ ∈ C and |ϕ〉, |ψ〉 ∈ H.
An inner product over a vector space H is a mapping 〈·|·〉 : H×H → C satisfying
the following properties:
1. 〈ϕ|ϕ〉 ≥ 0 with equality if and only if |ϕ〉 = 0;
2. 〈ϕ|ψ〉 = 〈ψ|ϕ〉∗; and
3. 〈ϕ|λ1ψ1 + λ2ψ2〉 = λ1〈ϕ|ψ1〉+ λ2〈ϕ|ψ2〉
for any |ϕ〉, |ψ〉, |ψ1〉, |ψ2〉 ∈ H and for any λ1, λ2 ∈ C. Sometimes, we also write
(|ϕ〉, |ψ〉) for the inner product 〈ϕ|ψ〉 of |ϕ〉 and |ψ〉.
For any vector |ψ〉 in H, its length ||ψ|| is defined to be
√
〈ψ|ψ〉. A vector |ψ〉
is called a unit vector if ||ψ|| = 1. Let {|ψn〉} be a sequence of vectors in H and
|ψ〉 ∈ H. If for any ǫ > 0, there exists a positive integer N such that ||ψm−ψn|| < ǫ
for all m,n ≥ N , then {|ψn〉} is called a Cauchy sequence. If for any ǫ > 0, there
exists a positive integer N such that ||ψn − ψ|| < ǫ for all n ≥ N , then |ψ〉 is called
a limit of {|ψn〉} and we write |ψ〉 = limn→∞ |ψn〉.
A family {|ψi〉}i∈I of vectors in H is said to be summable with the sum |ψ〉 and
we write |ψ〉 =∑i∈I |ψi〉 if for any ǫ > 0 there is a finite subset J of I such that
||ψ −
∑
i∈K
ψi|| < ǫ
for every finite subset K of I containing J . A family {|ψi〉}i∈I of unit vectors is
called an orthonormal basis of H if
1. |ψi〉 ⊥ |ψj〉 for any i, j ∈ I with i 6= j; and
2. |ψ〉 =∑i∈I〈ψi|ψ〉|ψi〉 for each |ψ〉 ∈ H.
In this case, the cardinality of I is called the dimension of H.
A Hilbert space is defined to be a complete inner product space; that is, an inner
product space in which each Cauchy sequence of vectors has a limit. According to
a basic postulate of quantum mechanics, the state space of an isolated quantum
system is represented by a Hilbert space, and a pure state of the system is described
by a unit vector in its state space.
4

Example 2.1 1. The state space of qubits is the 2−dimensional Hilbert space:
H2 = {α|0〉 + β|1〉 : α, β ∈ C}.
The inner product in H2 is defined by
(α|0〉 + β|1〉, α′|0〉+ β′|1〉 = α∗α′ + β∗β′
for all α,α′, β, β′ ∈ C. Then {|0〉, |1〉} is an orthonormal basis of H2, called
the computational basis.
2. The space l2 of square summable sequences is
H∞ = {
∞
∑
n=−∞
αn|n〉 : αn ∈ C for all n ∈ Z and
∞
∑
n=−∞
|αn|2 <∞},
where Z is the set of integers. The inner product in H∞ is defined by
(
∞
∑
n=−∞
αn|n〉,
∞
∑
n=−∞
α′|n〉) =
∞
∑
n=−∞
α∗nα′n
for all αn, α′n ∈ C, −∞ < n <∞. Then {|n〉 : n ∈ Z} is an orthonormal basis
of H∞, called the computational basis.
A (linear) operator on a Hilbert space H is a mapping A : H → H satisfying the
following conditions:
1. A(|ϕ〉 + |ψ〉) = A|ϕ〉+A|ψ〉;
2. A(λ|ψ〉) = λA|ψ〉
for all |ϕ〉, |ψ ∈ H and λ ∈ C. If {|ψi〉} is an orthonormal basis of H, then an
operator A is uniquely determined by the images {A|ψi〉} of basis vectors {|ψi〉}
under A. In particular, A can be represented by matrix
A = (〈ψi|A|ψj〉)ij
when H is finite-dimensional.
An operator A on H is said to be bounded if there is a constant C ≥ 0 such that
‖A|ψ〉‖ ≤ C ·‖ψ‖ for all |ψ〉 ∈ H. In this paper, we only consider bounded operators.
We write L(H) for the set of bounded operators on H. The identity operator on H
is denoted IH, and the zero operator on H that maps every vector in H to the zero
vector is denoted 0H.
For any operator A on H, there exists a unique linear operator A† on H such
that
(|ϕ〉, A|ψ〉) = (A†|ψ〉, |ϕ〉)
5

for all |ϕ〉, |ψ〉 ∈ H. The operator A† is called the adjoint of A. An operator M on
H is said to be Hermitian if M † = M .
An operator A on H is said to be positive if 〈ψ|A|ψ〉 ≥ 0 for all states |ψ〉 ∈ H.
We can define a partial order between operators, called the Lo¨wner partial order :
for any A,B ∈ L(H), A ⊑ B if B −A is a positive operator.
Lemma 2.1 A ⊑ B if and only if tr(Aρ) ≤ tr(Bρ) for all density operators ρ.
An operator A is said to be a trace operator if {〈ψi|A|ψi〉}i∈I is summable for
any orthonormal basis {|ψi〉}i∈I of H; in this case, the trace tr(A) of A is defined to
be
tr(A) =
∑
i
〈ψi|A|ψi〉
where {|ψi〉} is an orthonormal basis ofH. It can be shown that tr(A) is independent
of the choice of {|ψi〉}.
A density operator ρ on a Hilbert space H is defined to be a positive operator
with tr(ρ) = 1. Then a mixed state of a quantum system with state space H is
described by a density operator on H. In this paper, we take a slightly generalized
notion of density operator in the sequel: a partial density operator ρ is a positive
with tr(ρ) ≤ 1. In particular, the zero operator is a partial density operator. The
set of partial density operators is denoted D−(H). A partial density operator can
also be defined by an ensemble of pure states. Suppose that a quantum system is
in one of a number of pure states |ψi〉, with respective probabilities pi, where it is
required that
∑
i pi ≤ 1. Then
ρ =
∑
i
pi|ψi〉〈ψi|
is a density operator. Conversely, any density operator can be generated in such a
way.
2.2 Unitary Transformations
An operator U on H is called a unitary transformation if U †U = IdH, where IdH is
the identity operator on H; that is, IdH|ψ〉 = |ψ〉 for all |ψ〉 ∈ H.
Example 2.2 1. The most frequently used unitary operators on qubits are the
Hadamard transformation:
H = 1√
2
(
1 1
1 −1
)
,
and the Pauli matrices:
I =
(
1 0
0 1
)
, σx =
(
0 1
1 0
)
,
6

σy =
(
0 −i
i 0
)
, σz =
(
1 0
0 −1
)
.
2. Let k be an integer. Then the k−translation operator on H∞ is defined by
U+k|n〉 = |n+ k〉
for all n ∈ Z. It is easy to verify that U+k is a unitary operator.
The basic postulate of quantum mechanics about evolution of systems may be
stated as follows: Suppose that the states of a closed quantum system at times t0
and t are |ψ0〉 and |ψ〉, respectively. Then they are related to each other by a unitary
operator U which depends only on the times t0 and t,
|ψ〉 = U |ψ0〉.
This postulate can be reformulated in the language of density operators as follows:
The state ρ of a closed quantum system at time t is related to its state ρ0 at time
t0 by a unitary operator U which depends only on the times t and t0,
ρ = Uρ0U †.
2.3 Quantum Measurements
A quantum measurement on a system with state space H is described by a collection
{Mm} of operators on H satisfying
∑
m
M †mMm = IdH,
where Mm are called measurement operators, and the index m stands for the mea-
surement outcomes that may occur in the experiment. If the state of a quantum
system is |ψ〉 immediately before the measurement, then the probability that result
m occurs is
p(m) = 〈ψ|M †mMm|ψ〉
and the state of the system after the measurement is
|ψm〉 =
Mm|ψ〉
√
p(m)
.
We can also formulate the quantum measurement postulate in the language of den-
sity operators. If the state of a quantum system was ρ immediately before measure-
ment {Mm} is performed on it, then the probability that result m occur is
p(m) = tr(M †mMmρ),
7

and the state of the system after the measurement is
ρm =
MmρM †m
p(m) .
A special class of quantum measurements will be frequently used in the sequel:
If a measurement M has only two outcomes, say 0 and 1; that is, M = {M0,M1},
then we often call M a yes-no measurement, with 0 corresponding to “no”and 1 to
“yes”.
2.4 Tensor Products of Hilbert Spaces
The state space of a composite quantum system is the tensor product of the state
spaces of its components. In this subsection, we recall the definition of the tensor
product of a family {Hi} of Hilbert spaces. For simplicity of presentation, it will
be assumed that the set of quantum variables is countably infinite, and the type
of each quantum variable is either Boolean or integer (see next section). Thus,
we only need to consider a finite or countably infinite family {Hi} where each Hi is
finite-dimensional or countably infinite-dimensional. A more general notion of tensor
product introduced by von Neumann [21] should be adopted in order to generalize
the results obtained in this paper to the case of more quantum variables and other
types.
Let {|ψiji〉} be an orthonormal basis of Hi for each i. We write B for the set of
tensor products of basis vectors of all Hi; that is,
B = {
⊗
i
|ψiji〉}.
Then B is a countably infinite set, and it can be written in the form of a sequence
of vectors:
B = {|ϕn〉 : n = 0, 1, ...}.
The tensor product of {Hi} is defined to be the Hilbert space spanned by B, i.e.
⊗
i
Hi = {
∑
n
|ϕn〉 : αn ∈ C for all n ≥ 0 and
∑
n
|αn|2 <∞}.
We define the inner product in
⊗
iHi as follows:
(
∑
n
αn|ψn〉,
∑
n
α′n|ψn〉) =
∑
n
α∗nα′n
for any αn, α′n ∈ C, n ≥ 0. It is easy to see that
⊗
iHi is isomorphic to H∞.
The notion of partial trace is very useful for description of a subsystem of a
composite quantum system. Let H and K be two Hilbert spaces and operator
A ∈ L(H⊗K). Then the partial trace of A on H is defined to be
trK(A) =
∑
i
(IH ⊗ 〈ψi|)ρ(IH ⊗ |ψi〉),
8

which is an operator on H, where {|ψi〉} is an orthonormal basis of K. It can be
shown that trK(A) does not depend on choice of {|ψi〉}. In particular, if H1 and
H2 are the state spaces of quantum systems q1 and q2, respectively, and the state
of their composite system q1q2 is described by a density operator ρ ∈ D−(H1 ⊗H2),
then trH2(ρ) is the description for the state of component system q1.
3 Syntax of Quantum Programs
We assume a countably infinite set V ar of quantum variables. The symbols q, q′, q′′,
q0, q1, q2, ... will be used as meta-variables ranging over quantum variables. Recall
that in classical computation, we use a type to denote the domain of a variable.
Thus, in quantum computation, a type should be the state space of a quantum
system denoted by some quantum variable. Formally, a type t is a name of a Hilbert
space Ht. In this paper, we only consider two basic types: Boolean, integer. The
results obtained in this paper can be easily generalized to the case with more types.
The Hilbert spaces denoted by Boolean and integer are:
HBoolean = H2,
Hinteger = H∞.
Note that the sets denoted by types Boolean and integer in classical computation
are exactly the computational bases of HBoolean and Hinteger, respectively (see
Example 2.1). Now we assume that each quantum variable q has a type type(q),
which is either Boolean or integer. The state space Hq of a quantum variable q is
the Hilbert space denoted by its type; that is,
Hq = Htype(q).
A quantum register is defined to be a finite sequence of distinct quantum vari-
ables. The state space of a quantum register q = q1, ..., qn is the tensor product of
the state spaces of the quantum variables occurring in q; that is,
Hq =
n
⊗
i=1
Hqi .
Now we are able to define the syntax of quantum programs. The quantum pro-
grams considered in this paper are quantum extension of classical while-programs.
Formally, they are generated by the following grammar:
S ::= skip | q := 0 | q := Uq | S1;S2 | measure M [q] : S | while M [q] = 1 do S
where
• q is a quantum variable and q a quantum register;
9

• U in the statement “q := Uq”is a unitary operator on Hq. In particu-
lar, if type(q) = integer, then the statement q := U+kq, where U+k is the
k−translation operator, will be often abbreviated to q := q + k;
• in the statement “measure M [q] : S”, M = {Mm} is a measurement on the
state space Hq of q, and S = {Sm} is a set of quantum programs such that
each outcome m of measurement M corresponds to Sm;
• M = {M0,M1} in the statement “while M [q] = 1 do S”is a yes-no measure-
ment on Hq.
The intuitive meaning of these quantum program constructs will become clear
after introducing their operational semantics in the next section.
The following technical definition will be needed in the sequel.
Definition 3.1 The set var(S) of quantum variables in quantum program S is re-
cursively defined as follows:
1. If S = skip, then var(S) = ∅;
2. If S = q := 0, then var(S) = {q};
3. If S = q := Uq, then var(S) = {q};
4. If S = S1;S2, then var(S) = var(S1) ∪ var(S2);
5. If S = measure M [q] : S, then
var(S) = {q} ∪
⋃
m
var(Sm);
6. If S = while M [q] = 1 do S, then var(S) = {q} ∪ var(S).
4 Operational Semantics of Quantum Programs
We write Hall for the tensor product of the state spaces of all quantum variables,
that is,
Hall =
⊗
all q
Hq.
For simplicity of presentation, we will use E to denote the empty program. A
quantum configuration is a pair 〈S, ρ〉, where S is a quantum program or E, ρ ∈
D−(Hall) is a partial density operator on Hall, and it is used to indicate the (global)
state of quantum variables.
Let q = q1, ..., qn be a quantum register. A linear operator A on Hq has a cylinder
extension
A⊗ IV ar−{q} (1)
10

on Hall, where IV ar−{q} is the identity operator on the Hilbert space
⊗
q∈V ar−{q}
Hq.
In the sequel, we will simply for A for its extension (1), and it can be easily recognized
from the context, without any risk of confusion.
The operational semantics of quantum program is defined to be a transition
relation → between quantum configurations. By a transition
〈S, ρ〉 → 〈S′, ρ′〉
we mean that after executing quantum program S one step in state ρ, the state of
quantum variables becomes ρ′, and S′ is the remainder of S still to be executed. In
particular, if S′ = E, then S terminates in state ρ′. The transition relation → is
given by the transition rules in Fig.1.
The meanings of various program constructs are precisely specified by the tran-
sitional rules in Fig.1. The statement “skip”does nothing and terminates immedi-
ately. The initialization “q := 0”sets quantum variable q to the basis state |0〉. To see
the role of initialization more clearly, we consider the case of type(q) = integer as
an example. First, suppose ρ is a pure state; that is, ρ = |ψ〉〈ψ| for some |ψ〉 ∈ Hall.
We can write |ψ〉 in the form:
|ψ〉 =
∑
k
αk|ψk〉,
where |ψk〉 is a product state, say
|ψk〉 =
⊗
all q′
|ψkq′〉.
Then
ρ =
∑
k,l
αkα∗l |ψk〉〈ψl|.
After the initialization the state becomes:
ρq0 =
∞
∑
n=−∞
|0〉q〈n|ρ|n〉n〈0|
=
∑
k,l
αkα∗l (
∞
∑
n=−∞
|0〉q〈n|ψk〉〈ψl|n〉q〈0|)
=
∑
k,l
αkα∗l (
∞
∑
n=−∞
〈ψlq|n〉〈n|ψkq〉)(|0〉q〈0| ⊗
⊗
q′ 6=q
|ψkq′〉〈ψlq′ |)
=
∑
k,l
αkα∗l 〈ψlq|ψkq〉(|0〉q〈0| ⊗
⊗
q′ 6=q
|ψkq′〉〈ψlq′ |)
= |0〉q〈0| ⊗ (
∑
k,l
αkα∗l 〈ψlq|ψkq〉
⊗
q′ 6=q
|ψkq′〉〈ψlq′ |).
(2)
11

In general, suppose ρ is generated by an ensemble {(pi, |ψi〉)} of pure states, that is,
ρ =
∑
i
pi|ψi〉〈ψi|.
For each i, we write ρi = |ψi〉〈ψi| and assume that it becomes ρqi0 after the initial-
ization. By the above argument, we can write ρi0 in the form:
ρqi0 =
∑
k
αik(|0〉q〈0| ⊗ |ϕik〉〈ϕik|),
where |ϕik〉 ∈ Hvar−{q} for all k. Then the initialization makes that ρ becomes
ρq0 =
∞
∑
n=−∞
|0〉q〈n|ρ|n〉q〈0|
=
∑
i
pi(
∞
∑
n=−∞
|0〉q〈n|ρi|n〉q〈0|)
=
∑
i,k
piαik(|0〉q〈0| ⊗ |ϕik〉〈ϕik|).
(3)
From Eqs. (2) and (3) we see that the state of q is set to be |0〉 and the states of the
other quantum variables are unchanged. The statement “q := Uq”simply means that
unitary transformation U is performed on quantum register q, leaving the states of
the quantum variables not in q unchanged. Remark that U in the target configura-
tion of the rule (Unitary Transformation) stands indeed for the cylinder extension of
U on Hall (see Eq. (1)). A similar remark applies to the rules for measurements and
loops. Sequential composition is similar to its counterpart in classical computation.
The program construct “measure M [q] : S”is a quantum generalization of classi-
cal conditional statement. Recall that the first step of the execution of conditional
statement “if B then S1 else S2 fi”is to check whether Boolean expression B is
satisfied. However, according to a basic postulate of quantum mechanics, the unique
way to acquire information about a quantum system is to perform a measurement
on it. So, in executing the statement “measure M [q] : S”, quantum measurement
M will first be performed on quantum register q, and then a subprogram Sm in S
will be selected to be executed next according to the outcome of measurement. The
essential difference between a measurement statement and a classical conditional
statement is that the state of program variables is changed after performing the
measurement in the former, whereas it is not changed after checking the Boolean
expression in the latter. Note that the outcome m is observed with probability
pm = tr(MmρM †m),
and after the measurement the state becomes
ρm = MmρM †m/pm.
12

So, a natural presentation of the Measurement rule is the probabilistic transition:
〈measure M [q] : S, ρ〉 pm→ 〈Sm, ρm〉
However, we adopt Selinger’s suggestion [19] of encoding both probability pm and
density operator ρm into partial density operator
MmρM †m = pmρm.
This allows us to give the Measurement rule in terms of ordinary transition. The
statement “while M [q] = 1 do S”is a quantum generalization of classical loop
“while B do S od”. To acquire information about quantum register q, a measure-
ment M is performed on it. The measurement M is a yes-no measurement with
only two possible outcomes 0, 1. If the outcome 0 (no) is observed, then the pro-
gram terminates, and if the outcome 1 (yes) occurs, then the program executes the
subprogram S and continues. The only difference between a quantum loop and a
classical loop is that checking the loop guard B in a classical loop does not change
the state of program variables, but in a quantum loop the measurement outcomes 0
and 1 occur with probabilities:
p0 = tr(M0ρM †0), p1 = tr(M1ρM
†
1 ),
respectively, and the state becomes M0ρM †0 from ρ when the outcome is 0, and it
becomes M1ρM †1 when the outcome is 1. Again, we adopt Selinger’s suggestion so
that the (Loop 0) and (Loop 1) rules can be stated as ordinary transitions instead
of probabilistic transitions.
Let S be a quantum program and ρ ∈ D−(H). If 〈S′, ρ′〉 can be reached from
〈S, ρ〉 in n steps in the transition relation →; that is, there are configurations
〈S1, ρ1〉, ..., 〈Sn−1, ρn−1〉 such that
〈S, ρ〉 → 〈S1, ρ1〉 → ...→ 〈Sn−1, ρn−1〉 → 〈S′, ρ′〉,
then we write:
〈S, ρ〉 →n 〈S′, ρ′〉.
A transition sequence of S starting in ρ is a finite or infinite sequence of configura-
tions in the following form:
〈S, ρ〉 → 〈S1, ρ1〉 → ...→ 〈Sn, ρn〉 → 〈Sn+1, ρn+1〉 → ....
If it cannot be extended, then it is called a computation of S starting in ρ. Moveover,
if it is finite and its last configuration is 〈E, ρ′〉, then we say that it terminates in
ρ′; and if it is infinite, then we say that it diverges. We say that S can diverge from
ρ whenever it has a diverging computation starting in ρ.
Classical while-programs are a typical class of deterministic programs that
have exactly one computation starting in a given state. As shown in the follow-
ing example, however, quantum while-programs no longer possess such a deter-
minism because probabilism is introduced by the measurements in the statements
13

“measure M [q] : S”and “while M [q] = 1 do S”. After encoding probabilities into
partial density operators, probabilism manifests as nondeterminism in transition
rules (Measurement), (Loop 0) and (Loop 2).
Example 4.1 Suppose that type(q1) = Boolean and type(q2) = integer. Consider
the program:
S = q1 := 0; q2 := 0; q1 := Hq1; q2 := q2 + 2;measure M [q1] : S
where
• M is the measurement according to the computational basis {|0〉, |1〉} of H2;
that is, M = {M0,M1}, M0 = |0〉〈0| and M1 = |1〉〈1|;
• S = S1, S2, and
– S1 = skip;
– S2 = while N [q2] = 1 do q1 := σzq1, where N = {N0, N1},
N0 =
0
∑
n=−∞
|n〉〈n| and N1 =
∞
∑
n=1
|n〉〈n|.
Let
ρ0 =
⊗
q 6=q1,q2
|0〉q〈0|
and
ρ = |1〉q1〈1| ⊗ | − 1〉q2〈−1| ⊗ ρ0.
Then the computations of S starting in ρ are:
〈S, ρ〉 → 〈q2 := 0; q1 := Hq1; q2 := q2 + 2;measure, ρ1〉
→ 〈q1 := Hq1; q2 := q2 + 2;measure, ρ2〉
→ 〈q2 := q2 + 2;measure, ρ3〉
→ 〈measure, ρ4〉
→
{
〈S1, ρ5〉 → 〈E, ρ5〉,
〈S2, ρ6〉,
〈S2, ρ6〉 → 〈q1 := σzq1;S2, ρ6〉
→ 〈S2,−ρ6〉
→ ...
→2n−1 〈q1 := σzq1;S2, (−1)n−1ρ6〉
→ 〈S2, (−1)nρ6〉
→ ...
14

where measure stands for the statement “measure M [q1] : S”, and
ρ1 = |0〉q1〈0| ⊗ | − 1〉q2〈−1| ⊗ ρ0,
ρ2 = |0〉q1〈0| ⊗ |0〉q2〈0| ⊗ ρ0,
ρ3 = |+〉q1〈+| ⊗ |0〉q2〈0| ⊗ ρ0,
ρ4 = |+〉q1〈+| ⊗ |2〉q2〈2| ⊗ ρ0,
ρ5 =
1
2
|0〉q1〈0| ⊗ |2〉q2〈2| ⊗ ρ0,
ρ6 =
1
2
|1〉q1〈1| ⊗ |2〉q2〈2| ⊗ ρ0.
So, S can diverge from ρ. Note that S2 has also the transition
〈S2, (−1)nρ6〉 → 〈E, 0Hall〉,
but we always discard the transitions in which the partial density operator of the
target configuration is zero operator.
5 Denotational Semantics of Quantum Programs
The denotational semantics of a quantum program is defined to be a semantic func-
tion which maps partial density operators to themselves. More precisely, for any
quantum program S, the semantic function of S sums the computated results of all
terminating computations of S.
We write →∗ for the reflexive and transitive closures of →; that is, 〈S, ρ〉 →∗
〈S′, ρ′〉 if and only if 〈S, ρ〉 →n 〈S′, ρ′〉 for some n ≥ 0.
Definition 5.1 Let S be a quantum program. Then its semantic function
[|S|] : D−(Hall) → D−(Hall)
is defined by
[|S|](ρ) =
∑
{|ρ′ : 〈S, ρ〉 →∗ 〈E, ρ′〉|} (4)
for all ρ ∈ Hall.
It should be pointed out that {| · |} in Eq. (4) stands for multi-set. The reason
for using multi-sets is that the same density operator may be obtained through
different computational paths as we can see from the measurement and loop rules in
the operational semantics. The following simple example illustrates the case more
explicitly.
Example 5.1 Assume that type(q) = Boolean. Consider the program:
S = q := 0; q := Hq;measure M [q] : S,
where
15

• M is the measurement according to the computational basis {|0〉, |1〉} of H2;
• S = S0, S1, S0 = q := Iq and S1 = q := σxq.
Let ρ = |0〉all〈0|, where
|0〉all =
⊗
all q
|0〉q.
Then the computation of S starting in ρ is given as follows:
〈S, ρ〉 → 〈q := Hq;measure, ρ〉
→ 〈measure, |+〉q〈+| ⊗
⊗
q′ 6=q
|0〉q′〈0|〉
→
{
〈S0, 12 |0〉q〈0| ⊗
⊗
q′ 6=q |0〉q′〈0|〉 → 〈E, 12ρ〉,
〈S1, 12 |1〉q〈1| ⊗
⊗
q′ 6=q |0〉q′〈0|〉 → 〈E, 12ρ〉,
where measure is an abbreviation of “measure M [q] : S”. So, we have:
[|S|](ρ) = 1
2
ρ+ 1
2
ρ = ρ.
Now we are going to establish some basic properties of semantic functions. First,
we prove its linearity.
Lemma 5.1 Let ρ1, ρ2 ∈ D−(D) and λ1, λ2 ≥ 0. If λ1ρ1 + λ2ρ2 ∈ D−(D), then for
any quantum program S, we have:
[|S|](λ1ρ1 + λ2ρ2) = λ1[|S|](ρ1) + λ2[|S|](ρ2).
Proof. We can easily prove the following fact by induction on the structure of S:
• Claim: If 〈S, ρ1〉 → 〈S′, ρ′1〉 and 〈S, ρ2〉 → 〈S′, ρ′2〉, then
〈S, λ1ρ1 + λ2ρ2〉 → 〈S′, λ1ρ′1 + λ2ρ′2〉.
Then the conclusion immediately follows. 
Next we give a representation of semantic function [|S|] according to the structure
of program S. To do this for quantum loops, we need some auxiliary notations. Let
Ω be a quantum program such that [|Ω|] = 0Hall for all ρ ∈ D(H); for example,
Ω = while Mtrivial[q] = 1 do skip,
where q is a quantum variable, and
Mtrivial = {M0 = 0Hq ,M1 = IHq}
16

is a trivial measurement on Hq. We set:
(while M [q] = 1 do S)0 = Ω,
(while M [q] = 1 do S)n+1 = measure M [q] : S,
where S = S0, S1, and
S0 = skip,
S1 = S; (while M [q] = 1 do S)n
for all n ≥ 0.
Proposition 5.1 1. [|skip|](ρ) = ρ.
2. If type(q) = Boolean, then
[|q := 0|](ρ) = |0〉q〈0|ρ|0〉q〈0|+ |0〉q〈1|ρ|1〉q〈0|,
and if type(q) = integer, then
[|q := 0|](ρ)
∞
∑
n=−∞
|0〉q〈n|ρ|n〉q〈0|.
3. [|q := Uq|](ρ) = UρU †.
4. [|S1;S2|](ρ) = [|S2|]([|S1|](ρ)).
5. [|measure M [q] : S|](ρ) =∑m[|Sm|](MmρM
†
m).
6. [|while M [q] = 1 do S|](ρ) = ∨∞n=0[|(while M [q] = 1 do S)n|](ρ).
Proof. (1), (2) and (3) are obvious.
(4) By Lemma 5.1 and the transitional rule for sequential composition we obtain:
[|S2|]([|S1|](ρ)) = [|S2|](
∑
{|ρ1 : 〈S1, ρ〉 →∗ 〈E, ρ1〉|})
=
∑
{|[|S2|](ρ1) : 〈S1, ρ〉 →∗ 〈E, ρ1〉|}
=
∑
{|
∑
{|ρ′ : 〈S2, ρ1〉 →∗ 〈E, ρ′〉|} : 〈S1, ρ〉 →∗ 〈E, ρ1〉|}
=
∑
{|ρ′ : 〈S1, ρ〉 →∗ 〈E, ρ1〉 and 〈S2, ρ1〉 →∗ 〈E, ρ′〉|}
=
∑
{|ρ′ : 〈S1;S2, ρ〉 →∗ 〈E, ρ′〉|}
= [|S1;S2|](ρ).
(5) follows immediately from the transitional rule for measurement.
17

(6) We introduce two auxiliary operators:
Ei : D−(Hall) → D−(Hall),
Ei(ρ) = MiρM †i
for all ρ ∈ D−(H) and i = 0, 1. For simplicity, we write while for “while M [q] =
1 do S”. First, we prove:
[|(while)n|](ρ) =
n−1
∑
k=0
[E0 ◦ ([|S|] ◦ E1)k](ρ)
for all n ≥ 1 by induction on n. The case of n = 1 is obvious. Then by (1), (4) and
(5) and the induction hypothesis on n− 1 we obtain:
[|(while)n|](ρ) = [|skip|](E0(ρ)) + [|S; (while)n|](E1(ρ))
= E0(ρ) + [|(while)n−1|](([|S|] ◦ E1)(ρ))
= E0(ρ) +
n−2
∑
k=0
[E0 ◦ ([|S|] ◦ E1)k](([|S|] ◦ E0)(ρ))
=
n−1
∑
k=0
[E0 ◦ ([|S|] ◦ E1)k](ρ).
(5)
Second, we have:
[|while|](ρ) =
∑
{|ρ′ : 〈while, ρ〉 →∗ 〈E, ρ′〉|}
=
∞
∑
n=1
∑
{|ρ′ : 〈while, ρ〉 →n 〈E, ρ′〉|}.
So, it suffices to show that
∑
{|ρ′ : 〈while, ρ〉 →n 〈E, ρ′〉|} = [E0 ◦ ([|S|] ◦ E1)n−1](ρ)
for all n ≥ 1. This can be easily done by induction on n. 
If we only consider quantum variables of type Boolean, then the above propo-
sition coincides with Fig.1 in [11]. However, it is worth noting that in [11] the
denotational semantics of quantum programs was directly defined and it lacks a
basis of operational semantics. Similar to Lemma 3.2 in [11], we may prove that
the semantic function of a quantum program is a super-operator. Thus, the denota-
tional semantics given in this section is consistent with Selinger’s idea of modeling
quantum programs as super-operators [19].
A recursive characterization of the semantic function of a quantum loop can be
derived from the above proposition.
18

Corollary 5.1 If we write while for quantum loop “while M [q] = 1 do S”, then
for any ρ ∈ D−(Hall), it holds that
[|while|](ρ) = M0ρM †0 + [|while|]([|S|](M1ρM
†
1 )).
Proof.Immediate from Proposition 5.1(6) and Eq. (5). 
The following proposition shows that a semantic function does not increase the
trace of density operator of quantum variables.
Proposition 5.2 For any quantum program S, it holds that
tr([|S|](ρ)) ≤ tr(ρ)
for all ρ ∈ D−(Hall).
Proof. We proceed by induction on the structure of S.
Case 1. S = skip. Obvious.
Case 2. S = q := 0. If type(q) = integer, then
tr([|S|](ρ)) =
∞
∑
n=−∞
tr(|0〉q〈n|ρ|n〉n〈0|)
=
∞
∑
n=−∞
tr(q〈0|0〉q〈n|ρ|n〉q)
= tr[(
∞
∑
n=−∞
|n〉q〈n|)ρ] = tr(ρ).
It can be proved in a similar way when type(q) = Boolean.
Case 3. S = q := Uq. Then
tr([|S|](ρ) = tr(UρU †) = tr(U †Uρ) = tr(ρ).
Case 4. S = S1;S2. It follows from the induction hypothesis on S1 and S2 that
tr([|S|](ρ)) = tr([|S2|]([|S1|](ρ)))
≤ tr([|S1|](ρ))
≤ tr(ρ).
Case 5. S = measure M [q] : S. Then by induction hypothesis we obtain:
tr([|S|](ρ)) =
∑
m
tr([|Sm|](MmρM †m))
≤
∑
m
tr(MmρM †m)
= tr[(
∑
m
M †mMm)ρ]
= tr(ρ).
19

Case 6. S = whileM [q] = 1 do S′. We write (while)n for statement “(whileM [q] =
1 do S′)n”. With Proposition 5.1(6), it suffices to show that
tr([|(while)n|](ρ)) ≤ tr(ρ)
for all n ≥ 0. This can be carried out by induction on n. The case of n = 0 is
obvious. By the induction hypothesis on n and S′, we have:
tr([|(while)n+1|](ρ)) = tr(M0ρM †0 ) + tr([|(while)n|]par([|S′|](M1ρM
†
1)))
≤ tr(M0ρM †0 ) + tr([|S′|](M1ρM †1 ))
≤ tr(M0ρM †0 ) + tr(M1ρM
†
1 )
= tr[(M †0M0 +M
†
1M1)ρ]
= tr(ρ). 
From the proof of the above proposition, it is easy to see that the unique possi-
bility that tr([|S|](ρ)) < tr(ρ) comes from the quantum loops occurring in S. Thus,
tr(ρ) − tr([|S|](ρ)) is the probability that program S diverges from input state ρ.
This can be further illustrated by the following example.
Example 5.2 Let type(q) = integer, and let
M0 =
∞
∑
n=1
√
n− 1
2n (|n〉〈n|+ | − n〉〈−n|),
M1 =
∞
∑
n=1
√
n+ 1
2n (|n〉〈n|+ | − n〉〈−n|) + |0〉〈0|.
Then M = {M0,M1} is a yes-no measurement on Hq. Consider the program:
while M [q] = 1 do q := q + 1.
For simplicity, we write while for this program. Let
ρ0 =
⊗
q′ 6=q
|0〉q′〈0|
and ρ = |0〉q〈0| ⊗ ρ0. Then
[|(while)n|](ρ) =
{
0Hall if n = 0, 1, 2,
1
2(
∑n−1
k=2
k−1
k! |k〉q〈k|)⊗ ρ0 if n ≥ 3,
[|while|](ρ) = 1
2
(
∞
∑
n=2
n− 1
n! |n〉q〈n|)⊗ ρ0,
and
tr([|while|](ρ)) = 1
2
∞
∑
n=2
n− 1
n! =
1
2
.
This means that program while terminates on input ρ with probability 12 , and it
diverges from input ρ with probability 12 .
20

To conclude this section, we observe how quantum programs change the states
of quantum variables and how they access quantum variables.
Let X ⊆ V ar be a set of quantum variables. For any A ∈ L(Hall), we write
trX(A) for
trN
q∈X Hq(A).
Proposition 5.3 1. trvar(S)([|S|](ρ)) = trvar(S)(ρ).
2. If trV ar−var(S)(ρ1) = trV ar−var(S)(ρ2), then
trV ar−var(S)([|S|](ρ1)) = trV ar−var(S)([|S|](ρ2)).
We put the long and dumb proof of the above proposition into the appendix.
Recall that trX(ρ) describes the state of the quantum variables not in X when
the global state of all quantum variables is ρ. So, Proposition 5.3(1) indicates that
the state of the quantum variables not in var(S) after implementing quantum pro-
gram S is the same as that before implementing S. This means that program S
can only change the state of quantum variables in var(S). On the other hand,
Proposition 5.3(2) shows that if two input states ρ1 and ρ2 coincide on the quan-
tum variables in var(S), then the computed outcomes of S, starting in ρ1 and ρ2,
respectively, will also coincide on these quantum variables. In other words, program
S can access at most the quantum variables in var(S).
6 Correctness Formulas
Correctness of a quantum program will be expressed by a quantum extension of
Hoare triple in which a quantum predicate describes the input state and a quan-
tum predicate describes the output states of the program. We adopt D’Hondt and
Panangaden’s definition of quantum predicates [10]. For any X ⊆ V ar, a quantum
predicate on HX is defined to be a Hermitian operator P on HX such that
0HX ⊑ P ⊑ IHX .
We write P(HX) for the set of quantum predicates on HX . Intuitively, for any
ρ ∈ D−(HX), tr(Pρ) stands for the probability that predicate P is satisfied in state
ρ.
A correctness formula is a statement of the form:
{P}S{Q}
where S is a quantum program, and both P and Q are quantum predicates on Hall.
The quantum predicate P is called the precondition of the correctness formula and
Q the postcondition. A correctness formula can be interpreted in two different ways:
21

Definition 6.1 1. The correctness formula {P}S{Q} is true in the sense of total
correctness, written
|=tot {P}S{Q},
if we have:
tr(Pρ) ≤ tr(Q[|S|](ρ))
for all ρ ∈ D−(H).
2. The correctness formula {P}S{Q} is true in the sense of partial correctness,
written
|=par {P}S{Q},
if we have:
tr(Pρ) ≤ tr(Q[|S|](ρ)) + [tr(ρ)− tr([|S|](ρ))]
for all ρ ∈ D−(H).
The intuitive meaning of the defining inequality of total correctness is: the prob-
ability that input ρ satisfies quantum predicate P is not greater than the probability
that quantum program S terminates on ρ and its output [|S|](ρ) satisfies quantum
predicate Q. Recall that tr(ρ)−tr([|S|](ρ)) is the probability that quantum program
S diverges from input ρ. Thus, the definition inequality of partial correctness means:
if input ρ satisfies predicate P , then either program S terminates on it and its output
[|S|](ρ) satisfies Q, or S diverges from it. The difference between total correctness
and partial correctness is illustrated well by the following simple example.
Example 6.1 Assume that type(q) = Boolean. Consider the program:
S = while M [q] = 1 do q := σzq
where M0 = |0〉〈0| and M1 = |1〉〈1|. Let P = |ψ〉q〈ψ|⊗P ′, where |ψ〉 = α|0〉+β|1〉 ∈
H2, and P ′ ∈ P(HV ar−{q}). Then
|=tot {P}S{|0〉q〈0| ⊗ P ′}
does not hold if β 6= 0 and P 6= 0HV ar−{q}. In fact, put
ρ = |ψ〉q〈ψ| ⊗ IHV ar−{q} .
Then
[|S|](ρ) = |α|2|0〉q〈0| ⊗ IHV ar−{q}
and
tr(Pρ) = tr(P ′) > |α|2tr(P ′) = tr((|0〉q〈0| ⊗ P ′)[|S|](ρ)).
On the other hand, we always have:
|=par {P}S{|0〉q〈0| ⊗ P ′}.
22

To show this, we first consider a special class of partial density operators on HV ar−{q}:
ρ = |ϕ〉q〈ϕ| ⊗ ρ′, where |ϕ〉 = a|0〉 + b|1〉 ∈ H2, and ρ′ ∈ D−(HV ar−{q}). A routine
calculation yields:
[|S|](ρ) = |a|2|0〉q〈0| ⊗ ρ′
and
tr(Pρ) = |〈ψ|ϕ〉|2tr(P ′ρ′)
≤ |a|2tr(P ′ρ′) + [tr(ρ′)− |a|2tr(ρ′)]
= tr((|0〉q〈0| ⊗ P ′)[|S|](ρ)) + [tr(ρ)− tr([|S|](ρ))].
Then it follows from linearity of [|S|] (Lemma 5.1) that
tr(Pρ) ≤ tr((|0〉q〈0| ⊗ P ′)[|S|](ρ)) + [tr(ρ)− tr([|S|](ρ))]
for all ρ ∈ D−(Hall).
The following proposition presents some basic properties of correctness formulas.
Proposition 6.1 1. If |=tot {P}S{Q}, then |=par {P}S{Q}.
2. For any quantum program S, and for any P,Q ∈ P(Hall), we have:
|=tot {0Hall}S{Q}, |=par {P}S{IHall}.
3. Linearity: For any P1, P2, Q1, Q2 ∈ P(Hall) and λ1, λ2 ≥ 0 with λ1P1 +
λ2P2, λ1Q1 + λ2Q2 ∈ P(Hall), if
|=tot {Pi}S{Qi} (i = 1, 2),
then
|=tot {λ1P1 + λ2P2}S{λ1Q1 + λ2Q2}.
The same conclusion holds for partial correctness if λ1 + λ2 = 1.
Proof. Immediate from definition. 
7 Weakest Preconditions and Weakest Liberal Precon-
ditions
As in the case of classical Hoare logic, the notions of weakest precondition and
weakest liberal precondition of quantum program will play a key role in establishing
the (relative) completeness of Hoare logic for quantum programs. They may be
defined in a familiar way:
Definition 7.1 Let S be a quantum program and P ∈ P(Hall) be a quantum predi-
cate on Hall.
23

1. The weakest precondition of S with respect to P is defined to be the quantum
predicate wp.S.P ∈ P(Hall) satisfying the following conditions:
(a) |=tot {wp.S.P}S{P};
(b) if quantum predicate Q ∈ P(Hall) satisfies |=tot {Q}S{P} then Q ⊑
wp.S.P .
2. The weakest liberal precondition of S with respect to P is defined to be the
quantum predicate wlp.S.P ∈ P(Hall) satisfying the following conditions:
(a) |=par {wlp.S.P}S{P};
(b) if quantum predicate Q ∈ P(Hall) satisfies |=par {Q}S{P} then Q ⊑
wlp.S.P .
The next two propositions give explicit representations of weakest preconditions
and weakest liberal preconditions, respectively. They will be used in the proof of
completeness of quantum Hoare logic.
Proposition 7.1 1. (a) wp.skip.P = P.
(b) If type(q) = Boolean, then
wp.q := 0.P = |0〉q〈0|P |0〉q〈0|+ |1〉q〈0|P |0〉q〈1|,
and if type(q) = integer, then
wp.q := 0.P =
∞
∑
n=−∞
|n〉q〈0|P |0〉q〈n|.
(c) wp.q := Uq.P = U †PU .
(d) wp.S1;S2.P = wp.S1.(wp.S2.P ).
(e) wp.measure M [q] : S.P =∑mM
†
m(wp.Sm.P )Mm.
(f) wp.while M [q] = 1 do S.P = ∨∞n=0 Pn, where
{
P0 = 0Hall ,
Pn+1 = M †0PM0 +M
†
1(wp.S.Pn)M1 for all n ≥ 0.
2. For any quantum program S, for any quantum predicate P ∈ P(Hall), and for
any partial density operator ρ ∈ D−(Hall), we have:
tr((wp.S.P )ρ) = tr(P [|S|]par(ρ)).
24

Proof. The trick is to simultaneously prove (1) and (2) by induction on the
structure. This is indeed why we put these two conclusions that seem irrelevant at
the first glance into a single proposition.
Case 1. S = skip. Obvious.
Case 2. S = q := 0. We only consider the case of type(q) = integer, and the
case of type(q) = Boolean is similar. First, it holds that
tr((
∞
∑
n=−∞
|n〉q〈0|P |0〉q〈n|)ρ) = tr(P
∞
∑
n=−∞
|0〉q〈n|ρ|n〉q〈0|)
= tr(P [|q := 0|](ρ)).
On the other hand, for any quantum predicate Q ∈ P(Hall), if |=tot {Q}q := 0{P},
i.e.
tr(Qρ) ≤ tr(P [|q := 0|](ρ))
= tr((
∞
∑
n=−∞
|n〉q〈0|P |0〉q〈n|)ρ)
for all ρ ∈ D−(Hall), then it follows from Lemma 2.1 that
Q ⊑
∞
∑
n=−∞
|n〉q〈0|P |0〉q〈n|.
Case 3. S = q := Uq. Similar to Case 2.
Case 4. S = S1;S2. It follows from the induction hypothesis on S1 and S2 that
tr((wp.S1.(wp.S2.P ))ρ) = tr((wp.S2.P )[|S1|](ρ))
= tr(P [|S2|]([|S1|](ρ)))
= tr(P [|S1;S2|](ρ)).
If |=tot {Q}S1;S2{P}, then for all ρ ∈ D−(Hall), we have:
tr(QP ) ≤ tr(P [|S1;S2|](ρ)) = tr((wp.S1.(wp.S2.P ))ρ).
Therefore, it follows from Lemma 2.1 that Q ⊑ wp.S1.(wp.S2.P ).
Case 5. S = measure M [q] : S. Applying the induction hypothesis on Sm, we
obtain:
tr((
∑
m
M †m(wp.Sm.P )Mm)ρ) =
∑
m
tr((wp.Sm.P )MmρM †m)
=
∑
m
tr(P [|Sm|](MmρM †m))
= tr(P
∑
m
[|Sm|](MmρM †m))
= tr(P [|measure M [q] : S|]par(ρ)).
25

If |=tot {Q}measure M [q] : S{P}, then
tr(Qρ) ≤ tr((
∑
m
M †m(wp.Sm.P )Mm)ρ)
for all ρ, and it follows from Lemma 2.1 that
Q ⊑
∑
m
M †m(wlp.Sm.P )Mm.
Case 6. S = while M [q] = 1 do S′. For simplicity, we write (while)n for
statement “(while M [q] = 1 do S′)n”. First, we have:
tr(Pnρ) = tr(P [|(while)n|](ρ)).
This claim can be proved by induction on n. The basis case of n = 0 is obvious. By
the induction hypotheses on n and S′, we obtain:
tr(Pn+1ρ) = tr(M †0PM0ρ) + tr(M
†
1 (wp.S′.Pn)M1ρ)
= tr(PM0ρM †0 ) + tr((wp.S′.Pn)M1ρM
†
1)
= tr(PM0ρM †0 ) + tr(Pn[|S′|](M1ρM †1 ))
= tr(PM0ρM †0 ) + tr(P [|(while)n|]([|S′|]par(M1ρM †1 )))
= tr[P (M0ρM †0 + [|S′; (while)n|](M1ρM †1 ))]
= tr(P [|(while)n+1|](ρ)).
Now continuity of trace operator yields:
tr((
∞
∨
n=0
Pn)ρ) =
∞
∨
n=0
tr(Pnρ)
=
∞
∨
n=0
tr(P [|(while)n|](ρ))
= tr(P
∞
∨
n=0
[|(while)n|](ρ))
= tr(P [|while M [q] = 1 do S′|](ρ)).
So, if
|=tot {Q}while M [q] = 1 do S′{P},
then
tr(Qρ) ≤ tr((
∞
∨
n=0
Pn)ρ)
for all ρ, and by Lemma 2.1 we obtain Q ⊑ ∨∞n=0 Pn. 
26

Proposition 7.2 1. (a) wlp.skip.P = P.
(b) If type(q) = Boolean, then
wlp.q := 0.P = |0〉q〈0|P |0〉q〈0| + |1〉q〈0|P |0〉q〈1|,
and if type(q) = integer, then
wlp.q := 0.P =
∞
∑
n=−∞
|n〉q〈0|P |0〉q〈n|.
(c) wlp.q := Uq.P = U †PU .
(d) wlp.S1;S2.P = wlp.S1.(wlp.S2.P ).
(e) wlp.measure M [q] : S.P =∑mM
†
m(wlp.Sm.P )Mm.
(f) wlp.while M [q] = 1 do S.P = ∧∞n=0 Pn, where
{
P0 = IHall ,
Pn+1 = M †0PM0 +M
†
1 (wlp.S.Pn)M1 for all n ≥ 0.
2. For any quantum program S, for any quantum predicate P ∈ P(Hall), and for
any partial density operator ρ ∈ D−(Hall), we have:
tr((wlp.S.P )ρ) = tr(P [|S|]par(ρ)) + [tr(ρ)− tr([|S|](ρ)].
Proof. Similar to the case of weakest precondition, we prove (1) and (2) simul-
taneously by induction on the structure of quantum program S.
Case 1. S = skip, or q := 0, or q := Uq. Similar to Cases 1, 2 and 3 in the proof
of Proposition 7.1.
Case 2. S = S1;S2. First, with the induction hypothesis on S1 and S2, we have:
tr(wlp.S1.(wlp.S2.P )ρ) = tr(wlp.S2.P [|S1|](ρ)) + [tr(ρ)− tr([|S1|](ρ))]
= tr(P [|S2|]([|S1|](ρ)) + [tr([|S1|](ρ)) − tr([|S2|]([|S1|](ρ)))] + [tr(ρ)− tr([|S1|](ρ))]
= tr(P [|S2|]([|S1|](ρ)) + [tr(ρ)− tr([|S2|]([|S1|](ρ)))]
= tr(P [|S|](ρ)) + [tr(ρ)− tr([|S|](ρ))].
If |=par {Q}S{P}, then it holds that
tr(Qρ) ≤ tr(P [|S|](ρ)) + [tr(ρ)− tr([|S|](ρ))] = tr(wlp.S1.(wlp.S2.P )ρ)
for all ρ ∈ D−(Hall), and by Lemma 2.1 we obtain:
Q ⊑ wlp.S1.(wlp.S2.P ).
27

Case 3. S = measure M [q] : S. It can is derived by induction hypothesis on all
Sm that
tr(
∑
m
M †m(wlp.Sm.P )Mmρ) =
∑
m
tr(M †m(wlp.Sm.P )Mmρ)
=
∑
m
tr((wlp.Sm.P )MmρM †m)
=
∑
m
{tr(P [|Sm|](MmρM †m)) + [tr(MmρM †m)− tr([|Sm|](MmρM †m))]}
=
∑
m
tr(P [|Sm|](MmρM †m)) + [
∑
m
tr(MmρM †m)−
∑
m
tr([|Sm|](MmρM †m))]}
= tr(P
∑
m
[|Sm|](MmρM †m)) + [tr(ρ
∑
m
M †mMm)− tr(
∑
m
[|Sm|](MmρM †m))]}
= tr(P [|S|](ρ)) + [tr(ρ)− tr([|S|](ρ))]
because
∑
mM
†
mMm = IHq . If |=par {Q}S{P}, then for all ρ ∈ D−(Hall), it holds
that
tr(Qρ) ≤ tr(P [|S|](ρ)) + [tr(ρ)− tr([|S|](ρ))] = tr(
∑
m
M †m(wlp.Sm.P )Mmρ).
This together with Lemma 2.1 implies
Q ⊑
∑
m
M †m(wlp.Sm.P )Mm.
Case 4. S = while M [q] = 1 do S′. We first prove that
tr(Pnρ) = tr(P [|(while)n|](ρ)) + [tr(ρ)− tr([|(while)n|](ρ))] (6)
by induction on n, where (while)n is an abbreviation of (while M [q] = 1 do S′)n.
The case of n = 0 is obvious. By induction on S′ and induction hypothesis on n, we
observe:
tr(Pn+1ρ) = tr[(M †0PM0) +M
†
1 (wlp.S′.Pn)M1ρ]
= tr(M †0PM0ρ) + tr(M
†
1(wlp.S′.Pn)M1ρ)
= tr(PM0ρM †0 ) + tr((wlp.S′.Pn)M1ρM
†
1)
= tr(PM0ρM †0 ) + tr(Pn[|S′|](M1ρM †1)) + [tr(M1ρM †1 )− tr([|S′|](M1ρM †1 ))]
= tr(PM0ρM †0 ) + tr(P [|(while)n|]([|S|](M1ρM †1))) + [tr([|S|](M1ρM †1))
− tr([|(while)n|]([|S|](M1ρM †1 )))] + [tr(M1ρM †1 )− tr([|S′|](M1ρM †1 ))]
= tr(P [M0ρM †0 + [|(while)n|]([|S|](M1ρM †1 ))]
+ [tr(ρ)− tr(M0ρM †0 + [|(while)n|]([|S|](M1ρM †1 )))]
= tr(P [|(while)n+1|](ρ)) + [tr(ρ)− tr([|(while)n+1|](ρ)].
28

This completes the proof of Eq. (6). Note that quantum predicate P ⊑ I. Then
I − P is positive, and by continuity of trace operator we obtain:
tr((
∞
∧
n=0
Pn)ρ) =
∞
∧
n=0
tr(Pnρ)
=
∞
∧
n=0
{tr(P [|(while)n|](ρ)) + [tr(ρ)− tr([|(while)n|](ρ))]}
= tr(ρ) +
∞
∧
n=0
tr[(P − I)[|(while)n|](ρ)]
= tr(ρ) + tr[(P − I)
∞
∨
n=0
[|(while)n|](ρ)]
= tr(ρ) + tr[(P − I)[|S|](ρ)]
= tr(P [|S|](ρ)) + [tr(ρ)− tr([|S|](ρ))].
For any Q ∈ P(Hall), |=par {Q}S{P} implies:
tr(Qρ) ≤ tr(P [|S|](ρ)) + [tr(ρ)− tr([|S|](ρ)) = tr((
∞
∧
n=0
Pn)ρ)
for all ρ ∈ D−(Hall). This together with Lemma 2.1 leads to Q ⊑
∧∞
n=0 Pn. 
We see that Propositions 7.1 and 7.2 coincide with Figs. 2 and 3, respectively,
in [11] when only quantum variables of type Boolean are considered. But Figs. 2
and 3 in [11] are given directly as definitions, and their intuitive meanings are not
clear because they do not have any connection to total and partial correctness of
quantum programs. In contrast, Propositions 7.1 and 7.2 fill in such a gap, and they
are derived from Definition 7.1, which is given entirely based on the notions of total
and partial correctness of quantum programs.
The next proposition gives a recursive characterization of weakest precondition
and weakest liberal precondition of quantum loop, and it provides a key step in the
proof of completeness of quantum Hoare logic.
Proposition 7.3 We write while for quantum loop “while M [q] = 1 do S”. Then
for any P ∈ P(Hall), we have:
1. wp.while.P = M †0PM0 +M
†
1 (wp.S.(wp.while.P ))M1.
2. wlp.while.P = M †0PM0 +M
†
1 (wlp.S.(wlp.while.P ))M1.
29

Proof. We only prove (2), and the proof of (1) is similar and easier. For every
ρ ∈ D−(Hall), by Proposition 7.2(2) we observe:
tr[(M †0PM0 +M
†
1 (wlp.S.(wlp.while.P ))M1)ρ]
= tr(PM0ρM †0) + tr[(wlp.S.(wlp.while.P ))M1ρM
†
1 ]
= tr(PM0ρM †0) + tr[(wlp.while.P )[|S|](M1ρM †1 )]
+ [tr(M1ρM †1)− tr([|S|](M1ρM †1))]
= tr(PM0ρM †0) + tr[P [|while|]([|S|](M1ρM †1 ))] + [tr([|S|](M1ρM †1)
− tr([|while|]([|S|](M1ρM †1))] + [tr(M1ρM †1 )− tr([|S|](M1ρM †1 ))]
= tr[P (M0ρM †0 + [|while|]([|S|](M1ρM
†
1)))]
+ [tr(M1ρM †1 )− tr([|while|]([|S|](M1ρM †1 ))]
= tr(P [|while|](ρ)) + [tr(ρM †1M1)− tr([|while|]([|S|](M1ρM
†
1 )))]
= tr(P [|while|](ρ)) + [tr(ρ(I −M †0M0))− tr([|while|]([|S|](M1ρM †1 )))]
= tr(P [|while|](ρ)) + [tr(ρ)− tr(M0ρM †0 + [|while|]([|S|](M1ρM †1 )))]
= tr(P [|while|](ρ)) + [tr(ρ)− tr([|while|](ρ))].
This means that
{M †0PM0 +M †1(wlp.S.(wlp.while.P ))M1}while{P},
and
Q ⊑M †0PM0 +M
†
1(wlp.S.(wlp.while.P ))M1
provided |=par {Q}while{P}. 
8 Proof System for Partial Correctness
Now we are ready to present an axiomatic system of Hoare logic for quantum pro-
grams. The quantum Hoare logic can be divided into two proof systems, one for
partial correctness and one for total correctness. In this section, we introduce the
proof system qPD for partial correctness of quantum programs. It consists of the
axioms and inference rules in Fig. 2.
We first prove the soundness of the proof system qPD with respect to the se-
mantics of partial correctness: provability of a correctness formula in qPD implies
its truth in the sense of partial correctness.
Theorem 8.1 (Soundness) The proof system qPD is sound for partial correctness
of quantum programs; that is, for any quantum program S and quantum predicates
P,Q ∈ P(Hall), we have:
⊢qPD {P}S{Q} implies |=par {P}S{Q}.
30

Proof. We only need to show that the axioms and inference rules of qPD are
valid in the sense of partial correctness.
(Axiom Skip) It is obvious that |=par {P}skip{P}.
(Axiom Initialization) We only prove the case of type(q) = integer, and the case
of type(q) = Boolean is similar. For any ρ ∈ D−(Hall), it follows from Proposi-
tion 5.1.2 that
tr[(
∞
∑
n=−∞
|n〉q〈0|P |0〉q〈n|)ρ] =
∞
∑
n=−∞
tr(|n〉q〈0|P |0〉q〈n|ρ)
=
∞
∑
n=−∞
tr(P |0〉q〈n|ρ|n〉q〈0|)
= tr(P
∞
∑
n=−∞
|0〉q〈n|ρ|n〉q〈0|)
= tr(P [|q := 0|](ρ)).
Therefore, we have:
|=par {
∞
∑
n=−∞
|n〉q〈0|P |0〉q〈n|}q := 0{P}.
(Axiom Unitary Transformation) It is easy to see that
|=par {U †PU}q := Uq{P}.
(Rule Sequential Composition) If |=par {P}S1{Q} and |=par {Q}S2{R}, then for
any ρ ∈ D−(Hall) we have:
tr(Pρ) ≤ tr(Q[|S1|](ρ)) + [tr(ρ)− tr([|S1|](ρ))]
≤ tr(R[|S2|]([|S1|](ρ))) + [tr([|S1|](ρ))− tr([|S2|]([|S1|](ρ)))]
+ [tr(ρ)− tr([|S1|](ρ))]
= tr(R[|S1;S2|](ρ)) + [tr(ρ)− tr([|S1;S2|](ρ))].
Therefore, |=par {P}S1;S2{R} as desired.
(Rule Measurement) Assume that |=par {Pm}Sm{Q} for all m. Then for all
31

ρ ∈ D−(Hall), since
∑
mM
†
mMm = IHq , it holds that
tr(
∑
m
M †mPmMmρ) =
∑
m
tr(M †mPmMmρ)
=
∑
m
tr(PmMmρM †m)
≤
∑
m
{tr(Q[|Sm|](MmρM †m)) + [tr(MmρM †m)− tr([|Sm|](MmρM †m))]}
≤
∑
m
tr(Q[|Sm|](MmρM †m)) + [
∑
m
tr(MmρM †m)−
∑
m
tr([|Sm|](MmρM †m))]}
= tr(Q
∑
m
[|Sm|](MmρM †m)) + [tr(
∑
m
ρM †mMm)− tr(
∑
m
[|Sm|](MmρM †m))]}
= tr(Q[|measure|](ρ)) + [tr(ρ)− tr([|measure|](ρ)],
and
|=par {
∑
m
M †mPmMm}measure{Q},
where measure is an abbreviation of statement “measure M [q] : S”.
(Rule Loop Partial) Suppose that
|=par {Q}S{M †0PM0 +M †1QM1.
Then for all ρ ∈ D−(Hall), it holds that
tr(Qρ) ≤ tr((M †0PM0 +M †1QM1)[|S|](ρ)) + [tr(ρ)− tr([|S|](ρ))]. (7)
Furthermore, we have:
tr[(M †0PM0 +M
†
1QM1)ρ] ≤
n
∑
k=0
tr(P (E0 ◦ ([|S|] ◦ E1)k)(ρ))
+ tr(Q(E1 ◦ ([|S|] ◦ E1)n)(ρ))
+
n−1
∑
k=0
[tr(E1 ◦ ([|S|] ◦ E1)k(ρ))− tr(([|S|] ◦ E1)k+1(ρ))]
(8)
for all n ≥ 1. In fact, Eq. (8) may be proved by induction on n. The case of n = 1
is obvious. Using Eq. (7), we obtain:
tr(Q(E1 ◦ ([|S|] ◦ E1)n)(ρ)) ≤ tr((M †0PM0 +M †1QM1)([|S|] ◦ E1)n+1(ρ))
+ [tr((E1 ◦ ([|S|] ◦ E1)n)(ρ)) − tr(([|S|] ◦ E1)n+1(ρ))]
= tr(P (E0 ◦ ([|S|] ◦ E1)n+1)(ρ)) + tr(Q(E1 ◦ ([|S|] ◦ E1)n+1)(ρ))
+ [tr((E1 ◦ ([|S|] ◦ E1)n)(ρ)) − tr(([|S|] ◦ E1)n+1(ρ))].
(9)
32

Combining Eqs. (8) and (9), we assert that
tr[(M †0PM0 +M
†
1QM1)ρ] ≤
n+1
∑
k=0
tr(P (E0 ◦ ([|S|] ◦ E1)k)(ρ))
+ tr(Q(E1 ◦ ([|S|] ◦ E1)n+1)(ρ))
+
n
∑
k=0
[tr(E1 ◦ ([|S|] ◦ E1)k(ρ)) − tr(([|S|] ◦ E1)k+1(ρ))].
Therefore, Eq. (8) holds in the case of n+1 provided it is true in the case of n, and
we complete the proof of Eq. (8).
Now we note that
tr((E1 ◦ ([|S|] ◦ E1)k(ρ)) = tr(M1([|S|] ◦ E1)k(ρ)M †1 )
= tr(([|S|] ◦ E1)k(ρ)M †1M1)
= tr(([|S|] ◦ E1)k(ρ)(I −M †0M0))
= tr(([|S|] ◦ E1)k(ρ))− tr((E0 ◦ ([|S|] ◦ E1)k)(ρ)).
Then it follows that
n−1
∑
k=0
[tr(E1 ◦ ([|S|] ◦ E1)k(ρ))− tr(([|S|] ◦ E1)k+1(ρ))] =
n−1
∑
k=0
tr(([|S|] ◦ E1)k(ρ))
−
n−1
∑
k=0
[tr(E0 ◦ ([|S|] ◦ E1)k(ρ))−
n−1
∑
k=0
tr(([|S|] ◦ E1)k+1(ρ))
= tr(ρ)− tr(([|S|] ◦ E1)n(ρ))−
n−1
∑
k=0
tr(E0 ◦ ([|S|] ◦ E1)k(ρ)).
(10)
On the other hand, we have:
tr(Q(E1 ◦ ([|S|] ◦ E1)n)(ρ)) = tr(QM1([|S|] ◦ E1)n)(ρ)M †1 )
≤ tr(M1([|S|] ◦ E1)n)(ρ)M †1 )
= tr(([|S|] ◦ E1)n)(ρ)M †1M1)
= tr(([|S|] ◦ E1)n)(ρ)(I −M †0M0))
= tr(([|S|] ◦ E1)n)(ρ)) − tr((E0 ◦ ([|S|] ◦ E1)n)(ρ)).
(11)
33

Putting Eqs. (10) and (11) into Eq. (8), we obtain:
tr[(M †0PM0 +M
†
1QM1)ρ] ≤
n
∑
k=0
tr(P (E0 ◦ ([|S|] ◦ E1)k)(ρ))
+ [tr(ρ)−
n
∑
k=0
tr((E0 ◦ ([|S|] ◦ E1)k)(ρ))]
= tr(P
n
∑
k=0
(E0 ◦ ([|S|] ◦ E1)k)(ρ))
+ [tr(ρ)− tr(
n
∑
k=0
(E0 ◦ ([|S|] ◦ E1)k)(ρ))].
Let n→ ∞. Then it follows that
tr[(M †0PM0 +M
†
1QM1)ρ] ≤ tr(P [|while|](ρ) + [tr(ρ)− tr([|while|](ρ))]
and
|=par {M †0PM0 +M †1QM1}while{P},
where while is an abbreviation of quantum loop “while M [q] = 1 do S”. 
Now we are going to establish completeness for the proof system qPD with
respect to the semantics of partial correctness: truth of a quantum program in the
sense of partial correctness implies its provability in qPD. Note that the Lo¨wner
ordering assertions between quantum predicates in (Rule Order) are statements
about complex numbers. So, only a completeness of qPD relative to the theory of
the field of complex numbers may be anticipated; more precisely, we can add all
statements that are true in the field of complex numbers into qPD in order to make
it complete. The following theorem should be understood exactly in the sense of
such a relative completeness.
Theorem 8.2 (Completeness) The proof system qPD is complete for partial cor-
rectness of quantum programs; that is, for any quantum program S and quantum
predicates P,Q ∈ P(Hall), we have:
|=par {P}S{Q} implies ⊢qPD {P}S{Q}.
Proof. If |=par {P}S{Q}, then by Definition 7.1 (2) we have P ⊑ wlp.S.Q.
Therefore, by (Rule Order) it suffices to prove the following:
• Claim: ⊢qPD {wlp.S.Q}S{Q}.
We proceed by induction on the structure of S.
Case 1. S = skip. Immediate from (Axiom Skip).
Case 2. S = q := 0. Immediate from (Axiom Initialization).
34

Case 3. S = q := Uq. Immediate from (Axiom Unitary Transformation).
Case 4. S = S1;S2. It follows from the induction hypothesis on S1 and S2 that
⊢qPD {wlp.S1.(wlp.S2.Q)}S1{wlp.S2.Q}
and
⊢qPD {wlp.S2.Q}S2{Q}.
We obtain:
⊢qPD {wlp.S1.(wlp.S2.Q)}S1;S2{Q}
by (Rule Sequential Composition). Then with Proposition 7.2 (1.d) we see that
⊢qPD {wlp.S1;S2.Q}S1;S2{Q}.
Case 5. S = measure M [q] : S. For all m, by the induction hypothesis on Sm
we obtain:
⊢qPD {wlp.Sm.Q}Sm{Q}.
Then applying (Rule Measurement) yields:
⊢qPD {
∑
m
M †m(wlp.Sm.Q)Mm}measure M [q] : S{Q},
and using Proposition 7.2 (1.e) we have:
⊢qPD {wlp.measure M [q] : S.P}measure M [q] : S{Q}.
Case 6. S = while M [q] = 1 do S′. For simplicity, we write while for quantum
loop “while M [q] = 1 do S′”. The induction hypothesis on S asserts that
⊢qPD {wlp.S.(wlp.while.P )}S{wlp.while.P}.
By Proposition 7.3(2) we have:
wlp.while.P = M †0PM0 +M
†
1(wlp.S.(wlp.while.P ))M1.
Then by (Rule Loop Par) we obtain:
⊢qPD {wlp.while.P}while{P}
as desired. 
9 Proof System for Total Correctness
The aim of this section is to present a proof system qTD for correctness of quan-
tum program. The only difference between qTD and qPD is the inference rule for
quantum loops. To give the rule for total correctness of quantum loops, we need a
notion of bound function which express the number of iterations of a quantum loop
in its computation.
35

Definition 9.1 Let P ∈ P(Hall) and ǫ > 0. A function t : D−(Hall) → N is called
a (P, ǫ)−bound function of quantum loop “while M [q] = 1 do S”if it satisfies the
following conditions:
1. t([|S|](M1ρM †1)) ≤ t(ρ); and
2. tr(Pρ) ≥ ǫ implies t([|S|](M1ρM †1)) < t(ρ)
for all ρ ∈ D−(Hall).
Recall that a bound function t of a classical loop “while B do S od ”satisfies
the inequality t([|S|](s)) < t(s) for any input state s. It is interesting to compare it
with conditions (1) and (2) of the above definition, and we see that the latter are two
inequalities between t([|S|](M1ρM †1 )) and t(ρ) but not between t([|S|](ρ)) and t(ρ).
This is because in the implementation of the quantum loop “while M [q] = 1 do S”,
we need to perform the yes-no measurement M on ρ when checking the loop guard
“M [q] = 1”, and the state of quantum variables will become M1ρM †1 from ρ whence
the measurement outcome “yes”is observed.
The following lemma gives a characterization of the existence of bound function
of a quantum loop in terms of the limit of the state of quantum variables when the
number of iterations of the loop goes to infinity. It provides a key step for the proof
of soundness and completeness of the proof system qTD.
Lemma 9.1 Let P ∈ P(Hall). Then the following two statements are equivalent:
1. for any ǫ > 0, there exists a (P, ǫ)−bound function tǫ of quantum loop “whileM [q] =
1 do S”;
2. limn→∞ tr(P ([|S|] ◦ E1)n(ρ)) = 0 for all ρ ∈ D−(Hall).
Proof. (1 ⇒ 2) We prove this by refutation. If
lim
n→∞
tr(P ([|S|] ◦ E1)n(ρ)) 6= 0,
then there exist ǫ0 > 0 and strictly increasing sequence {nk} of nonnegative integers
such that
tr(P ([|S|] ◦ E1)nk(ρ)) ≥ ǫ0
for all k ≥ 0. Thus, we have a (P, ǫ0)−bound function of loop whileM [q] = 1 do S.
For each k ≥ 0, we set
ρk = ([|S|] ◦ E1)nk(ρ).
Then it holds that tr(Pρk) ≥ ǫ0, and by conditions 1 and 2 in Definition 9.1 we
obtain:
ttǫ0(ρk) > tǫ0([|S|](M1ρkM †1))
= tǫ0(([|S|] ◦ E1)(ρk))
≥ tǫ0(([|S|] ◦ E1)nk+1−nk(ρk))
= tǫ0(ρk+1).
36

Consequently, we have an infinitely descending chain {tǫ0(ρk)} in N, the set of non-
negative integers. This is a contradiction because N is a well-founded set.
(2 ⇒ 1) For each ρ ∈ D−(Hall), if
lim
n→∞
tr(P ([|S|] ◦ E1)n(ρ)) = 0,
then for any ǫ > 0, there exists N ∈ N such that
tr(P ([|S|] ◦ E1)n(ρ)) < ǫ
for all n ≥ N . We define:
tǫ(ρ) = min{N ∈ N : tr(P ([|S|] ◦ E1)n(ρ)) < ǫ for all n ≥ N}.
Now it suffices to show that tǫ is a (P, ǫ)−bound function of loop “while M [q] =
1 do S”. To this end. we consider the following two cases:
Case 1. tr(Pρ) ≥ ǫ. Suppose that tǫ(ρ) = N . Then tr(Pρ) ≥ ǫ implies N ≥ 1.
By the definition of tǫ, we assert that
tr(P ([|S|] ◦ E1)n(ρ)) < ǫ
for all n ≥ N . Thus, for all n ≥ N − 1 ≥ 0,
tr(P ([|S|] ◦ E1)n([|S|](M †1ρM1))) = tr(P ([|S|] ◦ E1)n+1(ρ)) < ǫ.
Therefore,
tǫ([|S|](M †1ρM1)) ≤ N − 1 < N = tǫ(ρ).
Case 2. tr(Pρ) < ǫ. Again, suppose that tǫ(ρ) = N . Now we have the following
two subcases:
Subcase 2.1. N = 0. Then for all n ≥ 0,
tr(P ([|S|] ◦ E1)n(ρ)) < ǫ.
It is easy to see that tǫ([|S|](M1ρM †1 )) = 0 = tǫ(ρ).
Subcase 2.2. n ≥ 1. We can derive that
tǫ(ρ) > tǫ([|S|](M1ρM †1 ))
in the way of Case 1. 
Now we are ready to present the proof system qTD for total correctness of quan-
tum programs. It consists of the axioms (Axiom Skip), (Axiom Initialization) and
(Axiom Unitary Transformation) and inference rules (Rule Sequential Composition),
(Rule Measurement) and (Rule Order) in Fig.2 as well as inference rule (Rule Loop
Total) in Fig.3.
The remainder of this section will be devoted to establish soundness and com-
pleteness of qTD: provability of a correctness formula in qTD is equivalent to its
truth in the sense of total correctness.
37

Theorem 9.1 (Soundness) The proof system TD is sound for total correctness of
quantum programs; that is, for any quantum program S and quantum predicates
P,Q ∈ P(Hall), we have:
⊢qTD {P}S{Q} implies |=tot {P}S{Q}.
Proof. It suffices to show that the axioms and inference rules of TD are valid in
the sense of total correctness.
The proof for soundness of (Axiom Skip), (Axiom Initialization) and (Axiom
Unitary Transformation) is similar to the case of partial correctness.
(Rule Sequential Composition) Suppose that |=tot {P}S1{Q} and |=tot {Q}S2{R}.
Then for any ρ ∈ D−(Hall), with Proposition 5.1.4 we obtain:
tr(Pρ) ≤ tr(Q[|S1|](ρ))
≤ tr(R[|S2|]([|S1|](ρ)))
= tr(P [|S1;S2|](ρ)).
Therefore, |=tot {P}S1;S2{R}.
(Rule Measurement) Suppose that |=tot {Pm}Sm{Q} for all m. Then for any
ρ ∈ D−(Hall), it holds that
tr(PmMmρM †m) ≤ tr(Q[|Sm|](MmρM †m))
because {Pm}Sm{Q} for all m. Therefore, we have:
tr(
∑
m
M †mPmMmρ) =
∑
m
tr(PmMmρM †m)
≤
∑
m
tr(Q[|Sm|](MmρM †m))
= tr(Q
∑
m
[|Sm|](MmρM †m))
= tr(Q[|measure M [q] : S|](ρ)),
and
|=tot {
∑
m
M †mPMm}measure M [q] : S{Q}.
(Rule Loop Total) If
|=tot {Q}S{M †0PM0 +M †1QM1},
then for any ρ ∈ D−(Hall), we have:
tr(Qρ) ≤ tr((M †0PM0 +M †1QM1)[|S|]par(ρ)). (12)
38

We first prove the following inequality:
tr[(M †0PM0 +M
†
1QM1)ρ]
≤
n
∑
k=0
tr(P [E0 ◦ ([|S|] ◦ E1)]k(ρ)) + tr(Q[E1 ◦ ([|S|] ◦ E1)n](ρ))
(13)
by induction on n. It holds that
tr[(M †0PM0 +M
†
1QM1)ρ] = tr(PM0ρM
†
0 ) + tr(QM1ρM
†
1 )
= tr(PE0(ρ)) + tr(QE1(ρ)).
So, Eq. (13) is correct for the base case of n = 0. Assume Eq. (13) is correct for the
case of n = m. Then applying Eq. (12), we obtain:
tr[(M †0PM0 +M
†
1QM1)ρ] = tr(PE0(ρ)) + tr(QM1ρM †1 )
≤
m
∑
k=0
tr(P [E0 ◦ ([|S|] ◦ E1)]k(ρ)) + tr(Q[E1 ◦ ([|S|] ◦ E1)m](ρ))
≤
m
∑
k=0
tr(P [E0 ◦ ([|S|] ◦ E1)]k(ρ)) + tr((M †0PM0 +M †1QM1)[|S|]([E1 ◦ ([|S|] ◦ E1)m](ρ)))
=
m
∑
k=0
tr(P [E0 ◦ ([|S|] ◦ E1)]k(ρ)) + tr(PM0[|S|]([E1 ◦ ([|S|] ◦ E1)m](ρ))M †0 )
+ tr(QM1[|S|]([E1 ◦ ([|S|] ◦ E1)m](ρ))M †1 )
=
m+1
∑
k=0
tr(P [E0 ◦ ([|S|] ◦ E1)]k(ρ)) + tr(Q[E1 ◦ ([|S|] ◦ E1)m+1](ρ)).
Therefore, Eq. (13) also holds for the case of n = M + 1. Now, since for any ǫ > 0,
there exists M †1QM1, ǫ−bound function tǫ of quantum loop “whileM [q] = 1 do S”,
by Lemma 9.1 we have:
lim
n→∞
tr(Q[E1 ◦ ([|S|] ◦ E1)n(ρ)) = limn→∞ tr(QM1([|S|] ◦ E1)
n(ρ)M †1 )
= lim
n→∞
tr(M †1QM1([|S|] ◦ E1)n(ρ)) = 0.
Consequently, it holds that
tr[(M †0PM0 +M
†
1QM1)ρ] ≤ limn→∞
n
∑
k=0
tr(P [E0 ◦ ([|S|] ◦ E1)]n(ρ))
+ lim
n→∞
tr(Q[E1 ◦ ([|S|] ◦ E1)n](ρ))
=
∞
∑
n=0
tr(P [E0 ◦ ([|S|] ◦ E1)]n(ρ))
= tr(P
∞
∑
n=0
[E0 ◦ ([|S|] ◦ E1)n](ρ))
= tr(P [|while M [q] = 1 do S|](ρ)). 
39

Theorem 9.2 (Completeness) The proof system TD is complete for total correct-
ness of quantum programs; that is, for any quantum program S and quantum predi-
cates P,Q ∈ P(Hall), we have:
|=tot {P}S{Q} implies ⊢qTD {P}S{Q}.
Proof. Similar to the case of partial correctness, it suffices to prove the following:
• Claim: ⊢qTD {wlp.S.Q}S{Q} for any quantum program S and quantum
predicate P ∈ P(Hall)
because by Definition 7.1 (1) we have P ⊑ wp.S.Q when |=tot {P}S{Q}. The above
claim can be done by induction on the structure of S. We only consider the case
of S = while M [q] = 1 do S′, and the other cases are similar to the proof of
Theorem 8.2. We write while for quantum loop “while M [q] = 1 do S′”. It follows
from Proposition 7.3(1) that
wp.while.Q = M †0QM0 +M
†
1(wp.S.(wp.while.Q))M1.
So, our aim is to derive that
⊢qTD {M †0QM0 +M †1 (wp.S.(wp.while.Q))M1}while{Q}.
By the induction hypothesis on S′ we get:
⊢qTD {wp.S′.(wp.while.Q)}S{wp.while.Q}.
Then by (Rule Loop Total) it suffices to show that for any ǫ > 0, there exists
a (M †1 (wp.S′. (wp.S.Q))M1, ǫ)−bound function of quantum loop while. Applying
Lemma 9.1, we only need to prove:
lim
n→∞
tr(M †1 (wp.S′.(wp.while.Q))M1([|S′|] ◦ E1)n(ρ)) = 0. (14)
First, by Propositions 7.1 (2) and 5.1 (6) we observe:
tr(M †1(wp.S′.(wp.while.Q))M1([|S′|] ◦ E1)n(ρ))
= tr(wp.S′.(wp.while.Q)M1([|S′|] ◦ E1)n(ρ)M †1 )
= tr(wp.while.Q[|S′|](M1([|S′|] ◦ E1)n(ρ)M †1 ))
= tr(wp.while.Q([|S′|] ◦ E1)n+1(ρ))
= tr(Q[|while|]([|S′|] ◦ E1)n+1(ρ))
=
∞
∑
k=n+1
tr(Q[E0 ◦ ([|S′|] ◦ E1)k](ρ)).
(15)
Second, we consider the following infinite series of nonnegative real numbers:
∞
∑
n=0
tr(Q[E0 ◦ ([|S′|] ◦ E1)k](ρ)) = tr(Q
∞
∑
n=0
[E0 ◦ ([|S′|] ◦ E1)k](ρ)). (16)
40

Since Q ⊑ IHall , it follows from Propositions 5.1 (6) and 5.2 that
tr(Q
∞
∑
n=0
[E0 ◦ ([|S′|] ◦ E1)k](ρ)) = tr(Q[|while|](ρ))
≤ tr([|while|](ρ)) ≤ tr(ρ) ≤ 1.
Therefore, the infinite series Eq. (16) converges. Note that Eq. (15) is the sum of the
remaining terms of the infinite series Eq. (16) after the nth term. Then convergence
of the infinite series Eq. (16) implies Eq. (14), and we complete the proof. 
It should be pointed out that the above theorem is merely a relative completeness
of qTD with respect to the theory of the fields of complex numbers because except
that (Rule Order) is employed in qTD, the existence of bound functions in (Rule
Loop Total) is also a statement about complex numbers.
10 Conclusion
Based on D’Hondt and Panangaden’s idea of representing quantum predicates by
Hermitian operators and Selinger’s idea of modeling quantum programs by super-
operators, a full-fledged Hoare logic is developed for deterministic quantum pro-
grams, and its completeness relative to the theory of the field of complex numbers
is proved in this paper.
An interesting problem for further studies is to find reasonable extensions of the
quantum Hoare logic presented in this paper for bigger classes of quantum programs,
including nondeterministic quantum programs [25], parallel and distributed quan-
tum programs. Hopefully, they will serve as a logical foundation of various effective
techniques for verification of these bigger classes of quantum programs.
References
[1] D. Akatov, The Logic of Quantum Program Verification, Master Thesis, Oxford
University Computing Laboratory, 2005.
[2] T. Altenkirch and J. Grattage, A functional quantum programming language,
in: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer
Science (LICS), 2005, pp. 249-258.
[3] K. R. Apt and E. R. Olderog, Verification of Sequential and Concurrent Pro-
grams, Springer-Verlag, New York, 1997.
[4] A. Baltag and S. Smets, The logic of quantum programs, in: P. Selinger (ed.),
Proceedinds of QPL’2004, TUCS General Publication 33, Turku Center for
Computer Science, pp. 39-56.
[5] A. Baltag and S. Smets, LQP: the dynamic logic of quantum information, Math-
ematical Structures in Computer Science, 16(2006)491-525.
41

[6] S. Bettelli, T. Calarco and L. Serafini, Toward an architecture for quantum
programming, The European Physical Journal D, 25(2003)181-200.
[7] G. Birkhoff and J. von Neumann, The logic of quantum mechanics, Annals of
Mathematics, 37(1936)823-843.
[8] O. Brunet and P. Jorrand, Dynamic quantum logic for quantum programs,
International Journal of Quantum Information, 2(2004)45-54.
[9] R. Chadha, P. Mateus and A. Sernadas, Reasoning about imperative quantum
programs, Electronic Notes in Theoretical Computer Science, 158(2006)19-39.
[10] E. D’Hondt and P. Panangaden, Quantum weakest preconditions, Mathematical
Structures in Computer Science, 16(2006)429-451.
[11] Y. Feng, R. Y. Duan, Z. F. Ji and M. S. Ying, Proof rules for the correctness
of quantum programs, Theoretical Computer Science, 386(2007)151-166.
[12] S. Gay, Quantum programming languages: survey and bibliography, Mathemat-
ical Structures in Computer Science, 16(2006)581-600.
[13] E. H. Knill, Conventions for quantum pseudocode, Technical Report LAUR-96-
2724, Los Alamos National Laboratory, 1996.
[14] C. Morgan, Proof rules for probabilistic loops, Technical Report PRG-TR-25-95,
Programming Research Group, Oxford University, 1995.
[15] S. -C. Mu and R. Bird, Functional quantum programming, in: Proceedings of
the 2nd Asian Workshop on Programming Languages and Systems, 2001.
[16] B. O¨mer, Structural quantum programming, Ph.D. Thesis, Technical University
of Vienna, 2003.
[17] A. Petersen and M. Oskin, A new algebraic foundation for quantum program-
ming languages, in: Proceedings of the 2nd Workshop on Non-Silicon Comput-
ing, 2003.
[18] J. W. Sanders and P. Zuliani, Quantum programming, in: Proceedings, Mathe-
matics of Program Construction, LNCS 1837, Springer-Verlag, 2000, pp. 88-99.
[19] P. Selinger, Towards a quantum programming language, Mathematical Struc-
tures in Computer Science, 14(2004)527-586.
[20] P. Selinger, A brief survey of quantum programming languages, in: Proceedings
of the 7th International Symposium on Functional and Logic Programming,
LNCS 2998, Springer-Verlag, 2004.
[21] J. von Neumann, On infinite direct products, Compos. Math., 6(1938)1-77.
42

[22] M. S. Ying, J. X. Chen, Y. Feng and R. Y. Duan, Commutativity of quantum
weakest preconditions, Information Processing Letters, 104(2007)152-158.
[23] M. S. Ying, R. Y. Duan, Y. Feng and Z. F. Ji, Predicate transformer semantics
of quantum programs, in: I. Mackie and S. Gay (eds.), Semantic Techniques in
Quantum Computation, Cambridge University Press, 2009.
[24] M. S. Ying and Y. Feng, Quantum loop programs, Acta Informatica (under
review).
[25] P. Zuliani, Nondeterministic quantum programming, in: P. Selinger (ed.), Pro-
ceedings of the 2nd International Workshop on Quantum Programming Lan-
guages, July 12-13, 2004, Turku, Finland, TUCS General Publication No. 33,
Turku Center for Computer Science, pp. 179-195.
[26] P. Zuliani, Compiling quantum programs, Acta Informatica, 41(2005)435-474.
43

Appendix: Proof of Proposition 5.3
(1) We proceed by induction on the structure of S.
Case 1. S = skip. Obvious.
Case 2. S = q := 0. We only consider the case of type(q) = integer, and the
case of type(q) = Boolean is similar. It holds that
trvar(S)([|S|](ρ)) =
∞
∑
n,n′=−∞
q〈n′|0〉q〈n|ρ|n〉q〈0|n′〉q
=
∞
∑
n=−∞
q〈n|ρ|n〉q
= trvar(S)(ρ).
Case 3. S = q := Uq. If {|ψi〉} is an orthonormal basis of Hq, then {U †|ψi〉} is
also an orthonormal basis of Hq. Consequently,
trV ar(S)([|S|](ρ)) =
∑
i
〈ψi|UρU †|ψi〉 = trV ar(S)(ρ).
Case 4. S = S1;S2. By the induction hypothesis on S1 and S2, we have:
trvar(S)([|S|](ρ)) = trvar(S1)∪var(S2)([|S2|]([|S1|](ρ)))
= trvar(S1)(trvar(S2)([|S2|]([|S1|](ρ))))
= trvar(S1)(trvar(S2)([|S1|](ρ)))
= trvar(S2)(trvar(S1)([|S1|](ρ)))
= trvar(S2)(trvar(S1)(ρ))
= trvar(S)(ρ).
Case 5. S = measure M [q] : S. By the induction hypothesis on Sm for all
44

outcome m of measurement M , we obtain:
trvar(S)([|S|](ρ)) =
∑
m
trvar(S)([|Sm|](MmρM †m))
=
∑
m
trvar(S)−var(Sm)(trvar(Sm)([|Sm|](MmρM †m)))
=
∑
m
trvar(S)−var(Sm)(trvar(Sm)(MmρM †m))
=
∑
m
trvar(S)(MmρM †m)
=
∑
m
trvar(S)−{q}(trq(MmρM †m))
=
∑
m
trvar(S)−{q}(trq(M †mMmρ))
= trvar(S)−{q}(trq((
∑
m
M †mMm)ρ))
= trvar(S)−{q}(trq(ρ))
= trvar(S)(ρ)
because
∑
mM
†
mMm = IHq .
Case 6. S = while M [q] = 1 do S′. For simplicity, we write while for quantum
loop “while M [q] = 1 do S′”. First, we have:
trvar(S)([|(while)0|](ρ)) = 0Hall ,
trvar(S)([|(while)n|](ρ)) = trvar(S)(ρ) (17)
for all n ≥ 1. This can be proved by induction on n. In fact,
(while)k+1 = measure M [q] : S
where S = S0, S1, S0 = skip, and S1 = S′; (while)k. Thus, by Cases 1, 4 and 5,
we can derive Eq. (17) for n = k+1 immediately from the induction hypothesis for
n = k. Now, it follows from continuity of trace that
trvar(S)([|S|](ρ)) = trvar(S)(
∞
∨
n=0
[|(while)n|](ρ))
=
∞
∨
n=0
trvar(S)([|(while)n|](ρ))
= trvar(S)(ρ).
(2) The trick is to prove the following slightly stronger conclusion:
• Claim: For any var(S) ⊆ X ⊆ V ar, trX−var(S)(ρ1) = trX−var(S)(ρ2) implies
trX−var(S)([|S|](ρ1)) = trX−var(S)([|S|](ρ2)).
45

We also proceed by induction on the structure of S.
Case 1. S = skip. Obvious.
Case 2. S = q := 0. We only consider the case of type(q) = integer, the case of
type(q) = Boolean is similar. First, let {|ψi〉} be an orthonormal basis of HX−{q},
then we have:
trX−var(S)([|S|](ρ)) = trX−{q}[
∞
∑
n=−∞
(|0〉q〈n| ⊗ IHV ar−{q})ρ(|n〉q〈0| ⊗ IHV ar−{q})]
=
∑
i
∞
∑
n=−∞
(IH(V ar−X)∪{q} ⊗ 〈ψi|)(|0〉q〈n| ⊗ IHV ar−{q})ρ
(|n〉q〈0| ⊗ IHV ar−{q})(IH(V ar−X)∪{q} ⊗ |ψi〉)
=
∞
∑
n=−∞
((|0〉q〈n| ⊗ IHV ar−{q})
∑
i
(IH(V ar−X)∪{q} ⊗ 〈ψi|)ρ
(IH(V ar−X)∪{q} ⊗ |ψi〉)(|n〉q〈0| ⊗ IHV ar−{q})
=
∞
∑
n=−∞
|0〉q〈n|trX−var(S)(ρ)|n〉q〈0|.
Thus, it is easy to see that (2) holds in this case.
Case 3. S = q := Uq. Assume that {|ψi〉} is an orthonormal basis of HX−{q}.
Then it holds that
trX−var(S)([|S|](ρ)) = trX−{q}(U ⊗ IHV ar−{q})ρ(U † ⊗ IHV ar−{q})
=
∑
i
(IH(V ar−X)∪{q} ⊗ 〈ψi|)(U ⊗ IHV ar−{q})ρ(U † ⊗ IHV ar−{q})(IH(V ar−X)∪{q} ⊗ |ψi〉)
= (U ⊗ IHV ar−{q})
∑
i
(IH(V ar−X)∪{q} ⊗ 〈ψi|)ρ(IH(V ar−X)∪{q} ⊗ |ψi〉)(U † ⊗ IHV ar−{q})
= (U ⊗ IHV ar−{q})trX−var(S)(ρ)(U † ⊗ IHV ar−{q})
because |ψi〉 ∈ HX−{q}, U ∈ L(Hq), and (X − {q}) ∩ {q} = ∅. Now it is easy to see
that (2) holds in this case.
Case 4. S = S1;S2. If var(S1) ∪ var(S2) = var(S) ⊆ X, then there are Y,Z ⊆
V ar such that var(S1) ⊆ Y , var(S2) ⊆ Z and
Y − var(S1) = X − var(S) = Z − var(S2).
Thus, we have:
trY−var(S1)(ρ1) = trX−var(S)(ρ1)
= trX−var(S)(ρ2)
= trY−var(S1)(ρ2).
46

By the induction hypothesis on S1, we obtain:
trZ−var(S2)([|S1|](ρ1)) = trY−var(S1)([|S1|](ρ1))
= trY−var(S1)([|S1|](ρ2))
= trZ−var(S2)([|S1|](ρ2)).
Furthermore, by the induction hypothesis on S2, we obtain:
trX−var(S)([|S|](ρ1)) = trZ−var(S2)([|S2|]([|S1|](ρ1)))
= trZ−var(S2)([|S2|]([|S1|](ρ2)))
= tr(X−var(S)([|S|](ρ2)).
Case 5. S = measure M [q] : S. First, let {|ψi〉} be an orthonormal basis of
HX−var(S). Then for any outcome m of measurement M , we have:
trX−var(S)(MmρM †m) =
∑
i
(IHV ar−(X−var(S)) ⊗ 〈ψi|)(Mm ⊗ IHV ar−{q})ρ
(M †m ⊗ IHV ar−{q})(IHV ar−(X−var(S)) ⊗ |ψi〉)
= (Mm ⊗ IHV ar−{q})
∑
i
(IHV ar−(X−var(S)) ⊗ 〈ψi|)ρ
(IHV ar−(X−var(S)) ⊗ |ψi〉)(M †m ⊗ IHV ar−{q})
= MmtrX−var(S)(ρ)M †m
because |ψi〉 ∈ HX−var(S), Mm ∈ L(Hq) and (X − var(S))∩{q} = ∅. Consequently,
it follows from trX−var(S)(ρ1) = trX−var(S)(ρ2) that
trX−var(S)(Mmρ1M †m) = trX−var(S)(Mmρ2M †m).
Note that we can write X − var(S) = Y − var(Sm) for some Y ⊇ var(Sm). Then it
holds that
trY−var(Sm)(Mmρ1M †m) = trY−var(Sm)(Mmρ2M †m).
By the induction hypothesis on Sm, we obtain:
trX−var(S)([|Sm|](Mmρ1M †m)) = trY−var(Sm)([|Sm|](Mmρ1M †m))
= trY−var(Sm)([|Sm|](Mmρ2M †m))
= trX−var(S)([|Sm|](Mmρ2M †m)).
47

Therefore, it follows that
trX−var(S)([|S|](ρ1)) = trX−var(S)
∑
m
[|Sm|](Mmρ1M †m)
=
∑
m
trX−var(S)([|Sm|](Mmρ1M †m))
=
∑
m
trX−var(S)([|Sm|](Mmρ2M †m))
= trX−var(S)
∑
m
[|Sm|](Mmρ2M †m)
= trX−var(S)([|S|](ρ2)).
Case 6. S = whileM [q] = 1 do S′. Assume that trX−var(S)(ρ1) = trX−var(S)(ρ2).
Using Cases 1, 4 and 5, we can show that
trX−var(S)([|(while)n|](ρ1)) = trX−var(S)([|(while)n|](ρ2))
for all n ≥ 0 by induction on n. Therefore, we obtain:
trX−var(S)([|while|](ρ1)) = trX−var(S)(
∞
∨
n=0
[|(while)n|](ρ1))
=
∞
∨
n=0
trX−var(S)([|(while)n|](ρ1))
=
∞
∨
n=0
trX−var(S)([|(while)n|](ρ2))
= trX−var(S)(
∞
∨
n=0
[|(while)n|](ρ2))
= trX−var(S)([|while|](ρ2))
by continuity of trace.
48

(Skip) 〈skip, ρ〉 → 〈E, ρ〉
(Initialization) 〈q := 0, ρ〉 → 〈E, ρq0〉
where
ρq0 = |0〉q〈0|ρ|0〉q〈0|+ |0〉q〈1|ρ|1〉q〈0|
if type(q) = Boolean, and
ρq0 =
∞
∑
n=−∞
|0〉q〈n|ρ|n〉q〈0|
if type(q) = integer.
(Unitary Transformation) 〈q := Uq, ρ〉 → 〈E,UρU †〉
(Sequential Composition) 〈S1, ρ〉 → 〈S
′
1, ρ′〉
〈S1;S2, ρ〉 → 〈S′1;S2, ρ〉
where we make the convention that E;S2 = S2.
(Measurement)
〈measure M [q] : S, ρ〉 → 〈Sm,MmρM †m〉
for each outcome m of measurement M = {Mm}
(Loop 0)
〈while M [q] = 1 do S, ρ〉 → 〈E,M0ρM †0 〉
(Loop 1)
〈while M [q] = 1 do S, ρ〉 → 〈S;while M [q] = 1 do S,M1ρM †1 〉
Figure 1: Transitional Semantics of Quantum Programs
49

(Axiom Skip) {P}Skip{P}
(Axiom Initialization) If type(q) = Boolean, then
{|0〉q〈0|P |0〉q〈0|+ |1〉q〈0|P |0〉q〈1|}q := 0{P}
and if type(q) = integer, then
{
∞
∑
n=−∞
|n〉q〈0|P |0〉q〈n|}q := 0{P}
(Axiom Unitary Transformation) {U †PU}q := Uq{P}
(Rule Sequential Composition) {P}S1{Q} {Q}S2{R}{P}S1;S2{R}
(Rule Measurement) {Pm}Sm{Q} for all m
{∑mM
†
mPmMm}measure M [q] : S{Q}
(Rule Loop Partial) {Q}S{M
†
0PM0 +M
†
1QM1}
{M †0PM0 +M †1QM1}while M [q] = 1 do S{P}
(Rule Order) P ⊑ P
′ {P ′}S{Q′} Q′ ⊑ Q
{P}S{Q}
Figure 2: Proof System qPD of Partial Correctness
(Rule Loop Total)
{Q}S{M †0PM0 +M
†
1QM1}
for any ǫ > 0, tǫ is a (M †1QM1, ǫ)− bound function
of loop while M [q] = 1 do S
{M †0PM0 +M
†
1QM1}while M [q] = 1 do S{P}
Figure 3: Proof System qTD of Total Correctness
50