11institutetext: Zhejiang Lab, Hangzhou, China

# On the Relative Completeness of Satisfaction-based Quantum Hoare Logic

Xin Sun  Xingchi Su  Xiaoning Bian  Huiwen Wu

###### Abstract

Quantum Hoare logic (QHL) is a formal verification tool specifically designed
to ensure the correctness of quantum programs. There has been an ongoing
challenge to achieve a relatively complete satisfaction-based QHL with while-
loop since its inception in 2006. This paper presents a solution by proposing
the first relatively complete satisfaction-based QHL with while-loop. The
completeness is proved in two steps. First, we establish a semantics and proof
system of Hoare triples with quantum programs and deterministic assertions.
Then, by utilizing the weakest precondition of deterministic assertion, we
construct the weakest preterm calculus of probabilistic expressions. The
relative completeness of QHL is then obtained as a consequence of the weakest
preterm calculus. Using our QHL, we formally verify the correctness of
Deutsch’s algorithm and quantum teleportation.

###### Keywords:

Hoare logic quantum program relative completeness weakest precondition

##  1 Introduction

In the realm of computer science, Hoare logic serves as a tool for formally
verifying the correctness of computer programs. It was first established by C.
A. R. Hoare in his groundbreaking paper [13] published in 1969, and later
expanded upon in [14]. When executing a program, it’s important to consider
the conditions that must be met before and after executing a command. The
precondition describes the property that the command is based on, while the
postcondition describes the desired outcome of the command after it has been
correctly executed. This is the key idea of Hoare logic which has become one
of the most influential tools in the formal verification of programs in the
past decades. It has been successfully applied in the analysis of
deterministic [13, 14, 24], non-deterministic [9, 10, 1], recursive [14, 12,
2], probabilistic [18, 7, 5, 19], and quantum programs [25, 16, 23, 29, 8]. A
comprehensive review of Hoare logic is referred to Apt, Boer, and Olderog [2,
4].

Quantum Hoare logic (QHL) is an extension of the classical Hoare logic. It is
specifically designed to ensure the correctness of quantum programs. To make
QHL work, a programming language that supports quantum commands, such as
unitary operations and measurements, as well as other classical commands is
required. The assertion language used in QHL describes quantum states, such as
unit vectors and density operators, along with the probabilistic distributions
over them. Hoare triples are used to formalize how quantum programs change the
states by showing the update on assertions. The proof system characterizes the
reasoning about Hoare triples so as to expose the deductive relationship
between the state changes caused by quantum programs. There has been a lot of
research on QHL that can be classified into two approaches: expectation-based
and satisfaction-based. Table 1 compares them in terms of different types of
programming languages, including the classical, probabilistic, and Quantum
programs. Note that, $\mathcal{D}(\mathcal{H})$ and $\mathcal{P(\mathcal{H})}$
in row Quantum-expectation stand for the set of density operators and
Hermitian operators over Hilbert space $\mathcal{H}$ with certain conditions,
following the notations in [25].

The first QHL was developed by Chadha et al [6], which is considered to be the
first satisfaction-based construction. Kakutani [15] established another
satisfaction-based QHL for a functional quantum programming language designed
by Selinger [20]. Unruh [22] provided a satisfaction-based QHL to feature
“ghost variables”, which is used to extend the expressive power of assertions.

Following the expectation-based approach, several different QHLs have been
developed by Ying et al in their series of work [25, 27, 29, 11]. They
investigate pure quantum language and infinite-dimensional quantum variables,
new auxiliary proof rules, quantum-classical language, and restricted
assertions, respectively.

Table 1: Comparison of the basic notions in different language paradigms.

| State | Semantic space of | Satisfiability of
---|---|---|---
|  | assertions | an assertion $a$
Classical | set of evaluations | subsets of states | $S\in[\\![a]\\!]$
$S\in\mathbb{S}$ | $\mathbb{S}\rightarrow\\{0,1\\}$
Probabilistic | (sub)distributions | random variables | $\sum_{S\in\mathbb{S}}[\\![a]\\!](S)\mu(S)$
(expectation) | $\mu\in\mathbb{S}\rightarrow[0,1]$ | $\mathbb{S}\rightarrow[0,1]$
Probabilistic | (sub)distributions | subsets of distributions | $\mu\in[\\![a]\\!]$
(satisfaction) | $\mu\in\mathbb{S}\rightarrow[0,1]$ | $(\mathbb{S}\rightarrow[0,1])\rightarrow\\{0,1\\}$
Quantum | cq-state | cq-assertion | $\sum_{S\in\mathbb{S}}\textbf{Tr}[\Delta(S)\Theta(S)]$
(expectation) | $\Delta\in\mathbb{S}\rightarrow\mathcal{D}(\mathcal{H})$ | $\Theta\in\mathbb{S}\rightarrow\mathcal{P}(\mathcal{H})$
Quantum | distributions of cq-state | subsets of distributions | $\mu\in[\\![a]\\!]$
(satisfaction) | $\mu\in(\mathbb{S}\,\times\,\mathcal{H})\rightarrow[0,1]$ | $((\mathbb{S}\,\times\,\mathcal{H})\rightarrow[0,1])\rightarrow\\{0,1\\}$

Several variants of QHL have been verified and implemented. The QHLProver [16]
was the first to formalize QHL in a proof assistant and used the verified
implementation to verify the correctness of Grover’s algorithm. CoqQ [28]
verifies the soundness of QHL adapted from [25, 27] in the Coq proof
assistant. The work then uses CoqQ to verify several quantum algorithms,
including Grover’s algorithm and quantum phase estimation.

The problem of establishing the relative completeness of satisfaction-based
QHL with While-loop has remained unresolved since its inception in 2006 [6].
This paper aims to address this issue by developing the first satisfaction-
based QHL with while-loop that is relatively complete. To accomplish this, we
follow the same approach as used to demonstrate the relative completeness of
satisfaction-based probabilistic Hoare logic (PHL) [21]. Our solution involves
two steps. Firstly, we establish a semantics and proof system of Hoare triples
with quantum programs and deterministic assertions. Then, using the weakest
precondition of deterministic assertion, we construct the weakest preterm
calculus of probabilistic expressions. The relative completeness of QHL is
then obtained as a consequence of the weakest preterm calculus.

This paper is organized as follows: Section 2 constructs a relatively complete
QHL with deterministic assertion. Section 3 extends the result of the QHL with
deterministic assertion to the QHL with probabilistic assertion. Section 4
concludes the paper and discusses possible future work. The Appendix
introduces some basics of quantum computing, gives proof details of major
theorems, and provides two applications of our QHL: correctness proofs of
Deutsch’s algorithm and quantum teleportation.

##  2 Quantum Hoare logic with deterministic assertion

###  2.1 Deterministic expressions and formulas

Let $\mathbb{PV}=\\{X,Y,Z,\ldots\\}$ be a set of classical program variables.
Let $\mathbb{LV}=\\{x,y,z,\ldots\\}$ be a set of logical variables. Program
variables are those variables that may occur only in programs. They constitute
deterministic expressions. Deterministic expressions are classified into
arithmetic expression $E$ and Boolean expression $B$. The arithmetic
expression consists of integer constants $n\in\mathbb{Z}$, variables from
$\mathbb{PV}$ and arithmetic operators
$\\{+,-,\times,...\\}\subseteq\mathbb{Z}\times\mathbb{Z}\rightarrow\mathbb{Z}$.

######  Definition 1 (Arithmetic expressions).

Given a set of program variables $\mathbb{PV}$, we define the arithmetic
expression $E$ as follows:

$E:=n\mid X\mid(E\ aop\ E)$.

An arithmetic expression ($E$) can take the form of an integer constant ($n$),
a program variable ($X$), or a combination of two arithmetic expressions ($E\
aop\ E$) composed by an arithmetic operation ($aop$).

The Boolean constant set is $\mathbb{B}=\\{\top,\bot\\}$. We use relational
operators ($rop$) i.e.,
$\\{>,<,\geq,=,...\\}\subseteq\mathbb{Z}\times\mathbb{Z}\rightarrow\mathbb{B}$
to compare arithmetic expressions ($E$) which represent integers in programs.

######  Definition 2 (Boolean expressions).

The Boolean expression is defined as follows:

$B:=\top\mid\bot\mid(E\ rop\ E)\mid\neg B\mid(B\wedge B).$

A Boolean expression is a statement that can only be true or false. In the
expression $(E\ rop\ E)$, the truth value is determined by the binary relation
$rop$ between two integers.

The semantics of deterministic expressions are defined on deterministic
states, which are mappings $S:\mathbb{PV}\rightarrow\mathbb{Z}$. Let
$\mathbb{S}$ be the set of all deterministic states. Each state
$S\in\mathbb{S}$ is a description of the value of each program variable.
Consequently, the semantics of the arithmetic expressions is $[\\![E]\\!]:\
\mathbb{S}\rightarrow\mathbb{Z}$ which assigns an integer value to each
deterministic state. Similarly, the semantics of Boolean expressions is
$[\\![B]\\!]:\ \mathbb{S}\rightarrow\mathbb{B}$ that maps each state to a
Boolean value.

######  Definition 3 (Semantics of deterministic expressions).

The semantics of deterministic expressions are defined inductively as follows:

$[\\![X]\\!]S$ | = | $S(X)$
---|---|---
$[\\![n]\\!]S$ | = | $n$
$[\\![E_{1}\ aop\ E_{2}]\\!]S$ | = | $[\\![E_{1}]\\!]S\ aop\ [\\![E_{2}]\\!]S$
$[\\![\top]\\!]S$ | = | $\top$
$[\\![\bot]\\!]S$ | = | $\bot$
$[\\![E_{1}\ rop\ E_{2}]\\!]S$ | = | $[\\![E_{1}]\\!]S\ rop\ [\\![E_{2}]\\!]S$
$[\\![\neg B]\\!]S$ | = | $\neg[\\![B]\\!]S$
$[\\![B_{1}\wedge B_{2}]\\!]S$ | = | $[\\![B_{1}]\\!]S\wedge\ [\\![B_{2}]\\!]S$

###  2.2 Commands

We use a command called random assignment that allows programs to exhibit
probabilistic behaviors and use quantum operations such as unitary operation
and measurement to exhibit quantum computation. Let
$\mathbb{QV}=\\{q_{1},\ldots,q_{m}\\}$ be a finite set of quantum variables.

######  Definition 4 (Syntax of command expressions).

The commands are defined inductively as follows:

$C:=skip\mid X\leftarrow E\mid X\xleftarrow[]{\$}R\mid C_{1};C_{2}\mid if\ B\
then\ C_{1}\ else\ C_{2}\mid while\mbox{ }B\mbox{ }do\mbox{ }C\mid$

$U[\overline{q}]\mid X\leftleftarrows q_{i}$

where $R=\\{a_{1}:r_{1},\cdots,a_{n}:r_{n}\\}$ in which
$\\{r_{1},\cdots,r_{n}\\}$ is a set of integers and $a_{1},\ldots,a_{n}$ are
real numbers such that $0<a_{i}<1$ and $a_{1}+\ldots+a_{n}=1$.

The command $skip$ represents a null command that does not do anything.
$X\leftarrow E$ is the normal assignment. $X\xleftarrow[]{\$}R$ is the random
assignment which can be read as a value $r_{i}$ is selected randomly with
probability $a_{i}$ and assigned to $X$. $C_{1};C_{2}$ stands for the
sequential execution of $C_{1}$ and $C_{2}$. The next two expressions are the
classical conditional choice and loop, respectively. In terms of quantum
commands, $U[\overline{q}]$ applies the unitary operator $U$ to the quantum
variables indicated by $\overline{q}$. The command $X\leftleftarrows q_{i}$
measures the quantum variables $q_{i}$ using the computational basis and
stores the measurement result in the classical variable $X$. The basics of
quantum computation can be referred to in Appendix A.

For every quantum variable $q_{i}$, we assume a two-dimensional Hilbert space
$\mathcal{H}_{i}$. Let
$\mathcal{H}=\mathcal{H}_{1}\otimes\ldots\otimes\mathcal{H}_{m}$ be the
Hilbert space of all quantum variables. A quantum state is a unit vector
$|u\rangle\in\mathcal{H}$. We assume that two unit vectors, which differ only
in a globe phase, represent the same quantum state. A pure classical-quantum
state (cq-state) is a pair $\theta=(S,|u\rangle)$ of a classical state and a
quantum state. We use $\theta_{c}$ to denote its classical part and
$\theta_{q}$ to denote its quantum part. That is, we let $\theta_{c}=S$ and
$\theta_{q}=|u\rangle$.

Let $\mathbb{PS}$ be the set of all pure cq-states. A probabilistic cq-state
(also called mixed cq-state), denoted by $\Theta$, is a probability sub-
distribution on pure cq-states, i.e. $\Theta:\mathbb{PS}\to[0,1]$ such that
$\Sigma_{\theta\in\mathbb{PS}}\Theta(\theta)\leq 1$. It is worth noting that
we utilize subdistributions considering the cases where some programs may
never terminate. We use $D(\mathbb{PS})$ to denote the set of all
probabilistic cq-states.

For an arbitrary pure cq-state $\theta\in\mathbb{PS}$, $\widehat{\theta}$
denotes a special probabilistic cq-state which maps $\theta$ to 1 and maps any
other state to 0, i.e., a point distribution.

######  Definition 5 (Semantics of command expressions).

The semantics of command expressions is a function $[\\![C]\\!]\in
D(\mathbb{PS})\rightarrow D(\mathbb{PS})$. It is defined inductively as
follows:

  * •

$[\\![skip]\\!](\Theta)=\Theta$

  * •

$[\\![X\leftarrow E]\\!](\widehat{\theta})=\widehat{\theta^{\prime}}$, where
$\theta^{\prime}_{c}=\theta_{c}[X\mapsto[\\![E]\\!]\theta_{c}]$,
$\theta^{\prime}_{q}=\theta_{q}$.

  * •

$[\\![X\leftarrow
E]\\!](\Theta)=\displaystyle\sum\limits_{\theta\in\mathbb{PS}}\Theta(\theta)\cdot\widehat{\theta^{\prime}}$,
where $\widehat{\theta^{\prime}}=[\\![X\leftarrow E]\\!](\widehat{\theta})$.

  * •

$[\\![X\xleftarrow{\$}\\{a_{1}:r_{1},...,a_{n}:r_{n}\\}]\\!](\Theta)=\displaystyle\sum_{i=1}^{n}a_{i}[\\![X\leftarrow
r_{i}]\\!](\Theta)$.

  * •

$[\\![C_{1};\ C_{2}]\\!](\Theta)=[\\![C_{2}]\\!]([\\![C_{1}]\\!](\Theta))$

  * •

$[\\![if\ B\ then\ C_{1}\ else\
C_{2}]\\!](\Theta)=[\\![C_{1}]\\!](\downarrow_{B}(\Theta))+[\\![C_{2}]\\!](\downarrow_{\neg
B}(\Theta))$.

  * •

$[\\![while\mbox{ }B\mbox{ }do\mbox{
}C]\\!](\Theta)=\displaystyle\sum_{i=0}^{\infty}\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{i}(\Theta))$.

  * •

$[\\![U[\overline{q}]]\\!](\widehat{\theta})=\widehat{\theta^{\prime}}$, where
$\theta^{\prime}_{c}=\theta_{c}$,$\theta_{q}^{\prime}=U_{\overline{q}}\theta_{q}$.

  * •

$[\\![U[\overline{q}]]\\!](\Theta)=\displaystyle\sum\limits_{\theta\in\mathbb{PS}}\Theta(\theta)\cdot[\\![U[\overline{q}]]\\!](\widehat{\theta})$.

  * •

$[\\![X\leftleftarrows
q_{i}]\\!](\widehat{\theta})=\displaystyle\sum\limits_{j=0}^{1}p_{j}\widehat{\theta_{j}}$,
where $p_{j}=\textbf{Tr}((|j\rangle\langle j|\otimes
I_{-i})\theta_{q}\theta_{q}^{\dagger})$, $\theta_{j,c}=\theta_{c}[X\mapsto
j]$, $\theta_{j,q}=\frac{(|j\rangle\langle j|\otimes
I_{-i})\theta_{q}}{\sqrt{p_{j}}}$ if $p_{j}\neq 0$, otherwise
$\theta_{j,q}=(|j\rangle\langle j|\otimes I_{-i})\theta_{q}$.

  * •

$[\\![X\leftleftarrows
q_{i}]\\!](\Theta)=\displaystyle\sum\limits_{\theta\in\mathbb{PS}}\Theta(\theta)\cdot[\\![U[\overline{q}]]\\!](\widehat{\theta})$.

The command $skip$ changes nothing. We write
$\theta_{c}[X\mapsto[\\![E]\\!]\theta_{c}]$ to denote the classical state that
assigns the same values to the variables as $\theta_{c}$, except the variable
$X$ is assigned the value $[\\![E]\\!]\theta_{c}$. Here,
$\downarrow_{B}(\Theta)$ denotes the distribution $\Theta$ restricted to those
pure states that make $B$ true. Formally, $\downarrow_{B}(\Theta)=\Lambda$
with $\Lambda(\theta)=\Theta(\theta)$ if $[\\![B]\\!]\theta_{c}=\top$ and
$\Lambda(\theta)=0$ otherwise. So the condition choice can split any $\Theta$
into two parts with respect to a boolean expression $B$, one of which is the
sub-distribution of states that satisfy $B$ and then execute the command
$C_{1}$, the remaining execute the command $C_{2}$.

###  2.3 Proof system with deterministic assertions

Now we define deterministic assertions based on deterministic expressions.

######  Definition 6 (Syntax of deterministic assertions).

The deterministic assertions are defined by the following BNF:

$\phi:=\top\mid\bot\mid P_{j}^{0}\mid P_{j}^{1}\mid(e\ rop\
e)\mid\neg\phi\mid(\phi\wedge\phi)\mid\forall
x\phi\mid[U_{\overline{q}}]\phi\mid[\mathfrak{P}_{j}^{0}]\phi\mid[\mathfrak{P}_{j}^{1}]\phi\mid\bigwedge\limits_{i=0}^{\infty}\phi_{i}$

where $e$ represents arithmetic expression build on
$\mathbb{LV}\cup\mathbb{PV}$:

$e:=n\mid X\mid x\mid(e\ aop\ e)$.

Here, $\top$ and $\bot$ are boolean constants which represent true and false,
respectively. $P^{i}$ is the projector $|i\rangle\langle i|$. We restrict the
logical operators to the classical operators $\neg$ and $\wedge$ since $\vee$
and $\to$ can be expressed in the standard way. The formula $\forall x\phi$
applies a universal quantifier to the logical variable $x$ in formula $\phi$.
$[U_{\overline{q}}]\phi$ intuitively means that $\phi$ is true after the
unitary operation $U$ is applied on the qubits $\overline{q}$.
$[\mathfrak{P}_{j}^{i}]\phi$ means that $\phi$ is true after the qubit $q_{j}$
is projected to state $|i\rangle$. $\bigwedge_{i=0}^{\infty}\phi_{i}$ is the
infinitary conjunction. We will need an infinitary conjunction to define the
weakest preconditions.

An interpretation $I:\mathbb{LV}\mapsto\mathbb{Z}$ is a function that maps
logical variables to integers. Given an interpretation $I$ and a pure cq-state
$\theta$, the semantics of $e$ is defined as follows.

$[\\![n]\\!]^{I}\theta$ | = | $n$
---|---|---
$[\\![X]\\!]^{I}\theta$ | = | $\theta_{c}(X)$
$[\\![x]\\!]^{I}\theta$ | = | $I(x)$
$[\\![E_{1}\ aop\ E_{2}]\\!]^{I}\theta$ | = | $[\\![E_{1}]\\!]^{I}\theta\ aop\ [\\![E_{2}]\\!]^{I}\theta$

The semantics of a deterministic assertion, to be defined in the next
definition, is denoted by
$[\\![\phi]\\!]^{I}=\\{\theta:\theta\models^{I}\phi\\}$ which represents the
set of all states satisfying $\phi$.

######  Definition 7 (Semantics of deterministic assertions).

The semantics of deterministic assertions is defined inductively as follows:

$[\\![\top]\\!]^{I}$ |  = |  $\mathbb{PS}$
---|---|---
$[\\![\bot]\\!]^{I}$ |  = |  $\emptyset$
$[\\![P_{j}^{i}]\\!]^{I}$ |  = |  $\\{\theta\in\mathbb{PS}\mid\textbf{Tr}(P^{i}\textbf{Tr}_{-j}(\theta_{q}\theta_{q}^{\dagger}))=1\\}$
$[\\![e_{1}\ rop\ e_{2}]\\!]^{I}$ |  = |  $\\{\theta\in\mathbb{PS}\mid[\\![e_{1}]\\!]^{I}\theta_{c}\ rop\ [\\![e_{2}]\\!]^{I}\theta_{c}=\top\\}$
$[\\![\neg\phi]\\!]^{I}$ |  = |  $\mathbb{PS}\backslash[\\![\phi]\\!]^{I}$
$[\\![\phi_{1}\wedge\phi_{2}]\\!]^{I}$ |  = |  $[\\![\phi_{1}]\\!]^{I}\cap[\\![\phi_{2}]\\!]^{I}$
$[\\![\forall x\phi]\\!]^{I}$ |  $=$ |  $\\{\theta\mid$ for all integer $n$ and $I^{\prime}=I[x\mapsto n]$, $\theta\in[\\![\Phi]\\!]^{I^{\prime}}\\}$
$[\\![[U_{\overline{q}}]\phi]\\!]^{I}$ |  $=$ |  $\\{\theta\mid U_{\overline{q}}\theta\models^{I}\phi\\}$, here $U_{\overline{q}}\theta$ is short for $(\theta_{c},U_{\overline{q}}\theta_{q})$
$[\\![[\mathfrak{P}_{j}^{i}]\phi]\\!]^{I}$ |  $=$ |  $\\{\theta\mid\theta^{\prime}\models^{I}\phi,$ where $\theta^{\prime}_{c}=\theta_{c}$, $\theta^{\prime}_{q}=\frac{(P^{i}_{j}\otimes I_{-j})\theta_{q}}{\sqrt{p_{i}}}$, $p_{i}=\textbf{Tr}((P^{i}_{j}\otimes I_{-j})\theta_{q}\theta_{q}^{\dagger})$ and $p_{i}>0$ $\\}$
$[\\![\bigwedge\limits_{i=0}^{\infty}\phi_{i}]\\!]$ |  $=$ |  $\bigcap_{i=0}^{\infty}[\\![\phi_{i}]\\!]^{I}$

Most of the above cases are self-explanatory. $[U_{\overline{q}}]\phi$ is true
on these pure cq-states which renders $\phi$ true after applied the unitary
operator $U$ on quantum variables $\overline{q}$. $[\mathfrak{P}_{j}^{i}]\phi$
is satisfied on a pure cq-state $\theta$ if and only if after projecting
variable $q_{i}$ in $\theta_{q}$ to the quantum state $|i\rangle$, the
obtained pure cq-state $\theta^{\prime}$ satisfies $\phi$.

Definition 7 gives the semantics of deterministic formulas over pure cq-
states. We straightforwardly extend the semantics to probabilistic states as
follows:

$\Theta\models^{I}\phi$ iff for each support $\theta$ of $\Theta$,
$\theta\in[\\![\phi]\\!]^{I}$.

We call it possibility semantics because the definition intuitively means that
a deterministic formula $\phi$ is true on a probabilistic cq-state $\Theta$ if
and only if $\phi$ is true on all possible pure cq-state.

A QHL proof system consists of Hoare triples. A Hoare triple
$\\{\phi\\}C\\{\psi\\}$ is valid if for each pure cq-state that satisfies
$\phi$, after the termination of the execution command $C$, the mixed
consequence of the cq-state satisfies $\psi$. Formally,

$\models\\{\phi\\}C\\{\psi\\}$ if for each interpretation $I$ and each pure
cq-state $\theta$, if $\theta\models^{I}\phi$, then
$[\\![C]\\!](\widehat{\theta})\models^{I}\psi$.

We now build a proof system (QHLd) for the derivation of Hoare triples with
deterministic assertions.

######  Definition 8 (Proof system QHLd).

The proof system QHLd consists of the following inference rules:

$SKIP:$ | $\frac{}{\vdash\\{\phi\\}\texttt{skip}\\{\phi\\}}$
---|---
$AS:$ | $\frac{}{\vdash\\{\phi[X/E]\\}X\leftarrow E\\{\phi\\}}$
$PAS:$ | $\frac{}{\vdash\\{\phi[X/k_{1}]\wedge\ldots\wedge\phi[X/k_{n}]\\}X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}\\{\phi\\}}$
$SEQ:$ | $\frac{\vdash\\{\phi\\}C_{1}\\{\phi_{1}\\}\quad\vdash\\{\phi_{1}\\}C_{2}\\{\phi_{2}\\}}{\vdash\\{\phi\\}C_{1};C_{2}\\{\phi_{2}\\}}$
$IF:$ | $\frac{\vdash\\{\phi\wedge B\\}C_{1}\\{\psi\\}\quad\vdash\\{\phi\wedge\neg B\\}C_{2}\\{\psi\\}}{\vdash\\{\phi\\}\texttt{if}\ B\ \texttt{then}\ C_{1}\ \texttt{else}\ C_{2}\\{\psi\\}}$
$WHILE:$ | $\frac{\vdash\\{\phi\wedge B\\}C\\{\phi\\}}{\vdash\\{\phi\\}\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{ }C\\{\phi\wedge\neg B\\}}$
$UNITARY:$ | $\frac{}{\vdash\\{[U_{\overline{q}}]\phi\\}U[\overline{q}]\\{\phi\\}}$
$MEASURE:$ | $\frac{}{\vdash\\{([\mathfrak{P}^{0}_{j}]\phi[X/0]\vee P^{1}_{j})\wedge([\mathfrak{P}^{1}_{j}]\phi[X/1]\vee P^{0}_{j})\\}X\leftleftarrows q_{j}\\{\phi\\}}$
$CONS:$ | $\frac{\models\phi^{\prime}\rightarrow\phi\quad\vdash\\{\phi\\}C\\{\psi\\}\quad\models\psi\rightarrow\psi^{\prime}}{\vdash\\{\phi^{\prime}\\}C\\{\psi^{\prime}\\}}$

###  2.4 Soundness and completeness

######  Theorem 2.1 (Soundness).

The proof system QHLd is sound, $i.e.$, for all deterministic formula $\phi$
and $\psi$ and command $C$, $\vdash\\{\phi\\}C\\{\psi\\}$ implies
$\models\\{\phi\\}C\\{\psi\\}$.

###### Proof.

Please refer to Appendix Theorem. ∎

In order to determine the completeness, we use the method of weakest
preconditions denoted by $wp(C,\psi)$. Essentially, we want to find the
largest set of states (represented as an assertion) from which if a program
$C$ is executed, the resulting states satisfy the given postcondition $\psi$,
and $[\\![wp(C,\psi)]\\!]$ represents this set. This set is considered to be a
precondition since $\models\\{wp(C,\psi)\\}C\\{\psi\\}$ and it is also the
weakest precondition because if $\models\\{\phi\\}C\\{\psi\\}$, then
$\models\phi\rightarrow wp(C,\psi)$. Although the weakest precondition is a
semantic notion, we can represent it syntactically using $wp(C,\psi)$. In this
paper, we will treat the weakest precondition as a syntactic notion when it is
more convenient for our constructions and proofs.

######  Definition 9 (Weakest precondions).

The weakest precondition is defined inductively on the structure of commands
as follows:

  1. 1.

$wp(skip,\phi)=\phi$.

  2. 2.

$wp(X\leftarrow E,\phi)=\phi[X/E]$.

  3. 3.

$wp(X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\},\phi)=\phi[X/k_{1}]\wedge\ldots\wedge\phi[X/k_{n}]$.

  4. 4.

$wp(C_{1};C_{2},\phi)=wp(C_{1},wp(C_{2},\phi))$.

  5. 5.

$wp(if\ B\ then\ C_{1}\ else\ C_{2},\phi)=(B\wedge wp(C_{1},\phi))\vee(\neg
B\wedge wp(C_{2},\phi))$.

  6. 6.

$wp(while\mbox{ }B\mbox{ }do\mbox{
}C,\phi)=\bigwedge\limits_{k=0}^{\infty}\psi_{k}$, where $\psi_{0}=\top$ and
$\psi_{i+1}=(B\wedge wp(C,\psi_{i}))\vee(\neg B\wedge\phi)$.

  7. 7.

$wp(U[\overline{q}],\phi)=[U_{\overline{q}}]\phi$.

  8. 8.

$wp(X\leftleftarrows q_{j},\phi)=([\mathfrak{P}^{0}_{j}]\phi[X/0]\vee
P^{1}_{j})\wedge([\mathfrak{P}^{1}_{j}]\phi[X/1]\vee P^{0}_{j})$.

Some readers may be wondering if it is possible to define $wp(while\mbox{
}B\mbox{ }do\mbox{ }C,\phi)$ without using an infinitary conjunction. In
classical and probabilistic Hoare logic, the weakest precondition of the
while-loop can be defined using G$\ddot{o}$del’s $\beta$ predicate without an
infinitary conjunction. Unfortunately, this does not appear to be possible in
the current setting. The reason for this is that in our QHL, the number of
pure cq-states is uncountable, whereas in classical and probabilistic Hoare
logic, the number of (pure) states is countable. This is why they can be
encoded by natural numbers, which is a crucial step in defining the weakest
precondition.

If we want to remove an infinitary conjunction, we have to reduce the number
of pure cq-states to countable infinity. This is possible by, for example,
restricting unitary operators to the Clifford+T family and letting the set of
cq-states be the minimal set that contains $|0\rangle$ and is closed under the
Clifford+T operations. However, the rigorous study of this issue will be left
for future work.

######  Theorem 2.2.

$\Theta\models^{I}wp(C,\phi)$ iff $[\\![C]\\!](\Theta)\models^{I}\phi$.

###### Proof.

Please refer to Appendix Theorem. ∎

######  Proposition 1.

It holds that $\vdash\\{wp(C,\phi)\\}C\\{\phi\\}$.

###### Proof.

Please refer to Appendix Proposition. ∎

######  Lemma 1.

If $\models\\{\phi\\}C\\{\psi\\}$ then $\models\phi\rightarrow wp(C,\psi)$

###### Proof.

If $\theta\models\phi$, then $[\\![C]\\!]\theta\models\psi$. Therefore,
$\theta\models wp(C,\psi)$.

∎

######  Corollary 1 (Completeness).

If $\models\\{\phi\\}C\\{\psi\\}$, then $\vdash\\{\phi\\}C\\{\psi\\}$.

###### Proof.

If $\models\\{\phi\\}C\\{\psi\\}$, then $\models\phi\rightarrow wp(C,\psi)$.
By Proposition 1, we know $\vdash\\{wp(C,\psi)\\}C\\{\psi\\}$. Then
$\vdash\\{\phi\\}C\\{\psi\\}$ is obtained by applying the inference rule
(CONS). ∎

We have already established that QHLd is both sound and complete, but it only
deals with deterministic formulas. Probabilistic assertions, on the other
hand, are more expressive, as they can describe the probabilistic nature of
probabilistic cq-states, such as the probability of $X>3$ being $\frac{1}{2}$.
The next section delves into probabilistic assertions and their corresponding
proof system. To begin, a useful lemma is presented, highlighting the
relationship between the WHILE command and the IF command, which plays a
significant role in the completeness proof in the following section.

######  Lemma 2.

For all $i\geq 0$ and all pure cq-state $\theta$, if $\theta\models^{I}\neg
wp(C^{0},\neg B)\wedge\ldots\wedge\neg wp(C^{i-1},\neg B)\wedge wp(C^{i},\neg
B)$, then

$[\\![\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{
}C]\\!](\widehat{\theta})=[\\![(\texttt{if}\mbox{ }B\mbox{
}\texttt{then}\mbox{ }C\mbox{ }\texttt{else}\mbox{
}\texttt{skip})^{i}]\\!](\widehat{\theta}).$

###### Proof.

Please refer to Appendix Lemma. ∎

##  3 Quantum Hoare logic with probabilistic assertion

###  3.1 Probabilistic formulas

To better describe the probabilistic aspects of cq-states, it is inevitable to
expand deterministic formulas into probabilistic formulas. To achieve this, we
begin by defining real expressions (also known as probabilistic expressions)
which serve as the fundamental components of probabilistic formulas.

######  Definition 10 (Real expressions).

Let $\mathbb{RV}$ be a set of real variables. The real expression $r$ is
defined as follows:

$r:=a\mid\mathfrak{x}\mid\mathbb{P}(\phi)\mid r\mbox{ }aop\mbox{
}r\mid\phi\Rightarrow Q\mid\sum\limits_{i=0}^{\infty}r_{i}$

Here, $a\in\mathbb{R}$ is a real number, $\mathfrak{x}\in\mathbb{RV}$ is a
real variable, and $aop$ is arithmetic operations on real numbers such as
$+,-,\times,\ldots$. $\mathbb{P}(\phi)$ is the probability that a
deterministic assertion $\phi$ is true. $Q$ is a projective operator on
$\mathcal{H}$, which means that $Q$ is self-adjoint and idempotent. A cq-
conditional $\phi\Rightarrow Q$ denotes the probability of observing $Q$ in
those states where $\phi$ is true. $\sum\limits_{i=0}^{\infty}r_{i}$ is an
infinite summation.

To decide the value of logical variable $x$, an interpretation $I$ is used to
map logical variables to integers and real variables to real numbers.

######  Definition 11 (Semantics of real expressions).

Given an interpretation $I$ and a probabilistic cq-state $\Theta$, the
semantics of real expressions are defined inductively as follows.

  * •

$[\\![a]\\!]^{I}_{\Theta}=a$.

  * •

$[\\![\mathfrak{x}]\\!]^{I}_{\Theta}=I(\mathfrak{x})$.

  * •

$[\\![\mathbb{P}(\phi)]\\!]^{I}_{\Theta}=\sum\limits_{\theta\models^{I}\phi}\Theta(\theta)$.

  * •

$[\\![r_{1}\mbox{ }aop\mbox{
}r_{2}]\\!]^{I}_{\Theta}=[\\![r_{1}]\\!]^{I}_{\Theta}\mbox{ }aop\mbox{
}[\\![r_{2}]\\!]^{I}_{\Theta}$.

  * •

$[\\![\phi\Rightarrow
Q]\\!]^{I}_{\Theta}=\sum\limits_{\theta\models\phi}\Theta(\theta)\textbf{Tr}(Q\theta_{q}\theta_{q}^{\dagger})$.

  * •

$[\\![\sum\limits_{i=0}^{\infty}r_{i}]\\!]^{I}_{\Theta}=\sum\limits_{i=0}^{\infty}[\\![r_{i}]\\!]^{I}_{\Theta}$

A real number $a$ is interpreted as itself on a probabilistic cq-state. The
probability that the deterministic formula $\phi$ holds over some
probabilistic cq-state is denoted by $\mathbb{P}(\phi)$. This probability can
be computed by adding up the probabilities of all pure cq-states where $\phi$
is true. $r_{1}\ aop\ r_{2}$ characterizes the arithmetic calculation between
two real expressions. Additionally, the summation of infinitely many values of
$r_{i}$s is represented by $\sum\limits_{i=0}^{\infty}r_{i}$.

Now we define probabilistic formulas (assertions). These formulas typically
involve two real expressions and are used to compare probabilities. For
instance, it is common to see a probabilistic formula like
$\mathbb{P}(X>1)<\frac{1}{2}$, which compares two probabilities.

######  Definition 12 (Syntax of probabilistic formulas).

Probabilistic formulas are defined inductively as follows.

$\Phi=(r\mbox{ }rop\mbox{ }r)\mid\neg\Phi\mid(\Phi\wedge\Phi)$

where $r$ is a real expression.

For example,
$(\mathbb{P}([U_{\overline{q}}](X>0))>\frac{1}{2})\wedge\neg(\mathbb{P}([\mathfrak{P}_{1}^{0}](X>1))<(P_{1}^{0}\Rightarrow
Q))$ is a well-formed probabilistic formula.

######  Definition 13 (Semantics of probabilistic formulas).

Given an interpretation $I$, the semantics of the probabilistic assertion is
defined in the probabilistic cq-states $\Theta$ as follows:

  * •

$\Theta\models^{I}r_{1}\mbox{ }rop\mbox{ }r_{2}$ if
$[\\![r_{1}]\\!]^{I}_{\Theta}\mbox{ }rop\mbox{
}[\\![r_{2}]\\!]^{I}_{\Theta}=\top$

  * •

$\Theta\models^{I}\neg\Phi$ if not $\Theta\models^{I}\Phi$

  * •

$\Theta\models^{I}\Phi_{1}\wedge\Phi_{2}$ if $\Theta\models^{I}\Phi_{1}$ and
$\Theta\models^{I}\Phi_{2}$

###  3.2 Proof system with probabilistic assertions

Now we delve deeper into the Hoare triples $\\{\Phi\\}C\\{\Psi\\}$,
specifically those with probabilistic formulas, and the challenge of
determining the weakest preconditions for given commands and probabilistic
formulas. To address this, we extend the concept of weakest preterms in
probabilistic Hoare logic [5, 21] to the quantum setting. The concept of
weakest preterm is defined as the term whose interpretation on the initial
probabilistic cq-state is the same as the interpretation of the given term
(real expression) on the resulting cq-state after executing a given command
$C$. To define the weakest preterm, we also utilize the notion of conditional
term from Chadha et al. [5, 21].

######  Definition 14 (Conditional terms).

The conditional term $r/B$ of a real expression $r$ with a Boolean formula $B$
(a deterministic formula) is inductively defined as follows.

  * •

$a/B:=a$

  * •

$\mathfrak{x}/B:=\mathfrak{x}$

  * •

$\mathbb{P}(\phi)/B:=\mathbb{P}(\phi\wedge B)$

  * •

$(r_{1}\mbox{ }aop\mbox{ }r_{2})/B:=r_{1}/B\mbox{ }aop\mbox{ }r_{2}/B$

  * •

$(\phi\Rightarrow Q)/B:=(\phi\wedge B)\Rightarrow Q$

  * •

$(\sum\limits_{i=0}^{\infty}r_{i})/B=\sum\limits_{i=0}^{\infty}(r_{i}/B)$

A conditional term intuitively denotes a probability under some condition
described by a deterministic formula, which is shown by the next lemma.

######  Lemma 3.

Given an arbitrary probabilistic cq-state $\Theta$ and an interpretation $I$,
it holds that
$[\\![r/B]\\!]^{I}_{\Theta}=[\\![r]\\!]^{I}_{\downarrow_{B}\Theta}$.

###### Proof.

We only consider the non-trivial cases where $r$ is in the form of
$\mathbb{P}(\phi)$ or $\phi\Rightarrow Q$:

  * •

When $r=\mathbb{P}(\phi)$,
$[\\![\mathbb{P}(\phi)/B]\\!]^{I}_{\Theta}=[\\![\mathbb{P}(\phi\wedge
B)]\\!]^{I}_{\Theta}=[\\![\mathbb{P}(\phi)]\\!]^{I}_{\downarrow_{B}\Theta}$.

  * •

When $r=\phi\Rightarrow Q$, $[\\![(\phi\Rightarrow
Q)/B]\\!]^{I}_{\Theta}=[\\![(\phi\wedge B)\Rightarrow
Q]\\!]^{I}_{\Theta}=\sum\limits_{\theta\models\phi\wedge
B}\Theta(\theta)\textbf{Tr}(Q\theta_{q}\theta_{q}^{\dagger})=\sum\limits_{\theta\models\phi}\downarrow_{B}\Theta(\theta)\textbf{Tr}(Q\theta_{q}\theta_{q}^{\dagger})=[\\![\phi\Rightarrow
Q]\\!]^{I}_{\downarrow_{B}\Theta}$.

∎

###  3.3 Weakest preterms calculus and weakest precondition

We are ready to define the weakest preterms now. Defining the weakest preterms
for a real expression $a$, $\mathfrak{x}$, and $r_{1}\ aop\ r_{2}$ is
straightforward. With regard to $\mathbb{P}(\phi)$ and $\phi\Rightarrow Q$, we
need to divide the cases by different commands. Those cases with non-quantum
commands, especially with the while-loop, are essentially the same as their
analogues in probabilist Hoare logic in [21].

######  Definition 15 (Weakest preterms).

The weakest preterm of a real expression $r$ with command $C$ is inductively
defined as follows.

  1. 1.

$pt(C,a)=a$

  2. 2.

$pt(C,\mathfrak{x})=\mathfrak{x}$

  3. 3.

$pt(C,r_{1}\mbox{ }aop\mbox{ }r_{2})=pt(C,r_{1})\mbox{ }aop\mbox{
}pt(C,r_{2})$

  4. 4.

$pt(C,\sum\limits_{i\in K}r_{i})=\sum\limits_{i\in K}pt(C,r_{i})$

  5. 5.

$pt(\texttt{skip},\mathbb{P}(\phi))=\mathbb{P}(\phi)$

  6. 6.

$pt(X\leftarrow E,\mathbb{P}(\phi))=\mathbb{P}(\phi[X/E])$

  7. 7.

$pt(X\xleftarrow[]{\$}\\{a_{1}:k_{1},\ldots,a_{n}:k_{n}\\},\mathbb{P}(\phi))=$
$a_{1}\mathbb{P}(\phi[X/k_{1}]\wedge\neg\phi[X/k_{2}]\wedge\ldots\neg\phi[X/k_{n}])+$
$a_{2}\mathbb{P}(\neg\phi[X/k_{1}]\wedge\phi[X/k_{2}]\wedge\neg\phi[X/k_{3}]\wedge\ldots\wedge\neg\phi[X/k_{n}])+\ldots+$
$a_{n}\mathbb{P}(\neg\phi[X/k_{1}]\wedge\ldots\wedge\neg\phi[X/k_{n-1}]\wedge\phi[X/k_{n}])+$
$(a_{1}+a_{2})\mathbb{P}(\phi[X/k_{1}]\wedge\phi[X/k_{2}]\wedge\neg\phi[X/k_{3}]\wedge\ldots\wedge\neg\phi[X/k_{n}])+\ldots+(a_{1}+\ldots+a_{n})\mathbb{P}(\phi[X/k_{1}]\wedge\ldots\wedge\phi[X/k_{n}])$

  8. 8.

$pt(U[\overline{q}],\mathbb{P}(\phi))=\mathbb{P}([U_{\overline{q}}]\phi)$

  9. 9.

$pt(X\leftleftarrows q_{j},\mathbb{P}(\phi))=(\top\Rightarrow
P^{0}_{j})\mathbb{P}([\mathfrak{P}^{0}_{j}]\phi[X/0])+(\top\Rightarrow
P^{1}_{j})\mathbb{P}([\mathfrak{P}^{1}_{j}]\phi[X/1])+\mathbb{P}([P_{j}^{0}]\phi[X/0]\wedge[P_{j}^{1}]\phi[X/1])$

  10. 10.

$pt(C_{1};C_{2},\mathbb{P}(\phi))=pt(C_{1},pt(C_{2},\mathbb{P}(\phi)))$

  11. 11.

$pt(\texttt{if}\ B\ \texttt{then}\ C_{1}\ \texttt{else}\
C_{2},\mathbb{P}(\phi))=pt(C_{1},\mathbb{P}(\phi))/B+pt(C_{2},\mathbb{P}(\phi))/(\neg
B)$

  12. 12.

$pt(\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{
}C,\mathbb{P}(\phi))=\displaystyle\sum_{i=0}^{\infty}T_{i}$, in which $T_{i}$
is defined via the following procedure. We use the following abbreviation.

     * •

$wp(i)$ is short for $\neg wp(C^{0},\neg B)\wedge\ldots\wedge\neg
wp(C^{i-1},\neg B)\wedge wp(C^{i},\neg B)$

     * •

$wp(\infty)$ is short for $\displaystyle\bigwedge_{i=0}^{\infty}\neg
wp(C^{i},\neg B)$

     * •

$WL$ is short for $\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{ }C$

     * •

$IF$ is short for $\texttt{if}\ B\ \texttt{then}\ C\ \texttt{else}\mbox{
}\texttt{skip}$

     * •

$SUM$ is short for
$\displaystyle\sum_{i=0}^{\infty}(\mathbb{P}(wp(i))(pt((IF)^{i},\mathbb{P}(\phi))/(wp(i))))$

For any probabilistic cq-state $\Theta$, we let
$\Theta_{0}=\downarrow_{wp(\infty)}(\Theta)$,
$\Theta_{i+1}=\downarrow_{wp(\infty)}([\\![C]\\!]\Theta_{i})$.

     * •

Let $T_{0}=SUM$.

     * •

Let $T_{1}$ be the unique real expression such that

$[\\![T_{1}]\\!]_{\Theta}=[\\![\mathbb{P}(wp(\infty))]\\!]_{\Theta}[\\![SUM]\\!]_{[\\![C]\\!]\Theta_{0}}$

for all probabilistic cq-state $\Theta$. Equivalently,

$T_{1}=\mathbb{P}(wp(\infty))(pt(C,SUM)/wp(\infty)).$

     * •

Let $T_{2}$ be the unique real expression such that

$[\\![T_{2}]\\!]_{\Theta}=[\\![\mathbb{P}(wp(\infty))]\\!]_{\Theta}\mathbb{P}(wp(\infty))]\\!]_{[\\![C]\\!]\Theta_{0}}[\\![SUM]\\!]_{[\\![C]\\!]\Theta_{1}}$

for all probabilistic states $\Theta$. Equivalently, $T_{2}=$

$\mathbb{P}(wp(\infty))(pt(C,\mathbb{P}(wp(\infty)))/wp(\infty))(pt(C,pt(C,SUM)/wp(\infty))/wp(\infty))$

     * •

In general, we let $T_{i}$ be the unique real expression such that
$[\\![T_{i}]\\!]_{\Theta}=$

$[\\![\mathbb{P}(wp(\infty))]\\!]_{\Theta}[\\![\mathbb{P}(wp(\infty))]\\!]_{[\\![C]\\!]\Theta_{0}}\ldots$
$[\\![\mathbb{P}(wp(\infty))]\\!]_{[\\![C]\\!]\Theta_{i-2}}[\\![SUM]\\!]_{[\\![C]\\!]\Theta_{i-1}}$

for all probabilistic cq-state $\Theta$. Equivalently, let $f_{C,B}$ be the
function that maps a real expression $r$ to $f_{C,B}(r)=pt(C,r)/wp(\infty)$.
Then $T_{i}$ can be characterized by the following formula:

$T_{i}=f_{C,B}^{i}(SUM)\displaystyle\prod_{j=0}^{i-1}f_{C,B}^{j}(\mathbb{P}(wp(\infty))).$

Therefore,

$pt(\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{
}C,\mathbb{P}(\phi))=\displaystyle\sum_{i=0}^{\infty}f^{i}(SUM)\displaystyle\prod_{j=0}^{i-1}f^{j}(\mathbb{P}(wp(\infty))).$

  13. 13.

$pt(\texttt{skip},\phi\Rightarrow Q)=\phi\Rightarrow Q$

  14. 14.

$pt(X\leftarrow E,\phi\Rightarrow Q)=\phi[X/E]\Rightarrow Q$

  15. 15.

$pt(X\xleftarrow[]{\$}\\{a_{1}:k_{1},\ldots,a_{n}:k_{n}\\},\phi\Rightarrow
Q)=$
$a_{1}(\phi[X/k_{1}]\Rightarrow Q)+\ldots+a_{n}(\phi[X/k_{n}]\Rightarrow Q)$

  16. 16.

$pt(U[\overline{q}],\phi\Rightarrow Q)=[U_{\overline{q}}]\phi\Rightarrow
U^{\dagger}_{\overline{q}}QU_{\overline{q}}$

  17. 17.

$pt(X\leftleftarrows q_{j},\phi\Rightarrow Q)=(\phi[X/0]\Rightarrow
P^{0}_{j}QP^{0}_{j})+(\phi[X/1]\Rightarrow P^{1}_{j}QP^{1}_{j})$

  18. 18.

$pt(C_{1};C_{2},\phi\Rightarrow Q)=pt(C_{1},pt(C_{2},\phi\Rightarrow Q))$

  19. 19.

$pt(\texttt{if}\ B\ \texttt{then}\ C_{1}\ \texttt{else}\ C_{2},\phi\Rightarrow
Q)=$
$pt(C_{1},\phi\Rightarrow Q)/B+pt(C_{2},\phi\Rightarrow Q)/\neg B$

  20. 20.

$pt(WHILE,\phi\Rightarrow
Q)=pt(WHILE,\mathbb{P}(\psi))[\mathbb{P}(\psi)/(\phi\Rightarrow Q)]$

Note that $pt(WHILE,\mathbb{P}(\psi))[\mathbb{P}(\psi)/(\phi\Rightarrow Q)]$
is an informal notation. It means that $pt(WHILE,\phi\Rightarrow Q)$ is
obtained by replacing the appearance of $\mathbb{P}(\psi)$ in
$pt(WHILE,\mathbb{P}(\psi))$ by $(\phi\Rightarrow Q)$. The following lemma
shows that our definition of weakest preterm captures the intuition of weakest
preterm.

######  Lemma 4.

Given an arbitrary probabilistic cq-state $\Theta$, an interpretation $I$, a
command $C$, and a real expression $r$ (excluding cq conditionals),

$[\\![pt(C,r)]\\!]^{I}_{\Theta}=[\\![r]\\!]^{I}_{[\\![C]\\!]\Theta}$

###### Proof.

Please refer to Appendix Lemma. ∎

The major contribution of this paper is extending the concept of weakest
preterm from probabilistic Hoare logic to quanutum Hoare logic. With weakest
preterm at hand, we now straightforwardly define the weakest precondition of
probabilistic assertion and develop a proof system of QHL with probabilistic
assertion.

######  Definition 16 (Weakest precondition of probabilistic assertion).

  1. 1.

$WP(C,r_{1}\mbox{ }rop\mbox{ }r_{2})=pt(C,r_{1})\mbox{ }rop\mbox{
}pt(C,r_{2})$

  2. 2.

$WP(C,\neg\Phi)=\neg WP(C,\Phi)$

  3. 3.

$WP(C,\Phi_{1}\wedge\Phi_{2})=WP(C,\Phi_{1})\wedge WP(C,\Phi_{2})$

######  Theorem 3.1.

$\mu\models^{I}WP(C,\Phi)$ iff $[\\![C]\\!]\mu\models^{I}\Phi$.

We provide the proof in Appendix Theorem. The theorem mentioned above inspires
a definition for a QHL proof system with respect to probabilistic formulas in
a uniform manner. The proposed definition is
$\vdash\\{WP(C,\Phi)\\}C\\{\Phi\\}$, which applies to every command $C$ and
probabilistic formula $\Phi$. We will follow this construction with some minor
modifications.

###  3.4 Proof system with probabilistic assertions

######  Definition 17 (Proof system with probabilistic assertions).

The proof system of our QHL with probabilistic assertions consists of the
following inference rules:

$SKIP:$ | $\frac{}{\vdash\\{\Phi\\}\texttt{skip}\\{\Phi\\}}$
---|---
$AS:$ | $\frac{}{\vdash\\{WP(X\leftarrow E,\mbox{ }\Phi)\\}X\leftarrow E\\{\Phi\\}}$
$PAS:$ | $\frac{}{\vdash\\{WP(X\xleftarrow{\$}\\{a_{1}:r_{1},...,a_{n}:r_{n}\\},\mbox{ }\Phi)\\}X\xleftarrow{\$}\\{a_{1}:r_{1},...,a_{n}:r_{n}\\}\\{\Phi\\}}$
$UNITARY:$ | $\frac{}{\vdash\\{WP(U[\overline{q}],\mbox{ }\Phi)\\}U[\overline{q}]\\{\Phi\\}}$
$MEASURE:$ | $\frac{}{\vdash\\{WP(X\leftleftarrows q_{j},\mbox{ }\Phi)\\}X\leftleftarrows q_{j}\\{\Phi\\}}$
$SEQ:$ | $\frac{\vdash\\{\Phi\\}C_{1}\\{\Phi_{1}\\}\quad\vdash\\{\Phi_{1}\\}C_{2}\\{\Phi_{2}\\}}{\vdash\\{\Phi\\}C_{1};C_{2}\\{\Phi_{2}\\}}$
$IF:$ | $\frac{}{\vdash\\{WP(\texttt{if}\ B\ \texttt{then}\ C_{1}\ \texttt{else}\ C_{2},\mbox{ }\Phi)\\}\texttt{if}\ B\ \texttt{then}\ C_{1}\ \texttt{else}\ C_{2}\\{\Phi\\}}$
$WHILE:$ |  $\frac{}{\vdash\\{WP(\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{ }C,\mbox{ }\Phi)\\}\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{ }C\\{\Phi\\}}$,
$CONS:$ | $\frac{\models\Phi^{\prime}\rightarrow\Phi\quad\vdash\\{\Phi\\}C\\{\Psi\\}\quad\models\Psi\rightarrow\Psi^{\prime}}{\vdash\\{\Phi^{\prime}\\}C\\{\Psi^{\prime}\\}}$

With the rule (CONS) in our proof system, we can treat $WP(C,\Phi)$ as a
semantic notion: if $\models WP(C,\Phi)\leftrightarrow\Psi$, then $\Psi$ is
conceived as the weakest precondition of $\Phi$ with command $C$.

######  Lemma 5.

If $\models\\{\Phi\\}C\\{\Psi\\}$, then $\models\Phi\rightarrow WP(C,\Psi)$.

###### Proof.

Let $\mu$ be a probabilistic state such that $\mu\models\Phi$. Then
$[\\![C]\\!]\mu\models\Psi$. Then by Theorem 3.1 we know $\mu\models
WP(C,\Psi)$. ∎

######  Lemma 6.

For an arbitrary command $C$ and an arbitrary probabilistic formula $\Phi$, we
have $\vdash\\{WP(C,\Phi)\\}C\\{\Phi\\}$.

###### Proof.

Please refer to Appendix Lemma. ∎

######  Theorem 3.2.

The QHL proof system with probabilistic assertions is sound and complete.

###### Proof.

Soundness: the soundness of SKIP, AS, PAS, IF, WHILE follows from Theorem 3.1.
The soundness of SEQ and CON can be proved by simple deduction.

Completeness: Assume $\models\\{\Phi\\}C\\{\Psi\\}$, then
$\models\Phi\rightarrow WP(C,\Psi)$ by the lemma 5. Then by
$\vdash\\{WP(C,\Psi)\\}C\\{\Psi\\}$ and CONS we know
$\vdash\\{\Phi\\}C\\{\Psi\\}$.

∎

To showcase the expressive and inference power of our proposed QHL, we
formally verify two widely discussed quantum algorithms - Deutsch’s algorithm
and quantum teleportation. Due to page limitations, details are shown in
Appendix D.

##  4 Conclusion and future work

Inspired by the recent work on proving the relative completeness of
satisfaction-based probabilistic Hoare logic [21], in this paper we prove the
relative completeness of satisfaction-based quantum Hoare logic. The
completeness is proved in two steps. First, we establish a semantics and proof
system of Hoare triples with quantum programs and deterministic assertions.
Then, utilizing the weakest precondition of deterministic assertion, we
construct the weakest preterm calculus of probabilistic expressions. The
relative completeness of QHL is then obtained as a consequence of the weakest
preterm calculus.

It could be a good future project to extend this result to quantum relational
Hoare logic. However, we anticipate that achieving completeness for such a
logic could be quite challenging. Another possible direction is to implement
our QHL and use the implementation to verify numerous quantum algorithms.

## References

  * [1] Apt, K.R.: Ten years of hoare’s logic: A survey part II: nondeterminism. Theor. Comput. Sci. 28, 83–109 (1984). https://doi.org/10.1016/0304-3975(83)90066-X, https://doi.org/10.1016/0304-3975(83)90066-X
  * [2] Apt, K.R., de Boer, F.S., Olderog, E.: Verification of Sequential and Concurrent Programs. Texts in Computer Science, Springer (2009). https://doi.org/10.1007/978-1-84882-745-5, https://doi.org/10.1007/978-1-84882-745-5
  * [3] Apt, K.R., Boer, F.S., Olderog, E.R.: Verification of sequential and concurrent programs, vol. 2. Springer (2009)
  * [4] Apt, K.R., Olderog, E.R.: Fifty years of hoare’s logic. Formal Aspects of Computing 31, 751–807 (2019)
  * [5] Chadha, R., Cruz-Filipe, L., Mateus, P., Sernadas, A.: Reasoning about probabilistic sequential programs. Theoretical Computer Science 379(1-2), 142–165 (2007)
  * [6] Chadha, R., Mateus, P., Sernadas, A.: Reasoning about imperative quantum programs. In: Brookes, S.D., Mislove, M.W. (eds.) Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 2006, Genova, Italy, May 23-27, 2006. Electronic Notes in Theoretical Computer Science, vol. 158, pp. 19–39. Elsevier (2006). https://doi.org/10.1016/J.ENTCS.2006.04.003, https://doi.org/10.1016/j.entcs.2006.04.003
  * [7] Den Hartog, J., de Vink, E.P.: Verifying probabilistic programs using a hoare like logic. International journal of foundations of computer science 13(03), 315–340 (2002)
  * [8] Deng, Y., Feng, Y.: Formal semantics of a classical-quantum language. Theor. Comput. Sci. 913, 73–93 (2022). https://doi.org/10.1016/J.TCS.2022.02.017, https://doi.org/10.1016/j.tcs.2022.02.017
  * [9] Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975). https://doi.org/10.1145/360933.360975, https://doi.org/10.1145/360933.360975
  * [10] Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976), https://www.worldcat.org/oclc/01958445
  * [11] Feng, Y., Ying, M.: Quantum hoare logic with classical variables. ACM Transactions on Quantum Computing 2(4) (dec 2021). https://doi.org/10.1145/3456877, https://doi.org/10.1145/3456877
  * [12] Foley, M., Hoare, C.A.R.: Proof of a recursive program: Quicksort. Comput. J. 14(4), 391–395 (1971). https://doi.org/10.1093/COMJNL/14.4.391, https://doi.org/10.1093/comjnl/14.4.391
  * [13] Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (oct 1969). https://doi.org/10.1145/363235.363259, https://doi.org/10.1145/363235.363259
  * [14] Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages, Lecture Notes in Mathematics, vol. 188, pp. 102–116. Springer (1971). https://doi.org/10.1007/BFB0059696, https://doi.org/10.1007/BFb0059696
  * [15] Kakutani, Y.: A logic for formal verification of quantum programs. In: Datta, A. (ed.) Advances in Computer Science - ASIAN 2009. Information Security and Privacy, 13th Asian Computing Science Conference, Seoul, Korea, December 14-16, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5913, pp. 79–93. Springer (2009). https://doi.org/10.1007/978-3-642-10622-4_7, https://doi.org/10.1007/978-3-642-10622-4_7
  * [16] Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., Zhan, N.: Formal verification of quantum algorithms using quantum hoare logic. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II. Lecture Notes in Computer Science, vol. 11562, pp. 187–207. Springer (2019). https://doi.org/10.1007/978-3-030-25543-5_12, https://doi.org/10.1007/978-3-030-25543-5_12
  * [17] Nielsen, M.A., Chuang, I.L.: Quantum computation and quantum information, vol. 2. Cambridge university press Cambridge (2001)
  * [18] Ramshaw, L.: Formalizing the analysis of algorithms. Ph.D. thesis, Stanford University (1979)
  * [19] Rand, R., Zdancewic, S.: Vphl: A verified partial-correctness logic for probabilistic programs. Electronic Notes in Theoretical Computer Science 319, 351–367 (2015)
  * [20] Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527–586 (2004). https://doi.org/10.1017/S0960129504004256
  * [21] Sun, X., Su, X., Bian, X., Liu, Z., Cui, A.: On the relative completeness of satisfaction-based probabilistic hoare logic, submitted to CCS24
  * [22] Unruh, D.: Quantum hoare logic with ghost variables. In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’19, IEEE Press (2019)
  * [23] Unruh, D.: Quantum relational hoare logic. Proc. ACM Program. Lang. 3(POPL), 33:1–33:31 (2019). https://doi.org/10.1145/3290346, https://doi.org/10.1145/3290346
  * [24] Winskel, G.: The Formal Semantics of Programming Languages. The MIT Press (1993)
  * [25] Ying, M.: Floyd–hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6) (jan 2011). https://doi.org/10.1145/2049706.2049708, https://doi.org/10.1145/2049706.2049708
  * [26] Ying, M.: Floyd-hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6), 19:1–19:49 (2011). https://doi.org/10.1145/2049706.2049708, https://doi.org/10.1145/2049706.2049708
  * [27] Ying, M.: Toward automatic verification of quantum programs. Form. Asp. Comput. 31(1), 3–25 (feb 2019). https://doi.org/10.1007/s00165-018-0465-3, https://doi.org/10.1007/s00165-018-0465-3
  * [28] Zhou, L., Barthe, G., Strub, P.Y., Liu, J., Ying, M.: Coqq: Foundational verification of quantum programs. Proc. ACM Program. Lang. 7(POPL) (jan 2023). https://doi.org/10.1145/3571222, https://doi.org/10.1145/3571222
  * [29] Zhou, L., Yu, N., Ying, M.: An applied quantum hoare logic. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019. pp. 1149–1162. ACM (2019). https://doi.org/10.1145/3314221.3314584, https://doi.org/10.1145/3314221.3314584
  * [30] Zhou, L., Yu, N., Ying, M.: An applied quantum hoare logic. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 1149–1162 (2019)

##  Appendix 0.A Basics of quantum computation

We will introduce the basic ideas of quantum computation. For more information
on quantum computation, see [17, 20]. The basic concepts of quantum
computation are _states_ and _operations_ which act on states. Let
${\mathbb{C}}$ be the field of complex numbers. We write ${\mathbb{C}}^{n}$
for the space of $n$-dimensional column vectors.

####  0.A.0.1 $n$-qubit states

######  Definition 18.

An $n$-qubit state is a unit vector in ${\mathbb{C}}^{2^{n}}$.

In other words, the state space is the set of $2^{n}$-dimensional complex unit
vectors. For example, the space of the $1$-qubit states is the unit sphere in
the $2$-dimensional complex vector space.

For ${\mathbb{C}}^{2^{n}}$, we use the “ket-binary” notation to denote the
standard basis. For example, when $n=2$:

$|00\rangle=\begin{bmatrix}1\\\ 0\\\ 0\\\
0\end{bmatrix},\quad|01\rangle=\begin{bmatrix}0\\\ 1\\\ 0\\\
0\end{bmatrix},\quad|10\rangle=\begin{bmatrix}0\\\ 0\\\ 1\\\
0\end{bmatrix},\quad|11\rangle=\begin{bmatrix}0\\\ 0\\\ 0\\\ 1\end{bmatrix}.$

In general $|b_{n}b_{n-1}...b_{0}\rangle=e_{k}$, where
$k=\sum_{j=0}^{n}b_{j}2^{j}$, and $e_{k}$ is the $k$-th standard basis vector.
Note that $b_{n}b_{n-1}...b_{0}$ is the binary representation of $k$, and that
the standard basis starts from $e_{0}$. In the following, we will identify
each natural number index with its binary representation. One convenience of
this notation is

$|a_{m}a_{m-1}...a_{0}\rangle\otimes|b_{n}b_{n-1}...b_{0}\rangle=|a_{m}a_{m-1}...a_{0}b_{n}b_{n-1}...b_{0}\rangle.$

Another way to look at this is that every basis vector of
${\mathbb{C}}^{2^{m+n}}$ is a tensor product of basis vectors of
${\mathbb{C}}^{2^{m}}$ and ${\mathbb{C}}^{2^{n}}$. We can also identify
${\mathbb{C}}^{2^{n}}$ with the $n$-fold tensor product of ${\mathbb{C}}^{2}$.
The ket-binary notation reflects this identification.

There are two and only two kinds of operations that can be applied to an
$n$-qubit state — _unitary transformations_ and _measurements_. Quantum
algorithms are often of the form that first apply some number of unitary
transformations to a an $n$-qubit state and then do a measurement, and based
on the measurement result, some output or conclusion is drawn.

####  0.A.0.2 $n$-qubit unitary transformations

A linear function $U:{\mathbb{C}}^{k}\rightarrow{\mathbb{C}}^{m}$ is called an
_isometry_ if for all $v,w$ in ${\mathbb{C}}^{k}$, we have $\langle
Uv,Uw\rangle=\langle v,w\rangle$. $U$ is called _unitary_ if it is an
invertible isometry. Note that $U$ is unitary if and only if $UU^{\dagger}=I$
and $U^{\dagger}U=I$, where $U^{\dagger}$ denotes the adjoint of $U$. For a
matrix, the adjoint is the complex conjugate of the transpose.

######  Definition 19.

An $n$-qubit unitary transformation is a unitary transformation on
${\mathbb{C}}^{2^{n}}$

We also refer to an $n$-qubit unitary transformation as an _$n$ -qubit
operator_. The unitary condition is needed to preserve the norm of a state so
that applying a unitary transformation to a state produces a state.

####  0.A.0.3 Measurement

The other operation is the measurement. A measurement is like a finite-valued
random variable with “side-effect” which modifies the qubit state being
measured.

######  Definition 20.

Given an $n$-qubit state $\theta=\sum_{j=00...0}^{11...1}\alpha_{j}|j\rangle$,
a $1$-qubit measurement acting on the $k$-th qubit outputs $b$ and alters the
state to

$\sum_{j=00...0}^{11...1}\sum_{l=00...0}^{11...1}\alpha^{\prime}_{jbl}|jbl\rangle$

with a probability $p=\textbf{Tr}((I_{2^{j}}\otimes|b\rangle\langle b|\otimes
I_{2^{l}})\theta\theta^{\dagger})$, where $b=0,1$, $I_{2^{x}}$ is the
$2^{x}$-dimensional identity operator (i.e. identity operator on x-qubits),
$\alpha^{\prime}_{jbl}=\alpha_{jbl}/\sqrt{p}$, $j$ is of length $k-1$, and $l$
is of length $n-k$, and $jbl$ is a concatenation of binary strings $j$, $b$,
and $l$.

Later we will use $\textbf{Tr}((|b\rangle\langle b|\otimes
I_{-k})\theta\theta^{\dagger})$ to denote
$\textbf{Tr}((I_{2^{j}}\otimes|b\rangle\langle b|\otimes
I_{2^{l}})\theta\theta^{\dagger})$.

##  Appendix 0.B Proofs in Section 2

In this article, all proofs which involve no quantum operation are essentially
the same as their analogues in [21].

######  Theorem (Soundness).

The proof system QHLd is sound, $i.e.$ for all deterministic formula $\phi$
and $\psi$ and command $C$, $\vdash\\{\phi\\}C\\{\psi\\}$ implies
$\models\\{\phi\\}C\\{\psi\\}$.

###### Proof.

We prove by structural induction on $C$. Let $I$ be an arbitrary
interpretation.

  * •

(SKIP) It’s trivial to see that that
$\models\\{\phi\\}\texttt{skip}\\{\phi\\}$.

  * •

(AS) Assume $\theta\models^{I}\phi[X/E]$. We prove it by induction on the
structure of $\phi$. The only non-trivial case is when $\phi$ is of the form
$[U_{\overline{q}}]\psi$.

Assume $\theta\models[U_{\overline{q}}]\psi[X/E]$. Then
$(\theta_{c},U_{\overline{q}}\theta_{q})\models\psi[X/E]$. By the inference
rule (AS), we have $\vdash\\{\psi[X/E]\\}X\leftarrow E\\{\psi\\}$. By
induction hypothesis (IH), we obtain that $\models\\{\psi[X/E]\\}X\leftarrow
E\\{\psi\\}$. Therefore, it holds that $([\\![X\leftarrow
E]\\!]\theta_{c},U_{\overline{q}}\theta_{q})\models\psi$ and
$([\\![X\leftarrow E]\\!]\theta_{c},\theta_{q})\models[U_{\overline{q}}]\psi$
i.e. $[\\![X\leftarrow E]\\!]\widehat{\theta}\models[U_{\overline{q}}]\psi$.

  * •

(PAS) Assume $\theta\models^{I}\phi[X/k_{1}]\wedge\ldots\wedge\phi[X/k_{n}]$.
This means that $\phi$ is true if the variable $X$ is assigned to the any of
$\\{k_{1},\ldots,k_{n}\\}$ and all other values are assigned to a value
according to $\theta_{c}$. Let
$\Theta=[\\![X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}]\\!](\widehat{\theta})$.
Then $\Theta$ is a distribution with support
$\\{\theta_{1},\ldots,\theta_{n}\\}$, where $\theta_{i}=\theta[X\mapsto
k_{i}]$ for $i\in\\{1,\ldots,n\\}$. Since $\theta_{i,c}$ assigns $X$ to the
value $k_{i}$ and all other variables to the same value as $\theta_{c}$ and
$\theta_{i,q}=\theta_{q}$. We know that $\theta_{i}\models^{I}\phi$. This
means that $\phi$ is true on all supports of $\Theta$. Therefore,
$\Theta\models^{I}\phi$.

  * •

(SEQ) If the rule (SEQ) is used to derive
$\vdash\\{\phi\\}C_{1};C_{2}\\{\phi_{2}\\}$ from
$\vdash\\{\phi\\}C_{1}\\{\phi_{1}\\}$ and
$\vdash\\{\phi_{1}\\}C_{2}\\{\phi_{2}\\}$, then by IH, we have
$\models\\{\phi\\}C_{1}\\{\phi_{1}\\}$ and
$\models\\{\phi_{1}\\}C_{2}\\{\phi_{2}\\}$. Assume
$\theta\in[\\![\phi]\\!]^{I}$. Let $\theta^{\prime}$ be an arbitrary pure cq-
state such that $\theta^{\prime}\in
sp([\\![C_{1};C_{2}]\\!](\widehat{\theta}))$. By
$[\\![C_{1};C_{2}]\\!](\widehat{\theta})=[\\![C_{2}]\\!]([\\![C_{1}]\\!](\widehat{\theta}))$,
we know that there is a state $\theta_{1}\in
sp([\\![C_{1}]\\!](\widehat{\theta}))$ such that $\theta^{\prime}\in
sp([\\![C_{2}]\\!](\widehat{\theta_{1}}))$. Now by
$\models\\{\phi\\}C_{1}\\{\phi_{1}\\}$ we know that
$[\\![C_{1}]\\!](\widehat{\theta})\models^{I}\phi_{1}$ and hence
$\theta_{1}\models^{I}\phi_{1}$. By $\models\\{\phi_{1}\\}C_{2}\\{\phi_{2}\\}$
we know that $[\\![C_{2}]\\!](\widehat{\theta_{1}})\models^{I}\phi_{2}$ and
hence $\theta^{\prime}\models^{I}\phi_{2}$.

  * •

(IF) Assume $\theta\in[\\![\phi]\\!]^{I}$, $\vdash\\{\phi\wedge
B\\}C_{1}\\{\psi\\}$ and $\vdash\\{\phi\wedge\neg B\\}C_{2}\\{\psi\\}$. By
induction hypothesis we know that $\models\\{\phi\wedge B\\}C_{1}\\{\psi\\}$
and $\models\\{\phi\wedge\neg B\\}C_{2}\\{\psi\\}$. Let $\theta^{\prime}$ be
an arbitrary state which belongs to $sp([\\![\texttt{if}\ B\ \texttt{then}\
C_{1}\ \texttt{else}\ C_{2}]\\!](\widehat{\theta}))$.

Since $\theta$ is a pure cq-state, we know that either $\theta\in[\\![B]\\!]$
or $\theta\in[\\![\neg B]\\!]$.

    * –

If $\theta\in[\\![B]\\!]$, then $[\\![\texttt{if}\ B\ \texttt{then}\ C_{1}\
\texttt{else}\
C_{2}]\\!](\widehat{\theta})=[\\![C_{1}]\\!](\downarrow_{B}(\widehat{\theta}))=[\\![C_{1}]\\!](\widehat{\theta})$.
Hence $\theta^{\prime}\in sp([\\![C_{1}]\\!](\widehat{\theta}))$. From
$\theta\in[\\![\phi]\\!]^{I}$ and $\theta\in[\\![B]\\!]$ we know that
$\theta\models^{I}\phi\wedge B$. Now by $\models\\{\phi\wedge
B\\}C_{1}\\{\psi\\}$ we deduce that
$[\\![C_{1}]\\!](\widehat{\theta})\models^{I}\psi$. Therefore,
$\theta^{\prime}\models^{I}\psi$.

    * –

If $\theta\in[\\![\neg B]\\!]$, then $[\\![\texttt{if}\ B\ \texttt{then}\
C_{1}\ \texttt{else}\
C_{2}]\\!](\widehat{\theta})=[\\![C_{2}]\\!](\downarrow_{\neg
B}(\widehat{\theta}))=[\\![C_{2}]\\!](\widehat{\theta})$. Hence
$\theta^{\prime}\in sp([\\![C_{2}]\\!](\widehat{\theta}))$. From
$\theta\in[\\![\phi]\\!]^{I}$ and $\theta\in[\\![\neg B]\\!]$ we know that
$\theta\models^{I}\phi\wedge\neg B$. Now by $\models\\{\phi\wedge\neg
B\\}C_{2}\\{\psi\\}$ we deduce that
$[\\![C_{2}]\\!](\widehat{\theta})\models^{I}\psi$. Therefore,
$\theta^{\prime}\models^{I}\psi$.

  * •

(WHILE) Assume that $\vdash\\{\phi\wedge B\\}C\\{\phi\\}$, By IH, it holds
that $\models\\{\phi\wedge B\\}C\\{\phi\\}$. Let $\theta$ be an arbitrary pure
cq-state and $I$ be an arbitrary interpretation such that
$\theta\models^{I}\phi$. We remind the readers that $[\\![\texttt{while}\mbox{
}B\mbox{ }\texttt{do}\mbox{
}C]\\!](\theta)=\displaystyle\sum_{i=0}^{\infty}\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{i}(\theta))$. We want to show that for
each natural number $k$, it holds that
$([\\![C]\\!]\circ\downarrow_{B})^{k}(\theta)\models^{I}\phi$.

We prove it by induction on $k$:

    * –

If $k=0$, then
$([\\![C]\\!]\circ\downarrow_{B})^{k}(\theta)=\widehat{\theta}$. Hence
$([\\![C]\\!]\circ\downarrow_{B})^{k}(\theta)\models^{I}\phi$.

    * –

Assume that $([\\![C]\\!]\circ\downarrow_{B})^{k}(\theta)\models^{I}\phi$.
Then
$([\\![C]\\!]\circ\downarrow_{B})^{k+1}(\theta)=[\\![C]\\!]\circ\downarrow_{B}(([\\![C]\\!]\circ\downarrow_{B})^{k}(\theta))$.
For arbitrary $\theta^{\prime}\in
sp(([\\![C]\\!]\circ\downarrow_{B})^{k}(\theta))$, we have
$\theta^{\prime}\models^{I}\phi$.

      * *

If $\theta^{\prime}\models\neg B$, then
$sp([\\![C]\\!]\circ\downarrow_{B}(\theta^{\prime}))=\emptyset$. Then
$[\\![C]\\!]\circ\downarrow_{B}(\theta^{\prime})\models^{I}\phi$ vacuously.

      * *

If $\theta^{\prime}\models B$, then
$[\\![C]\\!]\circ\downarrow_{B}(\theta^{\prime})=[\\![C]\\!](\theta^{\prime})$.
Then by $\models\\{\phi\wedge B\\}C\\{\phi\\}$ we know
$[\\![C]\\!](\theta^{\prime})\models^{I}\phi$.

Therefore, we know
$[\\![C]\\!]\circ\downarrow_{B}(\theta^{\prime})\models^{I}\phi$ for all
$\theta^{\prime}\in sp(([\\![C]\\!]\circ\downarrow_{B})^{k}(\theta))$. This
implies that $([\\![C]\\!]\circ\downarrow_{B})^{k+1}(\theta)\models^{I}\phi$.
According to the above claim, we infer that $\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{i}(\theta))\models^{I}\phi\wedge\neg B$
for each $i\in\mathbb{N}$. Hence
$\displaystyle\sum_{i=0}^{\infty}\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{i}(\theta))\models^{I}\phi\wedge\neg B$.
This proves $[\\![\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{
}C]\\!](\theta)\models^{I}\phi\wedge\neg B$.

  * •

(UNITARY) If $\theta\models[U_{\overline{q}}]\phi$, then
$[U_{\overline{q}}]\theta\models\phi$. That is,
$[\\![U[\overline{q}]]\\!]\theta\models\phi$.

  * •

(MEASURE) Assume $\theta\models([\mathfrak{P}^{0}_{j}]\phi[X/0]\vee
P^{1}_{j})\wedge([\mathfrak{P}^{1}_{j}]\phi[X/1]\vee P^{0}_{j})$. We prove it
by case analysis:

    * –

If $\theta\models P^{1}_{j}$, then $\theta\not\models P^{0}_{j}$. Hence
$\theta\models[\mathfrak{P}^{1}_{j}]\phi[X/1]$. Note that in this case
$[\\![X\leftleftarrows q_{j}]\\!]\theta=\widehat{\theta^{\prime}}$ where
$\theta^{\prime}_{c}=\theta_{c}[X\mapsto 1]$ and
$\theta^{\prime}_{q}=\frac{(P^{1}\otimes I_{-j})\theta_{q}}{\sqrt{p_{1}}}$,
$p_{1}=\textbf{Tr}((P^{1}\otimes I_{-j})\theta_{q}\theta_{q}^{\dagger})$. From
$\theta\models[\mathfrak{P}^{1}_{j}]\phi[X/1]$, we obtain that
$(\theta_{c},\theta^{\prime}_{q})\models\phi[X/1]$, which further implies that
$(\theta_{c}[X\mapsto 1],\theta^{\prime}_{q})\models\phi$. That is
$\theta^{\prime}\models\phi$.

    * –

The case for $\theta\models P^{0}_{j}$ can be proved analogously.

    * –

If $\theta\models\neg P^{0}_{j}\wedge\neg P^{1}_{j}$, then
$\theta\models[\mathfrak{P}^{0}_{j}]\phi[X/0]\wedge[\mathfrak{P}^{1}_{j}]\phi[X/1]$.
In this case $[\\![X\leftleftarrows q_{j}]\\!]\theta=\Theta$ where
$\Theta=p_{0}\theta_{0}+p_{1}\theta_{1}$, $p_{i}=\textbf{Tr}((P^{i}\otimes
I_{-j})\theta_{q}\theta_{q}^{\dagger})>0$, $\theta_{i,c}=\theta_{c}[X\mapsto
i]$, $\theta_{i,q}=\frac{(P^{i}\otimes I_{-j})\theta_{q}}{\sqrt{p_{i}}}$. From
$\theta\models[\mathfrak{P}^{0}_{j}]\phi[X/0]$ we know
$(\theta_{c},\theta_{0,q})\models\phi[X/0]$, which implies that
$(\theta_{0,c},\theta_{0,q})\models\phi$. From
$\theta\models[\mathfrak{P}^{1}_{j}]\phi[X/1]$ we know
$(\theta_{c},\theta_{1,q})\models\phi[X/1]$, which implies that
$(\theta_{1,c},\theta_{1,q})\models\phi$. Therefore, $\Theta\models\phi$.

  * •

(CONS) Assume $\models\phi^{\prime}\rightarrow\phi$,
$\vdash\\{\phi\\}C\\{\psi\\}$ and $\models\psi\rightarrow\psi^{\prime}$. By
induction hypothesis we obtain that $\models\\{\phi\\}C\\{\psi\\}$. Let
$\theta$ be a state such that $\theta\models^{I}\phi^{\prime}$. Then by
$\models\phi^{\prime}\rightarrow\phi$ we know that $\theta\models^{I}\phi$. By
$\models\\{\phi\\}C\\{\psi\\}$ we know that
$[\\![C]\\!](\widehat{\theta})\models^{I}\psi$. Hence
$\theta^{\prime}\models^{I}\psi$ for all $\theta^{\prime}$ which belongs to
$sp([\\![C]\\!](\widehat{\theta}))$. Now by
$\models\psi\rightarrow\psi^{\prime}$ we know that
$\theta^{\prime}\models^{I}\psi^{\prime}$.

∎

######  Theorem.

$\Theta\models^{I}wp(C,\phi)$ iff $[\\![C]\\!](\Theta)\models^{I}\phi$.

###### Proof.

It is sufficient to prove that $\theta\models^{I}wp(C,\phi)$ iff
$[\\![C]\\!](\widehat{\theta})\models^{I}\phi$.

  * •

(skip) $\theta\models^{I}wp(skip,\phi)$ iff $\theta\models^{I}\phi$ iff
$[\\![skip]\\!](\widehat{\theta})\models^{I}\phi$.

  * •

(AS) $\theta\models^{I}wp(X\leftarrow E,\phi)$ iff
$\theta\models^{I}\phi[X/E]$. Then we will show that $[\\![X\leftarrow
E]\\!](\widehat{\theta})\models\phi$.

Assume that $\theta\models^{I}\phi[X/E]$. By Definition 5, $[\\![X\leftarrow
E]\\!](\widehat{\theta})=(\theta_{c},\theta^{\prime}_{q})$ where
$\theta^{\prime}_{q}=\theta_{q}$ and
$\theta^{\prime}_{c}=\theta_{c}[X\mapsto\llbracket
E\rrbracket^{I}\theta_{c}]$.

Do induction on the structure of $\phi$:

    * –

When $\phi$ is $\top$ or $\bot$, the proof is trivial.

    * –

When $\phi=P^{i}_{j}$, $\theta\models^{I}P^{i}_{j}[X/E]$ iff
$\theta\models^{I}P^{i}_{j}$ iff
$Tr(P^{i}Tr_{-j}(\theta_{q}\theta_{q}^{\dagger}))=1$ iff
$(\theta^{\prime}_{c},\theta_{q})\models P_{j}^{i}$ iff $\llbracket
X\leftarrow E\rrbracket\widehat{\theta}\models P_{j}^{i}$.

    * –

When $\phi=e_{1}\ rop\ e_{2}$, $\theta\models^{I}(e_{1}\ rop\ e_{2})[X/E]$ iff
$\theta\models^{I}e_{1}[X/E]\ rop\ e_{2}[X/E]$ iff
$\theta_{c}\models^{I}e_{1}[X/E]\ rop\ e_{2}[X/E]$.

Induction on the structure of $e_{1}$ (similarly to $e_{2}$), we will prove
$\llbracket e_{1}[X/E]\rrbracket^{I}\theta_{c}=\llbracket
e_{1}\rrbracket^{I}_{\theta_{c}[X\mapsto\llbracket
E\rrbracket^{I}\theta_{c}]}$.

      * *

If $e_{1}=n$ for some integer $n$, $\llbracket
n[X/E]\rrbracket^{I}\theta_{c}=n=\llbracket
n\rrbracket^{I}\theta_{c}[X\mapsto\llbracket E\rrbracket\theta_{c}]$.

      * *

If $e_{1}=X$, $\llbracket X[X/E]\rrbracket^{I}\theta_{c}=\llbracket
E\rrbracket\theta_{c}=\llbracket X\rrbracket^{I}\theta_{c}[X\mapsto\llbracket
E\rrbracket^{I}\theta_{c}]$.

      * *

If $e_{1}=x$, $\llbracket x[X/E]\rrbracket^{I}\theta_{c}=\llbracket
x\rrbracket\theta_{c}=\llbracket x\rrbracket^{I}\theta_{c}[X\mapsto\llbracket
E\rrbracket^{I}\theta_{c}]$.

      * *

If $e_{1}=e_{3}\ aop\ e_{4}$, $\llbracket(e_{3}\ aop\
e_{4})[X/E]\rrbracket^{I}\theta_{c}=\llbracket
e_{3}[X/E]\rrbracket^{I}\theta_{c}\ aop\ \llbracket
e_{4}[X/E]\rrbracket^{I}\theta_{c}$. By IH, it equals $\llbracket
e_{3}^{I}\theta_{c}[X\mapsto\llbracket E\rrbracket\theta_{c}]\ aop\
e_{4}^{I}\theta_{c}[X\mapsto\llbracket E\rrbracket\theta_{c}]=\llbracket
e_{3}\ aop\ e_{4}\rrbracket^{I}\theta_{c}[X\mapsto\llbracket
E\rrbracket\theta_{c}]$.

So we have $\theta_{c}\models^{I}e_{1}[X/E]\ rop\ e_{2}[X/E]$ iff
$\theta_{c}[X\mapsto\llbracket E\rrbracket\theta_{c}]=e_{1}\ rop\ e_{2}$ iff
$\llbracket X\leftarrow E\rrbracket(\widehat{\theta})\models^{I}e_{1}\ rop\
e_{2}$.

    * –

When $\phi=\neg\psi$, $\theta\models^{I}\neg\psi[X/E]$ iff
$\theta\not\models^{I}\psi[X/E]$. By IH, $\llbracket X\leftarrow
E\rrbracket(\widehat{\theta})\not\models\psi$. So $\llbracket X\leftarrow
E\rrbracket(\widehat{\theta})\models\neg\psi$.

    * –

When $\phi=\phi_{1}\wedge\phi_{2}$,
$\theta\models(\phi_{1}\wedge\phi_{2})[X/E]$ iff
$\theta\models^{I}\phi_{1}[X/E]\wedge\phi_{2}[X/E]$. By IH, we have
$\llbracket X\leftarrow E\rrbracket^{I}(\widehat{\theta})\models\phi_{1}$ and
$\llbracket X\leftarrow E\rrbracket(\widehat{\theta})\models^{I}\phi_{2}$ iff
$\llbracket X\leftarrow
E\rrbracket(\widehat{\theta})\models^{I}\phi_{1}\wedge\phi_{2}$.

    * –

When $\phi=\forall x\psi$, $\theta\models^{I}\forall x\psi[X/E]$ iff for all
integers $n$ and $I^{\prime}=I[x\mapsto n]$,
$\theta\models^{I^{\prime}}\psi[X/E]$. By IH, $\llbracket X\leftarrow
E\rrbracket(\widehat{\theta})\models^{I^{\prime}}\psi$ for each $I^{\prime}$
with $I^{\prime}=I[x\mapsto n]$ iff $\llbracket X\leftarrow
E\rrbracket(\widehat{\theta})\models\forall x\psi$.

    * –

When $\phi=[U_{\overline{q}}]\psi$,
$\theta\models^{I}[U_{\overline{q}}]\psi[X/E]$ iff $\llbracket
U_{\overline{q}}\rrbracket(\widehat{\theta})\models^{I}\psi[X/E]$ iff
$(\theta_{c},U_{\overline{q}}\theta
U^{\dagger}_{\overline{q}})\models^{I}\psi[X/E]$. By IH, $\llbracket
X\leftarrow E\rrbracket\llbracket
U_{\overline{q}}\rrbracket(\widehat{\theta})\models^{I}\psi$ iff
$(\theta_{c}[X\mapsto\llbracket
E\rrbracket\theta_{c}],U_{\overline{q}}\theta_{q}U_{\overline{q}}^{\dagger})\models^{I}\psi$
iff $\llbracket X\leftarrow
E\rrbracket(\widehat{\theta})\models[U_{\overline{q}}]\psi$.

    * –

When $\phi=[\mathcal{B}^{i}_{j}]\psi$,
$\theta\models^{I}[\mathcal{B}^{i}_{j}]\psi[X/E]$ iff
$\theta^{\prime}\models^{I}\psi[X/E]$ iff $\theta^{\prime}\models^{\psi}[X/E]$
where $\theta_{c}^{\prime}=\theta_{c}$ and
$\theta^{\prime}_{q}=\frac{(P_{j}^{1}\otimes
I_{-j})\theta_{q}}{\sqrt{p_{i}}}$. By IH, $(\llbracket X\leftarrow
E\rrbracket\theta_{c},\theta^{\prime}_{q})\models^{I}\psi$ iff $\llbracket
X\leftarrow E\rrbracket\theta\models^{I}[\mathcal{B}_{j}^{i}]\psi$.

  * •

(PAS)
$\theta\models^{I}wp(X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\},\phi)$
iff $\theta\models^{I}\phi[X/k_{1}]\wedge\ldots\wedge\phi[X/k_{n}]$. Then, it
will be proved that
$\theta\models^{I}\phi[X/k_{1}]\wedge\ldots\wedge\phi[X/k_{n}]$ iff
$\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}\rrbracket(\widehat{\theta})\models^{I}\phi$.

Do induction on the structure of $\phi$:

    * –

When $\phi$ is $\top$ or $\bot$, the proof is trivial.

    * –

When $\phi=P_{j}^{i}$, $\theta\models^{I}P_{j}^{i}[X/k_{1}]\wedge\cdots\wedge
P_{j}^{i}[X/k_{n}]$ iff $\theta\models^{I}P_{j}^{i}$ iff $\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}\rrbracket(\widehat{\theta})\models^{I}P_{j}^{i}$.

    * –

When $\phi=e_{1}\ rop\ e_{2}$, $\theta\models^{I}(e_{1}\ rop\
e_{2})[X/k_{1}]\wedge\cdots\wedge(e_{1}\ rop\ e_{2})[X/k_{n}]$ iff
$\theta\models^{I}(e_{1}\ rop\ e_{2})[X/k_{1}]$ and $\cdots$ and
$\theta\models(e_{1}\ rop\ e_{2})[X/k_{n}]$. By the proof in the case (AS)
above, we have $\llbracket X\leftarrow
k_{1}\rrbracket(\widehat{\theta})\models^{I}e_{1}\ rop\ e_{2}$ and $\cdots$
and $\llbracket X\leftarrow k_{n}\rrbracket(\widehat{\theta})\models^{I}e_{1}\
rop\ e_{2}$.

($\Rightarrow$) Let $\theta^{\prime}\in sp(\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}\rrbracket(\widehat{\theta}))$.
We know that $\theta^{\prime}_{q}=\theta_{q}$ and $\theta^{\prime}_{c}$ only
differs in the value of $X$ from $\theta_{c}$. Suppose $\llbracket
X\rrbracket^{I}\theta^{\prime}_{c}=k_{i}$($1\leq i\leq n$). So we have
$\llbracket X\leftarrow
k_{i}\rrbracket(\widehat{\theta})=\widehat{\theta^{\prime}}$ and
$\widehat{\theta^{\prime}}\models^{I}e_{1}\ rop\ e_{2}$. Since
$\theta^{\prime}$ is arbitrarily chosen, $\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}\rrbracket(\widehat{\theta})\models^{I}e_{1}\
rop\ e_{2}$.

($\Leftarrow$) Assume $\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}\rrbracket(\widehat{\theta})\models^{I}e_{1}\
rop\ e_{2}$. It implies that for each $\theta^{\prime}\in sp(\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}\rrbracket(\widehat{\theta}))$,
$\theta^{\prime}\models^{I}e_{1}\ rop\ e_{2}$. By Definition 5,
$\theta^{\prime}=\llbracket X\leftarrow k_{i}\rrbracket(\widehat{\theta})$ for
some $1\leq i\leq n$. So $\llbracket X\leftarrow
k_{i}\rrbracket(\widehat{\theta})\models e_{1}\ rop\ e_{2}$. Thus, we have
$\llbracket X\leftarrow k_{1}\rrbracket(\widehat{\theta})\models^{I}e_{1}\
rop\ e_{2}$ and $\cdots$ and $\llbracket X\leftarrow
k_{n}\rrbracket(\widehat{\theta})\models^{I}e_{1}\ rop\ e_{2}$.

    * –

When $\phi=\neg\psi$ or $\psi_{1}\wedge\psi_{2}$ or $\forall x\psi$, the
proofs are similar to those in the case of (AS), respectively.

    * –

When $\phi=[U_{\overline{q}}]\psi$,
$\theta\models^{I}[U_{\overline{q}}]\psi[X/k_{1}]\wedge\cdots\wedge[U_{\overline{q}}]\psi[X/k_{n}]$
iff $\theta\models^{I}[U_{\overline{q}}]\psi[X/k_{1}]$ and $\cdots$ and
$\theta\models^{I}[U_{\overline{q}}]\psi[X/k_{n}]$ iff
$(\theta_{c},U_{\overline{q}}\theta_{q}U_{\overline{q}}^{\dagger})\models^{I}\psi[X/k_{1}]$
and $\cdots$ and
$(\theta_{c},U_{\overline{q}}\theta_{q}U_{\overline{q}}^{\dagger})\models^{I}\psi[X/k_{n}]$
iff, by what we proved in the case of (AS), $\llbracket X\leftarrow
k_{1}\rrbracket(\widehat{\theta})\models[U_{\overline{q}}]\psi$ and $\cdots$
and $\llbracket X\leftarrow
k_{n}\rrbracket(\widehat{\theta})\models[U_{\overline{q}}]\psi$. Suppose
$\theta^{\prime}\in sp(\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}\rrbracket(\widehat{\theta}))$.
$\theta^{\prime}_{c}=\llbracket X\leftarrow k_{i}\rrbracket(\widehat{\theta})$
for some $1\leq i\leq n$ and $\theta^{\prime}_{q}=\theta_{q}$. So
$\theta^{\prime}=\llbracket X\leftarrow k_{i}\rrbracket(\theta)$.

($\Leftarrow$) By $\llbracket X\leftarrow
k_{i}\rrbracket(\widehat{\theta})\models[U_{\overline{q}}]\psi$,
$\theta^{\prime}\models[U_{\overline{q}}]\psi$. So $\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\rrbracket(\widehat{\theta})\models[U_{\overline{q}}]\psi$.

($\Rightarrow$) By $\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\rrbracket(\widehat{\theta})\models[U_{\overline{q}}]\psi$,
$\theta^{\prime}\models[U_{\overline{q}}]\psi$, which implies that $\llbracket
X\leftarrow
k_{i}\rrbracket(\widehat{\theta})\models^{I}[U_{\overline{Q}}]\psi$.

So we proved that
$\theta\models^{I}[U_{\overline{q}}]\psi[X/k_{1}]\wedge\cdots\wedge[U_{\overline{q}}]\psi[X/k_{n}]$
iff $\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}\rrbracket(\widehat{\theta})\models[U_{\overline{q}}]\psi$.

    * –

When $\phi=[\mathcal{B}_{j}^{i}]\psi$,
$\theta\models^{I}[\mathcal{B}_{j}^{i}]\psi[X/k_{1}]\wedge\cdots\wedge[\mathcal{B}_{j}^{i}]\psi[X/k_{n}]$
iff $\theta\models^{I}[\mathcal{B}_{j}^{i}]\psi[X/k_{1}]$ and $\cdots$ and
$\theta\models^{I}[\mathcal{B}_{j}^{i}]\psi[X/k_{n}]$ iff $\llbracket
X\leftarrow k_{1}\rrbracket(\widehat{\theta})\models[\mathcal{B}_{j}^{i}]\psi$
and $\cdots$ and $\llbracket X\leftarrow
k_{n}\rrbracket(\widehat{\theta})\models[\mathcal{B}_{j}^{i}]\psi$. Suppose
that $\theta^{\prime}\in sp(\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\\}\rrbracket(\widehat{\theta}))$.
We have $\theta^{\prime}=\llbracket X\leftarrow k_{i}\rrbracket\theta$ for
some $1\leq i\leq n$.

($\Leftarrow$) By $\llbracket X\leftarrow
k_{i}\rrbracket(\widehat{\theta})\models[\mathcal{B}_{j}^{i}]\psi$,
$\theta^{\prime}\models[\mathcal{B}_{j}^{i}]\psi$. So $\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\rrbracket(\widehat{\theta})\models[\mathcal{B}_{j}^{i}]\psi$.

($\Rightarrow$) By $\llbracket
X\xleftarrow{\$}\\{a_{1}:k_{1},...,a_{n}:k_{n}\rrbracket(\widehat{\theta})\models[\mathcal{B}_{j}^{i}]\psi$,
$\theta^{\prime}\models[\mathcal{B}_{j}^{i}]\psi$, which implies that
$\llbracket X\leftarrow
k_{i}\rrbracket(\widehat{\theta})\models^{I}[\mathcal{B}_{j}^{i}]\psi$.

So we proved the case.

  * •

(SEQ) $\theta\models wp(C_{1};C_{2},\phi)$ iff $\theta\models
wp(C_{1},wp(C_{2},\phi))$ iff, by IH, $[\\![C_{1}]\\!](\theta)\models
wp(C_{2},\phi)$ iff, by IH,
$[\\![C_{2}]\\!]([\\![C_{1}]\\!](\theta)\models)\models\phi$ iff
$[\\![C_{1};C_{2}]\\!](\theta)\models\phi$

  * •

(IF) $\theta\models wp(if\ B\ then\ C_{1}\ else\ C_{2},\phi)$ iff
$\theta\models(B\wedge wp(C_{1},\phi))\vee(\neg B\wedge wp(C_{2},\phi))$ iff
$\theta\models B$ and $\theta\models wp(C_{1},\phi)$ or $\theta\models\neg B$
and $\theta\models wp(C_{2},\phi)$ iff $\theta\models B$ and
$[\\![C_{1}]\\!]\theta\models\phi$ or $\theta\models\neg B$ and
$[\\![C_{2}]\\!]\theta\models\phi$ iff $[\\![if\ B\ then\ C_{1}\ else\
C_{2}]\\!]\theta\models\phi$.

  * •

(WHILE) ($\Rightarrow$) Assume $\theta\models wp(while\mbox{ }B\mbox{
}do\mbox{ }C,\phi)$, then from soundness and
$\vdash\\{wp(C,\phi)\\}C\\{\phi\\}$ we know
$\models\\{wp(C,\phi)\\}C\\{\phi\\}$. Therefore, $[\\![while\mbox{ }B\mbox{
}do\mbox{ }C]\\!]\theta\models\phi$.

($\Leftarrow$) Assume $[\\![while\mbox{ }B\mbox{ }do\mbox{
}C]\\!]\theta\models\phi$.

We prove by induction on the iteration times of the while loop.

    * –

Suppose that the while loop is terminated after $0$ time of execution.111The
loop terminated after $k$ steps means that the longest branch of the execution
of the while loop terminates after $k$ steps.  Then $\theta\not\models B$ and
$[\\![while\mbox{ }B\mbox{ }do\mbox{ }C]\\!](\theta)=\theta$. Therefore,
$\theta\models^{I}\phi$. Then we have $\theta\models^{I}\neg B\wedge\phi$.
Hence $\theta\models^{I}\psi_{i}$ for all $i$. Therefore,
$\theta\models^{I}wp(while\mbox{ }B\mbox{ }do\mbox{ }C,\phi)$.

    * –

Suppose that the while loop is terminated after $1$ time of execution. Then
$\theta\models B$ ,
$([\\![C]\\!]\circ\downarrow_{B})(\theta)=[\\![C]\\!](\theta)$ and
$[\\![C]\\!](\theta)\models\neg B\wedge\phi$.

Hence $[\\![C]\\!](\theta)\models^{I}\psi_{i}$ for all $i$.

By I.H. we know $\theta\models wp(C,\psi_{i})$. Therefore, $\theta\models
B\wedge wp(C,\psi_{i})$,

$\theta\models^{I}\psi_{i}$ for all $i$. That is,
$\theta\models^{I}wp(while\mbox{ }B\mbox{ }do\mbox{ }C,\phi)$.

    * –

By induction hypothesis, it holds that if iteration time is $k$, $\llbracket
While\ B\ do\ C\rrbracket\models\phi$.

Suppose that the while loop is terminated after $k+1$ times of execution.

Let $\theta_{1}\in sp(([\\![C]\\!]\circ\downarrow_{B})^{k}(\theta))$.

      * *

If $\theta_{1}\models\neg B$, then $\theta_{1}$ is a state where the loop
terminates after $k$ time of execution. Then by the induction hypothesis we
know $\theta_{1}\models^{I}\psi_{i}$ for all $i$.

      * *

If $\theta_{1}\models B$, then
$([\\![C]\\!]\circ\downarrow_{B})(\theta_{1})=[\\![C]\\!](\theta_{1})$.
Therefore, for all $\theta^{\prime}\in sp([\\![C]\\!](\theta_{1}))$,
$\theta^{\prime}\not\models B$, $\theta^{\prime}\models^{I}\phi$ and
$[\\![C]\\!](\theta_{1})\models^{I}\neg B\wedge\phi$. Hence
$[\\![C]\\!](\theta_{1})\models^{I}\psi_{i}$ for all $i$. By I.H. we know
$\theta_{1}\models wp(C,\psi_{i})$. From $\theta_{1}\models B$ we deduce that

$\theta_{1}\models^{I}\psi_{i}$ for all $i$.

This proves $([\\![C]\\!]\circ\downarrow_{B})^{k}(\theta)\models^{I}\psi_{i}$
for all $i$.

    * –

Now we study the case in which the loop never terminates. That is, there is an
infinite sequence of pure cq-states $\theta_{0},\theta_{1},\theta_{2},\ldots$
in which $\theta_{0}=\theta$ and $\theta_{j+1}\in
sp([\\![C]\\!](\theta_{j}))$. We will show that $\theta_{j}\models\psi_{i}$
for all $i$ and $j$.

It’s easy to see that $\theta_{j}\models B$ for all $j$ because otherwise the
loop will terminate. Now we prove that for all $j$,
$\theta_{j}\models\psi_{i}$ for all $i$ by induction on $i$.

It’s easy to see that $\theta_{j}\models\psi_{0}$ for all $j$. Assume for all
$j$ it holds that $\theta_{j}\models\psi_{k}$. Then $\theta_{j-1}\models
wp(C,\psi_{k})$. Therefore, $\theta_{j-1}\models\psi_{k+1}$.

  * •

(UNITARY) $\theta\models wp(U[\overline{q}],\phi)$ iff
$\theta\models[U_{\overline{q}}]\phi$ iff $U[\overline{q}]\theta\models\phi$.

  * •

(MEASURE) $\theta\models wp(X\leftleftarrows q_{j},\phi)$ iff
$\theta\models(P^{1}_{j}\vee[\mathfrak{P}^{0}_{j}]\phi[X/0])\wedge(P^{0}_{j}\vee[\mathfrak{P}^{1}_{j}]\phi[X/1])$.
Now we prove it by case analysis.

    1. 1.

If $\theta\models P^{1}_{j}$, then
$\theta\models(P^{1}_{j}\vee[\mathfrak{P}^{0}_{j}]\phi[X/0])\wedge(\mathfrak{P}^{0}_{j}\vee[P^{1}_{j}]\phi[X/1])$
iff $[\\![X\leftarrow M[q_{j}]]\\!]\theta\models\phi$

    2. 2.

If $\theta\models P^{0}_{j}$, then
$\theta\models(P^{1}_{j}\vee[\mathfrak{P}^{0}_{j}]\phi[X/0])\wedge(P^{0}_{j}\vee[\mathfrak{P}^{1}_{j}]\phi[X/1])$
iff $[\\![X\leftarrow M[q_{j}]]\\!]\theta\models\phi$

    3. 3.

If $\theta\models\neg P^{0}_{j}\wedge\neg P^{1}_{j}$, then
$\theta\models(P^{1}_{j}\vee[\mathfrak{P}^{0}_{j}]\phi[X/0])\wedge(P^{0}_{j}\vee[\mathfrak{P}^{1}_{j}]\phi[X/1])$
iff $[\\![X\leftleftarrows q_{j}]\\!]\theta\models\phi$

∎

######  Proposition.

It holds that $\vdash\\{wp(C,\phi)\\}C\\{\phi\\}$.

###### Proof.

We use structural induction on $C$. We only show these non-trivial cases
below. The cases of (SKIP),(AS), (PAS), (UNITARY) and (MEASURE) are trivial.

  * •

(SEQ) We have $\vdash\\{wp(C_{1},wp(C_{2},\phi))\\}C_{1}\\{wp(C_{2},\phi)\\}$
and $\vdash\\{wp(C_{2},\phi)\\}C_{2}\\{\phi\\}$ by inductive hypothesis. Using
SEQ, we have $\vdash\\{wp(C_{1},wp(C_{2},\phi))\\}C_{1};C_{2}\\{\phi\\}$.

  * •

(IF) By inductive hypothesis we have $\\{wp(C_{1},\phi)\\}C_{1}\\{\phi\\}$ and
$\\{wp(C_{2},\phi)\\}C_{2}\\{\phi\\}$. Then by (CONS) we know
$\\{B\wedge(wp(C_{1},\phi)\wedge B)\vee(wp(C_{2},\phi)\wedge\neg
B))\\}C_{1}\\{\phi\\}$ and $\\{\neg B\wedge(wp(C_{1},\phi)\wedge
B)\vee(wp(C_{2},\phi)\wedge\neg B)))\\}C_{2}\\{\phi\\}$. Now, by (IF) we have
$\vdash\\{(wp(C_{1},\phi)\wedge B)\vee(wp(C_{2},\phi)\wedge\neg B)\\}if\ B\
then\ C_{1}\ else\ C_{2}\\{\phi\\}$.

  * •

(WHILE) It is easy to see that $\models(B\wedge\bigwedge\limits_{k\geq
0}\psi_{k})\rightarrow(B\wedge\bigwedge\limits_{k\geq 1}wp(C,\psi_{i}))$. By
inductive hypothesis, $\vdash\\{\bigwedge\limits_{k\geq
1}wp(C,\psi_{i})\\}C\\{\bigwedge\limits_{k\geq 1}\psi_{i}\\}$. Now by (CONS)
we have $\vdash\\{B\wedge\bigwedge\limits_{k\geq
1}wp(C,\psi_{i})\\}C\\{\bigwedge\limits_{k\geq 1}\psi_{i}\\}$. Note that
$\models\bigwedge\limits_{k\geq
1}\psi_{i}\leftrightarrow\bigwedge\limits_{k\geq 0}\psi_{i}$. Then by (CONS)
we have $\vdash\\{B\wedge\bigwedge\limits_{k\geq
1}wp(C,\psi_{i})\\}C\\{\bigwedge\limits_{k\geq 0}\psi_{i}\\}$.
That is, $\vdash\\{B\wedge wp(while\mbox{ }B\mbox{ }do\mbox{
}C,\phi)\\}C\\{wp(while\mbox{ }B\mbox{ }do\mbox{ }C,\phi)\\}$.

Then by (WHILE) we know

$\vdash\\{wp(while\mbox{ }B\mbox{ }do\mbox{ }C,\phi)\\}while\mbox{ }B\mbox{
}do\mbox{ }C\\{wp(while\mbox{ }B\mbox{ }do\mbox{ }C,\phi)\wedge\neg B\\}$.

Then by the definition of $wp(while\mbox{ }B\mbox{ }do\mbox{ }C,\phi)$ we know
$\vdash\\{wp(while\mbox{ }B\mbox{ }do\mbox{ }C,\phi)\\}while\mbox{ }B\mbox{
}do\mbox{ }C\\{\phi\\}$.

∎

######  Lemma.

For all $i\geq 0$ and all pure cq-state $\theta$, if $\theta\models^{I}\neg
wp(C^{0},\neg B)\wedge\ldots\wedge\neg wp(C^{i-1},\neg B)\wedge wp(C^{i},\neg
B)$, then

$[\\![\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{
}C]\\!](\widehat{\theta})=[\\![(\texttt{if}\mbox{ }B\mbox{
}\texttt{then}\mbox{ }C\mbox{ }\texttt{else}\mbox{
}\texttt{skip})^{i}]\\!](\widehat{\theta}).$

###### Proof.

We first prove the case where $i=0$. Then we have
$\theta\models^{I}wp(C^{0},\neg B)$. That is, $\theta\models^{I}\neg B$. It is
trivial to show that $[\\![\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{
}C]\\!](\widehat{\theta})=[\\![(\texttt{if}\mbox{ }B\mbox{
}\texttt{then}\mbox{ }C\mbox{ }\texttt{else}\mbox{
}\texttt{skip})^{0}]\\!](\widehat{\theta})$.

We then prove the case where $i=1$. Then we have $\theta\models^{I}\neg
wp(C^{0},\neg B)\wedge wp(C,\neg B)$, which implies that
$\theta\models^{I}\neg B$ and for all $\theta^{\prime}\in sp(\llbracket
C\rrbracket\widehat{\theta})$, $\theta^{\prime}\models^{I}\neg B$. Then it is
easy to see that $[\\![\texttt{while}\mbox{ }B\mbox{ }\texttt{do}\mbox{
}C]\\!](\widehat{\theta})=[\\![(\texttt{if}\mbox{ }B\mbox{
}\texttt{then}\mbox{ }C\mbox{ }\texttt{else}\mbox{
}\texttt{skip})^{1}]\\!](\widehat{\theta})$.

We now prove the case where $i=2$, other cases are similar. Assume $i=2$. Then
we have $\theta\models\neg wp(C^{0},\neg B)\wedge\neg wp(C^{1},\neg B)\wedge
wp(C^{2},\neg B)$. Then we know $\theta\not\models^{I}wp(\texttt{skip},\neg
B)$, $\theta\not\models^{I}wp(C,\neg B)$ and $\theta\models^{I}wp(C;C,\neg
B)$. Therefore, $\theta\models^{I}\neg B$,
$[\\![C]\\!](\widehat{\theta})\not\models^{I}\neg B$ and
$[\\![C;C]\\!](\widehat{\theta})\models^{I}\neg B$. We then know
$\downarrow_{B}([\\![C;C]\\!](\widehat{\theta}))=\textbf{0}$.

It’s easy to see that
$sp([\\![C]\\!]\circ\downarrow_{B}(\widehat{\theta}))\subseteq
sp([\\![C]\\!](\widehat{\theta}))$. Then from $\theta\models^{I}wp(C^{2},\neg
B)$ we deduce $[\\![C^{2}]\\!]\theta\models^{I}\neg B$, which implies
$[\\![(C\circ\downarrow_{B})^{2}]\\!]\theta\models^{I}\neg B$.

Then $\displaystyle\sum_{i=0}^{\infty}\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{i}(\widehat{\theta}))=\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{0}(\widehat{\theta}))+\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{1}(\widehat{\theta}))+\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{2}(\widehat{\theta}))+\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{3}(\widehat{\theta}))+\ldots=\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{0}(\widehat{\theta}))+\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{1}(\widehat{\theta})+\downarrow_{\neg
B}(([\\![C]\\!]\circ\downarrow_{B})^{2}(\widehat{\theta}))=\downarrow_{\neg
B}(\widehat{\theta})+\downarrow_{\neg
B}\circ[\\![C]\\!]\circ\downarrow_{B}(\widehat{\theta})+([\\![C]\\!]\circ\downarrow_{B})^{2}(\widehat{\theta})$.

On the other hand, $[\\![\texttt{if}\mbox{ }B\mbox{ }\texttt{then}\mbox{
}C\mbox{ }\texttt{else}\mbox{ }\texttt{skip}]\\!]^{2}(\widehat{\theta})=$
$[\\![\texttt{if}\mbox{ }B\mbox{ }\texttt{then}\mbox{ }C\mbox{
}\texttt{else}\mbox{
}\texttt{skip}]\\!]([\\![C]\\!]\circ\downarrow_{B}(\widehat{\theta})+\downarrow_{\neg
B}(\widehat{\theta}))=$
$[\\![C]\\!]\circ\downarrow_{B}([\\![C]\\!]\circ\downarrow_{B}(\widehat{\theta})+\downarrow_{\neg
B}(\widehat{\theta}))+\downarrow_{\neg
B}([\\![C]\\!]\circ\downarrow_{B}(\widehat{\theta})+\downarrow_{\neg
B}(\widehat{\theta}))=$
$[\\![C]\\!]\circ\downarrow_{B}[\\![C]\\!]\circ\downarrow_{B}(\widehat{\theta})+[\\![C]\\!]\circ\downarrow_{B}(\downarrow_{\neg
B}(\widehat{\theta}))+\downarrow_{\neg
B}[\\![C]\\!]\circ\downarrow_{B}(\widehat{\theta})+\downarrow_{\neg
B}(\downarrow_{\neg B}(\widehat{\theta}))=$
$([\\![C]\\!]\circ\downarrow_{B})^{2}((\widehat{\theta}))+\textbf{0}+\downarrow_{\neg
B}[\\![C]\\!]\circ\downarrow_{B}(\widehat{\theta})+\downarrow_{\neg
B}(\widehat{\theta})=$
$\downarrow_{\neg B}(\widehat{\theta})+\downarrow_{\neg
B}[\\![C]\\!]\circ\downarrow_{B}(\widehat{\theta})+([\\![C]\\!]\circ\downarrow_{B})^{2}(\widehat{\theta})$.

∎

##  Appendix 0.C Proofs in Section 3

######  Lemma.

Given an arbitrary probabilistic cq-state $\Theta$, an interpretation $I$, a
command $C$ and a real expression $r$,

$[\\![pt(C,r)]\\!]^{I}_{\Theta}=[\\![r]\\!]^{I}_{[\\![C]\\!]\Theta}$

###### Proof.

  1. 1.

$[\\![pt(C,a)]\\!]^{I}_{\Theta}=[\\![a]\\!]^{I}_{\Theta}=a=[\\![a]\\!]^{I}_{[\\![C]\\!]\Theta}$.

  2. 2.

$[\\![pt(C,\mathfrak{x})]\\!]^{I}_{\Theta}=[\\![\mathfrak{x}]\\!]^{I}_{\Theta}=I(\mathfrak{x})=[\\![\mathfrak{x}]\\!]^{I}_{[\\![C]\\!]\Theta}$.

  3. 3.

$[\\![pt(C,r_{1}\mbox{ }aop\mbox{
}r_{2})]\\!]^{I}_{\Theta}=[\\![pt(C,r_{1})\mbox{ }aop\mbox{
}pt(C,r_{2})]\\!]^{I}_{\Theta}=$
$[\\![pt(C,r_{1})\mbox{ }]\\!]^{I}_{\Theta}\ aop\ [\\![\mbox{
}pt(C,r_{2})]\\!]^{I}_{\Theta}=[\\![r_{1}]\\!]^{I}_{[\\![C]\\!]\Theta}\ aop\
[\\![r_{2}]\\!]^{I}_{[\\![C]\\!]\Theta}$.

  4. 4.

Similarly, $\llbracket pt(C,\sum\limits_{i\in
K}r_{i})\rrbracket_{\Theta}^{I}=\llbracket\sum\limits_{i\in
K}r_{i}\rrbracket^{I}_{\llbracket C\rrbracket\Theta}$.

  5. 5.

$[\\![pt(\texttt{skip},\mathbb{P}(\phi))]\\!]^{I}_{\Theta}=[\\![\mathbb{P}(\phi)]\\!]^{I}_{\Theta}=[\\![\mathbb{P}(\phi)]\\!]^{I}_{[\\![\texttt{skip}]\\!]\Theta}$.

  6. 6.

$[\\![pt(X\leftarrow
E,\mathbb{P}(\phi))]\\!]^{I}_{\Theta}=[\\![\mathbb{P}(\phi[X/E])]\\!]^{I}_{\Theta}=[\\![\mathbb{P}(wp(X\leftarrow
E,\phi))]\\!]^{I}_{\Theta}$. Since for each $\theta\in\mathbb{PS}$,
$\theta\models\phi[X/E]$ iff $\theta\models wp(X\leftarrow E,\phi)$ iff
$[\\![X\leftarrow E]\\!]\widehat{\theta}\models\phi$, then it can inferred
that
$[\\![\mathbb{P}(\phi[X/E])]\\!]^{I}_{\Theta}=[\\![\mathbb{P}(\phi)]\\!]^{I}_{[\\![X\leftarrow
E]\\!]\Theta}$.

  7. 7.

PAS: For the sake of simplicity, we assume $n=2$. No generality is lost with
this assumption. We have
$[\\![pt(X\xleftarrow[]{\$}\\{a_{1}:k_{1},a_{2}:k_{2}\\},\mathbb{P}(\phi))]\\!]^{I}_{\Theta}=[\\![a_{1}\mathbb{P}(\phi[X/k_{1}]\wedge\neg\phi[X/k_{2}])+a_{2}\mathbb{P}(\neg\phi[X/k_{1}]\wedge\phi[X/k_{2}])+(a_{1}+a_{2})\mathbb{P}(\phi[X/k_{1}]\wedge\phi[X/k_{2}])]\\!]^{I}_{\Theta}$.
Without loss generality, assume
$sp(\Theta)=\\{\theta_{1},\theta_{2},\theta_{3},\theta_{4}\\}$,
$\theta_{1}\models^{I}\phi[X/k_{1}]\wedge\neg\phi[X/k_{2}]$,
$\theta_{2}\models^{I}\neg\phi[X/k_{1}]\wedge\phi[X/k_{2}]$,
$\theta_{3}\models^{I}\phi[X/k_{1}]\wedge\phi[X/k_{2}]$,
$\theta_{4}\models^{I}\neg\phi[X/k_{1}]\wedge\neg\phi[X/k_{2}]$,
$\Theta(S_{i})=b_{i}$. Then we have
$\\![a_{1}\mathbb{P}(\phi[X/k_{1}]\wedge\neg\phi[X/k_{2}])+a_{2}\mathbb{P}(\neg\phi[X/k_{1}]\wedge\phi[X/k_{2}])+(a_{1}+a_{2})\mathbb{P}(\phi[X/k_{1}]\wedge\phi[X/k_{2}])]\\!]^{I}_{\Theta}=a_{1}b_{1}+a_{2}b_{2}+(a_{1}+a_{2})b_{3}$.

We further have
$[\\![X\xleftarrow[]{\$}\\{a_{1}:k_{1},a_{2}:k_{2}\\}]\\!](\theta_{1})\models^{I}\mathbb{P}(\phi)=a_{1}$,
$[\\![X\xleftarrow[]{\$}\\{a_{1}:k_{1},a_{2}:k_{2}\\}]\\!](\theta_{2})\models^{I}\mathbb{P}(\phi)=a_{2}$,
$[\\![X\xleftarrow[]{\$}\\{a_{1}:k_{1},a_{2}:k_{2}\\}]\\!](\theta_{3})\models^{I}\mathbb{P}(\phi)=a_{1}+a_{2}$
and
$[\\![X\xleftarrow[]{\$}\\{a_{1}:k_{1},a_{2}:k_{2}\\}]\\!](\theta_{4})\models^{I}\mathbb{P}(\phi)=0$.
Then we know
$[\\![X\xleftarrow[]{\$}\\{a_{1}:k_{1},a_{2}:k_{2}\\}]\\!](\Theta)\models^{I}\mathbb{P}(\phi)=a_{1}b_{1}+a_{2}b_{2}+(a_{1}+a_{2})b_{3}$.
This means that
$[\\![\mathbb{P}(\phi)]\\!]^{I}_{[\\![X\xleftarrow[]{\$}\\{a_{1}:k_{1},a_{2}:k_{2}\\}]\\!]\Theta}=a_{1}b_{1}+a_{2}b_{2}+(a_{1}+a_{2})b_{3}=[\\![pt(X\xleftarrow[]{\$}\\{a_{1}:k_{1},a_{2}:k_{2}\\},\mathbb{P}(\phi))]\\!]^{I}_{\Theta}$.

  8. 8.

UNITARY: Trivial.

  9. 9.

MEASURE: $[\\![X\leftleftarrows
q_{j}]\\!]\widehat{\theta}=p_{0}\widehat{\theta_{0}}+p_{1}\widehat{\theta_{1}}$,
where

$p_{0}=\sqrt{\textbf{Tr}(P^{0}_{j}\theta_{q}\theta_{q}^{\dagger})}$,
$p_{1}=\sqrt{\textbf{Tr}(P^{1}_{j}\theta_{q}\theta_{q}^{\dagger})}$,
$\theta_{0,c}=\theta_{c}[X\mapsto 0]$, $\theta_{1,c}=\theta_{c}[X\mapsto 1]$,
$\theta_{0,q}=\frac{P^{0}_{j}\theta_{q}}{\sqrt{p_{0}}}$,
$\theta_{1,q}=\frac{P^{1}_{j}\theta_{q}}{\sqrt{p_{1}}}$.

If $p_{0}=0$, then $p_{1}=1$ and
$[\\![\mathbb{P}(\phi)]\\!]_{[\\![X\leftleftarrows
q_{j}]\\!]\widehat{\theta}}=[\\![\mathbb{P}(\phi)]\\!]_{\theta_{1}}$. Note
that in this case
$[\\![\mathbb{P}(\phi)]\\!]_{\theta_{1}}=[\\![\mathbb{P}([\mathfrak{P}^{1}_{j}]\phi[X/1])]\\!]_{\theta}$.
We then know $[\\![\mathbb{P}(\phi)]\\!]_{[\\![X\leftleftarrows
q_{j}]\\!]\widehat{\theta}}=[\\![(\top\Rightarrow
P^{0}_{j})\mathbb{P}([\mathfrak{P}^{0}_{j}]\phi[X/0])+(\top\Rightarrow
P^{1}_{j})\mathbb{P}([\mathfrak{P}^{1}_{j}]\phi[X/1])]\\!]_{\theta}$.

If $p_{1}=0$, then $p_{0}=1$ and
$[\\![\mathbb{P}(\phi)]\\!]_{[\\![X\leftleftarrows
q_{j}]\\!]\widehat{\theta}}=[\\![\mathbb{P}(\phi)]\\!]_{\theta_{0}}$. Note
that in this case
$[\\![\mathbb{P}(\phi)]\\!]_{\theta_{0}}=[\\![\mathbb{P}([\mathfrak{P}^{0}_{j}]\phi[X/0])]\\!]_{\theta}$.
We then know $[\\![\mathbb{P}(\phi)]\\!]_{[\\![X\leftleftarrows
q_{j}]\\!]\widehat{\theta}}=[\\![(\top\Rightarrow
P^{0}_{j})\mathbb{P}([\mathfrak{P}^{0}_{j}]\phi[X/0])+(\top\Rightarrow
P^{1}_{j})\mathbb{P}([\mathfrak{P}^{1}_{j}]\phi[X/1])]\\!]_{\theta}$.

If $p_{0},p_{1}>0$, then
$[\\![\mathbb{P}([\mathfrak{P}^{0}_{j}]\phi[X/0])]\\!]_{\theta}=[\\![\mathbb{P}(\phi[X/0])]\\!]_{\frac{(P^{0}_{j}\otimes
I_{-j})\theta}{\sqrt{p_{0}}}}=[\\![\mathbb{P}(\phi[X/0])]\\!]_{(\theta_{c},\theta_{0,q})}=[\\![\mathbb{P}(\phi)]\\!]_{\theta_{0}}$.

Similarly,
$[\\![\mathbb{P}([\mathfrak{P}^{1}_{j}]\phi[X/1])]\\!]_{\theta}=[\\![\mathbb{P}(\phi)]\\!]_{\theta_{1}}$.

We then know $[\\![\mathbb{P}(\phi)]\\!]_{[\\![X\leftleftarrows
q_{j}]\\!]\widehat{\theta}}=[\\![(\top\Rightarrow
P^{0}_{j})\mathbb{P}([\mathfrak{P}^{0}_{j}]\phi[X/0])+(\top\Rightarrow
P^{1}_{j})\mathbb{P}([\mathfrak{P}^{1}_{j}]\phi[X/1])]\\!]_{\theta}$.

  10. 10.

SEQ:
$[\\![pt(C_{1};C_{2},\mathbb{P}(\phi))]\\!]^{I}_{\Theta}=[\\![pt(C_{1},pt(C_{2},\mathbb{P}(\phi)))]\\!]^{I}_{\Theta}=$
$[\\![pt(C_{2},\mathbb{P}(\phi))]\\!]^{I}_{[\\![C_{1}]\\!]\Theta}=[\\![\mathbb{P}(\phi)]\\!]^{I}_{[\\![C_{2}]\\!][\\![C_{1}]\\!]\Theta}=[\\![\mathbb{P}(\phi)]\\!]^{I}_{[\\![C_{1};C_{2}]\\!]\Theta}$.

  11. 11.

IF: $[\\![pt(\texttt{if}\ B\ \texttt{then}\ C_{1}\ \texttt{else}\
C_{2},\mathbb{P}(\phi))]\\!]^{I}_{\Theta}=$

$[\\![pt(C_{1},\mathbb{P}(\phi))/B+pt(C_{2},\mathbb{P}(\phi))/(\neg
B)]\\!]^{I}_{\Theta}=$

$[\\![pt(C_{1},\mathbb{P}(\phi))/B]\\!]^{I}_{\Theta}+[\\![pt(C_{2},\mathbb{P}(\phi))/(\neg
B)]\\!]^{I}_{\Theta}=$

$[\\![pt(C_{1},\mathbb{P}(\phi))]\\!]^{I}_{\downarrow_{B}\Theta}+[\\![pt(C_{2},\mathbb{P}(\phi))]\\!]^{I}_{\downarrow_{\neg
B}\Theta}=$

$[\\![\mathbb{P}(\phi)]\\!]^{I}_{[\\![C_{1}]\\!]\downarrow_{B}\Theta}+[\\![\mathbb{P}(\phi)]\\!]^{I}_{[\\![C_{2}]\\!]\downarrow_{\neg
B}\Theta}=$

$[\\![\mathbb{P}(\phi)]\\!]^{I}_{[\\![C_{1}]\\!]\downarrow_{B}\Theta+[\\![C_{2}]\\!]\downarrow_{\neg
B}\Theta}=$ $[\\![\mathbb{P}(\phi)]\\!]^{I}_{[\\![\texttt{if}\ B\
\texttt{then}\ C_{1}\ \texttt{else}\ C_{2}]\\!]\Theta}$

  12. 12.

WHILE: Without loss of generality, let
$sp(\Theta)=\\{\theta_{0,\infty},\theta_{0,0},\theta_{0,1},\ldots\\}$, in
which $\theta_{0,i}\models wp(i)$ and $\theta_{0,\infty}\models wp(\infty)$.
Equivalently, we may let $\Theta_{\theta_{0,i}}=\downarrow_{wp(i)}(\Theta)$
and $\Theta_{\theta_{0,\infty}}=\downarrow_{wp(\infty)}(\Theta)$.

Then we know $\Theta(\theta_{0,i})=[\\![\mathbb{P}(wp(i))]\\!]_{\Theta}$,
$\Theta(\theta_{0,\infty})=[\\![\mathbb{P}(wp(\infty))]\\!]_{\Theta}$.

That is,
$\Theta=[\\![\mathbb{P}(wp(\infty))]\\!]_{\Theta}\Theta_{\theta_{0,\infty}}+\displaystyle\sum_{i=0}^{\infty}[\\![\mathbb{P}(wp(i))]\\!]_{\Theta}\Theta_{\theta_{0,i}}$.

Then $[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta}$

$=[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!](\Theta(\theta_{0,\infty})\Theta_{\theta_{0,\infty}}+\displaystyle\sum_{i=0}^{\infty}\Theta(\theta_{0,i})\Theta_{\theta_{0,i}})}$

$=[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!](\Theta(S_{0,\infty})\Theta_{\theta_{0,\infty}})}+[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\displaystyle\sum_{i=0}^{\infty}\Theta(\theta_{0,i})\Theta_{\theta_{0,i}}}$

$=\Theta(\theta_{0,\infty})[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!](\Theta_{\theta_{0,\infty}})}+\displaystyle\sum_{i=0}^{\infty}\Theta(\theta_{0,i})[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta_{\theta_{0,i}}}$

By Lemma 2, we know
$[\\![WL]\\!]\Theta_{\theta_{0,i}}=[\\![(IF)^{i}]\\!]\Theta_{\theta_{0,i}}$.

Therefore,

$[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta_{\theta_{0,i}}}=[\\![\mathbb{P}(\phi)]\\!]_{[\\![(IF)^{i}]\\!]\Theta_{\theta_{0,i}}}$

By induction hypothesis we know

$[\\![\mathbb{P}(\phi)]\\!]_{[\\![(IF)^{i}]\\!]\Theta_{\theta_{0,i}}}=[\\![pt((IF)^{i},\mathbb{P}(\phi))]\\!]_{\Theta_{\theta_{0,i}}}$

Then we have

$[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta_{\theta_{0,i}}}=[\\![pt((IF)^{i},\mathbb{P}(\phi))]\\!]_{\Theta_{\theta_{0,i}}}$

Moreover,

$[\\![pt((IF)^{i},\mathbb{P}(\phi))]\\!]_{\Theta_{\theta_{0,i}}}=[\\![pt((IF)^{i},\mathbb{P}(\phi))]\\!]_{\downarrow_{wp(i)}(\Theta)}$

$=[\\![pt((IF)^{i},\mathbb{P}(\phi))/(wp(i))]\\!]_{\Theta}$

At this stage we know $[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta}=$

$\Theta(\theta_{0,\infty})[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!](\Theta_{\theta_{0,\infty}})}+\displaystyle\sum_{i=0}^{\infty}\Theta(\theta_{0,i})[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta_{\theta_{0,i}}}$

in which
$\displaystyle\sum_{i=0}^{\infty}\Theta(\theta_{0,i})[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta_{\theta_{0,i}}}=$

$[\\![\displaystyle\sum_{i=0}^{\infty}(\mathbb{P}(wp(i))(pt((IF)^{i},\mathbb{P}(\phi))/(wp(i))))]\\!]_{\Theta}$

Note that $SUM$ is short for

$\displaystyle\sum_{i=0}^{\infty}(\mathbb{P}(wp(i))(pt((IF)^{i},\mathbb{P}(\phi))/(wp(i)))).$

Then $[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta}=$

$\Theta(\theta_{0,\infty})[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!](\Theta_{\theta_{0,\infty}})}+[\\![SUM]\\!]_{\Theta}$
$=[\\![\mathbb{P}(wp(\infty))]\\!]_{\Theta}[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!](\Theta_{\theta_{0,\infty}})}+[\\![SUM]\\!]_{\Theta}.$

It remains to study
$[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta_{\theta_{0,\infty}}}$.

Note that $[\\![WL]\\!]=[\\![IF;WL]\\!]$.

We then know
$[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta_{\theta_{0,\infty}}}$
$=[\\![\mathbb{P}(\phi)]\\!]_{[\\![IF;WL]\\!]\Theta_{\theta_{0,\infty}}}$
$=[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!][\\![IF]\\!]\Theta_{\theta_{0,\infty}}}$
$=[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!][\\![\texttt{if}\ B\ \texttt{then}\
C\ \texttt{else}\mbox{ }\texttt{skip}]\\!]\Theta_{\theta_{0,\infty}}}$
$=[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!][\\![C]\\!]\Theta_{\theta_{0,\infty}}}$.

Here we also note that
$[\\![C]\\!]\Theta_{\theta_{0,\infty}}=[\\![C]\\!]\downarrow_{wp(\infty)}(\Theta)$.

Without loss of generality, let
$sp([\\![C]\\!]\Theta_{\theta_{0,\infty}})=\\{\theta_{1,\infty},\theta_{1,0},\theta_{1,1},\ldots,\\}$,
in which $\theta_{1,i}\models wp(i)$ and $\theta_{1,\infty}\models
wp(\infty)$.

Then by repeating the reasoning on the cases of $\theta_{0,i}$, we know

$[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!][\\![C]\\!]\Theta_{\theta_{0,\infty}}}=$

$[\\![\mathbb{P}(wp(\infty))]\\!]_{[\\![C]\\!]\Theta_{\theta_{0,\infty}}}[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!](\Theta_{\theta_{1,\infty}})}+[\\![SUM]\\!]_{[\\![C]\\!]\Theta_{\theta_{0,\infty}}}=$

$[\\![\mathbb{P}(wp(\infty))]\\!]_{[\\![C]\\!]\downarrow_{wp(\infty)}(\Theta)}[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!](\Theta_{\theta_{1,\infty}})}+[\\![SUM]\\!]_{[\\![C]\\!]\downarrow_{wp(\infty)}(\Theta)}$

By induction hypothesis we know

$[\\![\mathbb{P}(wp(\infty))]\\!]_{[\\![C]\\!]\downarrow_{wp(\infty)}(\Theta)}=[\\![pt(C,\mathbb{P}(wp(\infty)))]\\!]_{\downarrow_{wp(\infty)}(\Theta)}$
$=[\\![pt(C,\mathbb{P}(wp(\infty)))/wp(\infty)]\\!]_{\Theta}$

and
$[\\![SUM]\\!]_{[\\![C]\\!]\downarrow_{wp(\infty)}(\Theta)}=[\\![pt(C,SUM)/wp(\infty)]\\!]_{\Theta}$.

It then remains to study
$[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!]\Theta_{\theta_{1,\infty}}}$.

By repeating the reasoning on the cases of $\theta_{0,i}$, we know

$[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!][\\![C]\\!]\Theta_{\theta_{1,\infty}}}=$

$[\\![\mathbb{P}(wp(\infty))]\\!]_{[\\![C]\\!]\Theta_{\theta_{1,\infty}}}[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!](\Theta_{\theta_{2,\infty}})}+[\\![SUM]\\!]_{[\\![C]\\!]\Theta_{\theta_{1,\infty}}}$

in which
$\Theta_{\theta_{2,\infty}}=\downarrow_{wp(\infty)}([\\![C]\\!](\Theta_{\theta_{1,\infty}}))$.

Let
$\Theta_{\theta_{i+1,\infty}}=\downarrow_{wp(\infty)}([\\![C]\\!](\Theta_{\theta_{i,\infty}}))$.

Repeat the above procedure to infinity, we get
$[\\![pt(WL,\mathbb{P}(\phi))]\\!]_{\Theta}=[\\![\mathbb{P}(\phi)]\\!]_{[\\![WL]\\!](\Theta)}$.

  13. 13.

(SKIP-cq) Trivial.

  14. 14.

(AS-cq) $[\\![\phi[X/E]\Rightarrow
Q]\\!]^{I}_{\Theta}=\sum\limits_{\theta\models\phi[X/E]}\Theta(\theta)[\\![Q]\\!]^{I}_{\theta}$.

By what we proved in Theorem 2.2, it holds that $\theta\models^{I}\phi[X/E]$
iff $[\\![X\leftarrow E]\\!]\theta\models^{I}\phi$ for each
$\theta\in\mathbb{PS}$.

Let $\Theta^{\prime}=[\\![X\leftarrow E]\\!]\Theta$. Then
$\Theta^{\prime}(\theta^{\prime})=\sum\\{\Theta(\theta):[\\![X\leftarrow
E]\\!]\widehat{\theta}=\widehat{\theta^{\prime}}\\}$.

Note that $[\\![Q]\\!]_{\theta}=[\\![Q]\\!]_{\theta^{\prime}}$ since
$\theta_{q}=\theta^{\prime}_{q}$.

Therefore, $[\\![\phi\Rightarrow Q]\\!]^{I}_{[\\![X\leftarrow
E]\\!]\Theta}=\sum\limits_{\theta^{\prime}\models\phi}\Theta^{\prime}(\theta^{\prime})[\\![Q]\\!]^{I}_{\theta^{\prime}}=\sum\limits_{[\\![X\leftarrow
E]\\!]\theta\models^{I}\phi}\Theta(\theta)[\\![Q]\\!]^{I}_{\theta}$
$=\sum\limits_{\theta\models^{I}\phi[X/E]}\Theta(\theta)[\\![Q]\\!]^{I}_{\theta}=\llbracket\phi[X/E]\Rightarrow
Q\rrbracket_{\Theta}^{I}$.

  15. 15.

(PAS-cq) Without loss of generality, we only consider the case where $n=2$.

$[\\![pt(X\xleftarrow[]{\$}\\{a_{1}:k_{1},,a_{2}:k_{2}\\},\phi\Rightarrow
Q)]\\!]_{\Theta}=[\\![a_{1}(pt(X\leftarrow k_{1},\phi\Rightarrow
Q))+a_{2}(pt(X\leftarrow k_{2},\phi\Rightarrow Q))]\\!]_{\Theta}$
$=a_{1}[\\![pt(X\leftarrow k_{1},\phi\Rightarrow
Q)]\\!]_{\Theta}+a_{2}[\\![pt(X\leftarrow k_{2},\phi\Rightarrow
Q)]\\!]_{\Theta}$

By IH, it equals $a_{1}[\\![\phi\Rightarrow Q]\\!]_{[\\![X\leftarrow
k_{1}]\\!]\Theta}+a_{2}[\\![\phi\Rightarrow Q]\\!]_{[\\![X\leftarrow
k_{2}]\\!]\Theta}$

$=[\\![\phi\Rightarrow Q]\\!]_{a_{1}[\\![X\leftarrow
k_{1}]\\!]\Theta}+[\\![\phi\Rightarrow Q]\\!]_{a_{2}[\\![X\leftarrow
k_{2}]\\!]\Theta}$

$=[\\![\phi\Rightarrow
Q]\\!]_{[\\![X\xleftarrow[]{\$}\\{a_{1}:k_{1},a_{2}:k_{2}\\}]\\!]\Theta}$

  16. 16.

(UNITARY-cq) Let $\Theta^{\prime}=\llbracket U[\overline{q}]\rrbracket\Theta$.
Then $\Theta^{\prime}(\theta^{\prime})=\sum\\{\Theta(\theta):\llbracket
U[\overline{q}]\rrbracket\widehat{\theta}=\widehat{\theta^{\prime}}\\}$.

$[\\![\phi\Rightarrow
Q]\\!]_{\Theta^{\prime}}=\sum\limits_{\theta^{\prime}\models\phi}\Theta^{\prime}(\theta^{\prime})[\\![Q]\\!]_{\theta^{\prime}}$.

Note that $\theta\models[U_{\overline{q}}]\phi$ iff
$\theta^{\prime}\models\phi$. Then we know
$\sum\limits_{\theta^{\prime}\models\phi}\Theta^{\prime}(\theta^{\prime})[\\![Q]\\!]_{\theta^{\prime}}=\sum\limits_{\theta\models[U_{\overline{q}}]\phi}\Theta(\theta)[\\![Q]\\!]_{\llbracket
U[\overline{q}]\rrbracket\theta}$.

Now we have $[\\![Q]\\!]_{\llbracket
U[\overline{q}]\rrbracket\theta}=\textbf{Tr}(Q(U_{\overline{q}}\theta_{q})(U_{\overline{q}}\theta_{q})^{\dagger})=\textbf{Tr}(Q(U_{\overline{q}}\theta)(\theta_{q}^{\dagger}U^{\dagger}_{\overline{q}}))=\textbf{Tr}(U^{\dagger}_{\overline{q}}Q(U_{\overline{q}}\theta)\theta^{\dagger})=[\\![U^{\dagger}_{\overline{q}}QU_{\overline{q}}]\\!]_{\theta}$.

We then know $[\\![\phi\Rightarrow Q]\\!]_{\llbracket
U_{\overline{q}}\rrbracket\Theta}=\sum\limits_{\theta^{\prime}\models\phi}\Theta^{\prime}(\theta^{\prime})\llbracket
Q\rrbracket_{\theta^{\prime}}=\sum\limits_{\theta\models[U_{\overline{q}}]\phi}\Theta(\theta)\llbracket
Q\rrbracket_{\llbracket U[\overline{q}]\rrbracket\widehat{\theta}}=$

$\llbracket[U_{\overline{q}}]\phi\Rightarrow
U_{\overline{q}}^{\dagger}QU_{\overline{q}}\rrbracket_{\Theta}$.

  17. 17.

(MEASURE-cq) We first want to show that, given an arbitrary
$\theta\in\mathbb{PS}$, $\llbracket(\phi[X/0]\Rightarrow
P_{j}^{0}QP_{j}^{0})+(\phi[X/1]\Rightarrow
P_{j}^{1}QP_{j}^{1})\rrbracket_{\widehat{\theta}}^{I}=\llbracket\phi\Rightarrow
Q\rrbracket_{\llbracket X\leftleftarrows q_{j}\rrbracket\widehat{\theta}}$.

We know that $[\\![X\leftleftarrows
q_{j}]\\!]\widehat{\theta}=p_{0}\widehat{\theta_{0}}+p_{1}\widehat{\theta_{1}}$,
where

$p_{0}=\sqrt{\textbf{Tr}(P^{0}_{j}\theta_{q}\theta_{q}^{\dagger})}$,
$p_{1}=\sqrt{\textbf{Tr}(P^{1}_{j}\theta_{q}\theta_{q}^{\dagger})}$,
$\theta_{0,c}=\theta_{c}[X\mapsto 0]$,
$\theta_{1,c}=\theta_{c}\theta_{c}[X\mapsto 1]$,
$\theta_{0,q}=\frac{P^{0}_{j}\theta_{q}}{\sqrt{p_{0}}}$,
$\theta_{1,q}=\frac{P^{1}_{j}\theta_{q}}{\sqrt{p_{1}}}$.

By what we have proved beforehand, $[\\![\phi[X/0]\Rightarrow
P^{0}_{j}QP^{0}_{j}]\\!]_{\widehat{\theta}}=[\\![\phi\Rightarrow
P^{0}_{j}QP^{0}_{j}]\\!]_{[\\![X\leftarrow
0]\\!]\widehat{\theta}}=[\\![\phi\Rightarrow
P^{0}_{j}QP^{0}_{j}]\\!]_{\widehat{(\theta_{0,c},\theta_{q})}}$.

Note that
$\textbf{Tr}(P^{0}_{j}QP^{0}_{j}\theta_{q}\theta_{q}^{\dagger})=\textbf{Tr}(QP^{0}_{j}\theta_{q}\theta_{q}^{\dagger}P^{0}_{j})=p_{0}[\\![Q]\\!]_{\frac{P^{0}_{j}\theta_{q}}{\sqrt{p_{0}}}}=p_{0}[\\![Q]\\!]_{\theta_{0,q}}$.

If $\theta\models\phi[X/0]$, then $\theta_{0,c}\models\phi$ and
$[\\![\phi[X/0]\Rightarrow
P^{0}_{j}QP^{0}_{j}]\\!]_{\widehat{\theta}}=\textbf{Tr}(P^{0}_{j}QP^{0}_{j}\theta_{q}\theta_{q}^{\dagger})=p_{0}[\\![Q]\\!]_{\theta_{0,q}}=[\\![\phi\Rightarrow
Q]\\!]_{p_{0}\widehat{\theta_{0}}}$.

If $\theta\not\models\phi[X/0]$, then $\theta_{0,c}\not\models\phi$ and
$[\\![\phi[X/0]\Rightarrow
P^{0}_{j}QP^{0}_{j}]\\!]_{\widehat{\theta}}=0=[\\![\phi\Rightarrow
Q]\\!]_{p_{0}\widehat{\theta_{0}}}$.

Similarly, we can prove that $[\\![\phi[X/1]\Rightarrow
P^{1}_{j}QP^{1}_{j}]\\!]_{\widehat{\theta}}=[\\![\phi\Rightarrow
Q]\\!]_{p_{1}\widehat{\theta_{1}}}$.

Therefore, we have $[\\![pt(X\leftleftarrows q_{j},\phi\Rightarrow
Q)]\\!]_{\widehat{\theta}}=[\\![\phi\Rightarrow Q]\\!]_{[\\![X\leftleftarrows
q_{j}]\\!]\widehat{\theta}}$, which implies that $[\\![pt(X\leftleftarrows
q_{j},\phi\Rightarrow Q)]\\!]_{\Theta}=[\\![\phi\Rightarrow
Q]\\!]_{[\\![X\leftleftarrows q_{j}]\\!]\Theta}$.

  18. 18.

(SEQ-cq) Trivial.

  19. 19.

(IF-cq) $[\\![\phi\Rightarrow Q]\\!]_{[\\![\texttt{if}\ B\ \texttt{then}\
C_{1}\ \texttt{else}\ C_{2}]\\!]\Theta}=[\\![\phi\Rightarrow
Q]\\!]_{[\\![C_{1}]\\!]\downarrow_{B}\Theta+[\\![C_{2}]\\!]\downarrow_{\neg
B}\Theta}$

$=[\\![pt(C_{1},\phi\Rightarrow
Q)]\\!]_{\downarrow_{B}\Theta}+[\\![pt(C_{2},\phi\Rightarrow
Q)]\\!]_{\downarrow_{\neg B}\Theta}$

$=[\\![pt(C_{1},\phi\Rightarrow
Q)/B]\\!]_{\Theta}+[\\![pt(C_{2},\phi\Rightarrow Q)/\neg B]\\!]_{\Theta}$

$=[\\![(pt(C_{1},\phi\Rightarrow Q)/B)+(pt(C_{2},\phi\Rightarrow Q)/\neg
B)]\\!]_{\Theta}$.

  20. 20.

(WHILE-cq) The proof is similar to the proof of $pt(WHILE,\mathbb{P}(\phi))$.

∎

######  Theorem.

$\mu\models^{I}WP(C,\Phi)$ iff $[\\![C]\\!]\mu\models^{I}\Phi$.

###### Proof.

We prove by structural induction:

  1. 1.

$\mu\models^{I}WP(C,r_{1}\mbox{ }rop\mbox{ }r_{2})$ iff
$\mu\models^{I}pt(C,r_{1})\mbox{ }rop\mbox{ }pt(C,r_{2})$ iff
$[\\![pt(C,r_{1})]\\!]^{I}_{\mu}\mbox{ }rop\mbox{
}[\\![pt(C,r_{2})]\\!]^{I}_{\mu}=\top$ iff
$[\\![r_{1}]\\!]^{I}_{[\\![C]\\!]\mu}\mbox{ }rop\mbox{
}[\\![r_{2}]\\!]_{[\\![C]\\!]^{I}\mu}=\top$ iff
$[\\![C]\\!]\mu\models^{I}r_{1}\mbox{ }rop\mbox{ }r_{2}$.

  2. 2.

$\mu\models^{I}WP(C,\neg\Phi)$ iff $\mu\models^{I}\neg WP(C,\Phi)$ iff
$\mu\not\models^{I}WP(C,\Phi)$ iff $[\\![C]\\!]\mu\not\models^{I}\Phi$ iff
$[\\![C]\\!]\mu\models^{I}\neg\Phi$.

  3. 3.

$\mu\models^{I}WP(\Phi_{1}\wedge\Phi_{2})$ iff
$\mu\models^{I}WP(C,\Phi_{1})\wedge WP(C,\Phi_{2})$ iff
$\mu\models^{I}WP(C,\Phi_{1})$ and $\mu\models^{I}WP(C,\Phi_{2})$ iff
$[\\![C]\\!]\mu\models^{I}\Phi_{1}$ and $[\\![C]\\!]\mu\models^{I}\Phi_{2}$
iff $[\\![C]\\!]\mu\models^{I}\Phi_{1}\wedge\Phi_{2}$.

∎

######  Lemma.

For an arbitrary command $C$ and an arbitrary probabilistic formula $\Phi$, it
holds that $\vdash\\{WP(C,\Phi)\\}C\\{\Phi\\}$.

###### Proof.

We prove it by induction on the structure of command $C$. When $C$ is skip,
assignment, random assignment, IF or WHILE command, we can directly derive
them from the proof system PHL. The only case needs to show is the sequential
command, which means that we need to prove
$\vdash\\{WP(C_{1};C_{2},\Phi)\\}C_{1};C_{2}\\{\Phi\\}$.

By Definition 16, we have $WP(C_{1};C_{2},\Phi)=WP(C_{1},WP(C_{2},\Phi))$. By
induction hypothesis, $\vdash\\{WP(C_{2},\Phi)\\}C_{2}\\{\Phi\\}$ and
$\vdash\\{WP(C_{1},WP(C_{2},\Phi))\\}C_{1}\\{WP(C_{2};\Phi)\\}$. By inference
rule $SEQ$, we can conclude that
$\vdash\\{WP(C_{1},WP(C_{2},\Phi))\\}C_{1};C_{2}\\{\Phi\\}$ which implies that
$\vdash\\{WP(C_{1};C_{2},\Phi)\\}C_{1};C_{2}\\{\Phi\\}$.

∎

##  Appendix 0.D Application

In this section we use our QHL to verify some quantum algorithms and
protocols.

###  0.D.1 Deutsch’s algorithm

Given a boolean function $f$ with one input bit and one output bit, we want to
decide whether it is a constant function. Classically, we need to evaluate the
function twice (i.e., for input = 0 and input = 1), but quantumly, using
Deutsch’s algorithm, we only need to evaluate the function once. Recall that
the following circuit describes the operations of Deutsch’s algorithm.

The middle part is $U_{f}$, a $2$-qubit unitary that performs $U_{f}|x\otimes
y\rangle=|x\otimes(y\oplus f(x))\rangle$. The algorithm conclude that $f$ is
constant if and only if the measurement result is $0$. Deutsch’s algorithm is
described by the following commands in our QHL:

$\text{Deutsch}:=H[q_{1}];H[q_{2}];U_{f}[q_{1},q_{2}];H[q_{1}];X\leftleftarrows
q_{1}$

We now verify Deutsch’s algorithm using our QHL with deterministic assertions.
Assuming $f$ is constant, we want to show that

{ $P^{0}_{1}\land P^{1}_{2}$ } Deutsch { $X=0$ },

i.e. if before executing Deutsch, the cq-state satisfies $q_{1}=|0\rangle$ and
$q_{2}=|1\rangle$, then after the execution of Deutsch, the cq-state satisfies
$X=0$. We will prove the above Hoare trip in a bottom-up procedure.

(Claim1) { $P^{0}_{1}\land P^{1}_{2}$ } $H[q_{1}]$ {
$[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$ } (Claim2) {
$[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$ }
$H[q_{2}];U_{f}[q_{1},q_{2}];H[q_{1}];X\leftleftarrows q_{1}$ { $X=0$ } (SEQ)
{ $P^{0}_{1}\land P^{1}_{2}$ }
$H[q_{1}];H[q_{2}];U_{f}[q_{1},q_{2}];H[q_{1}];X\leftleftarrows q_{1}$ { $X=0$
} (definition) { $P^{0}_{1}\land P^{1}_{2}$ } Deutsch { $X=0$ }

Claim 1 is due to $H$ is self-inverse, i.e.
$[H_{q_{1}}]\,[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})=P^{0}_{1}\land P^{1}_{2}$,
and using (UNITARY).

For Claim 2,

(UNI) { $[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$ } $H[q_{2}]$ {
$[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$ } (Claim3) {
$[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$ }
$U_{f}[q_{1},q_{2}];H[q_{1}];X\leftleftarrows q_{1}$ { $X=0$ } (SEQ) {
$[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$ }
$H[q_{2}];U_{f}[q_{1},q_{2}];H[q_{1}];X\leftleftarrows q_{1}$ { $X=0$ }

For Claim 3,

(UNI) { $[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$ }
$U_{f}[q_{1},q_{2}]$ {
$[U^{-1}_{fq_{1},q_{2}}]\,[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$
} (Claim 4) {
$[U^{-1}_{fq_{1},q_{2}}]\,[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$
} $H[q_{1}];X\leftleftarrows q_{1}$ { $X=0$ } (SEQ) {
$[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$ }
$U_{f}[q_{1},q_{2}];H[q_{1}];X\leftleftarrows q_{1}$ { $X=0$ }

For Claim 4,

(UNI) { $[U^{-1}_{fq_{1},q_{2}}]\,[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land
P^{1}_{2})$ } $H[q_{1}]$ {
$[H_{q_{1}}]\,[U^{-1}_{fq_{1},q_{2}}]\,[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land
P^{1}_{2})$ } (Claim 5) {
$[H_{q_{1}}]\,[U^{-1}_{fq_{1},q_{2}}]\,[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land
P^{1}_{2})$ } $X\leftleftarrows q_{1}$ { $X=0$ } (SEQ) {
$[U^{-1}_{fq_{1},q_{2}}]\,[H_{q_{2}}]\,H_{q_{1}}](P^{0}_{1}\land P^{1}_{2})$ }
$H[q_{1}];X\leftleftarrows q_{1}$ { $X=0$ }

Claim 5 follows from (MEASURE) and (CONS) if we can show

$\models[H_{q_{1}}]\,[U^{-1}_{fq_{1},q_{2}}]\,[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land
P^{1}_{2})\rightarrow([\mathfrak{P}^{0}_{1}](X=0)[X/0]\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}](X=0)[X/1]\vee P^{0}_{1}).$

Therefore, we need to show that

$[\\![[H_{q_{1}}]\,[U^{-1}_{fq_{1},q_{2}}]\,[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land
P^{1}_{2})]\\!]\subseteq[\\![([\mathfrak{P}^{0}_{1}](X=0)[X/0]\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}](X=0)[X/1]\vee P^{0}_{1})]\\!]$

The right-hand side reduces to

$[\\![([\mathfrak{P}^{0}_{1}](X=0)[X/0]\vee P^{1}_{1})\wedge
P^{0}_{1}]\\!]=[\\![[\mathfrak{P}^{0}_{1}](X=0)[X/0]\land
P^{0}_{1}]\\!]=[\\![P^{0}_{1}]\\!]$

To reduce the left-hand side, we do a case analysis. If $f$ is a constant
function which maps all input to $0$, then $U_{f}$ is the identity operator.
The left-hand side reduces to

$[\\![[H_{q_{1}}]\,[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land
P^{1}_{2})]\\!]=[\\![[H_{q_{2}}](P^{0}_{1}\land
P^{1}_{2})]\\!]=[\\![P^{0}_{1}\land[H_{q_{2}}]P^{1}_{2}]\\!]\subseteq[\\![P^{0}_{1}]\\!].$

If $f$ is a constant function which maps all input to $1$, then
$U_{f}=I\otimes X$, where $I$ is identity and $X$ is the X-gate. The left-hand
side reduces to

$[\\![[H_{q_{1}}]\,[H_{q_{2}}]\,[I\otimes X]\,[H_{q_{1}}](P^{0}_{1}\land
P^{1}_{2})]\\!]=[\\![[H_{q_{2}}]\,[X_{q_{2}}](P^{0}_{1}\land
P^{1}_{2})]\\!]=[\\![P^{0}_{1}\land[H_{q_{2}}]\,[X_{q_{2}}]P^{1}_{2}]\\!]\subseteq[\\![P^{0}_{1}]\\!].$

This concludes the proof of

$\models[H_{q_{1}}]\,[U^{-1}_{fq_{1},q_{2}}]\,[H_{q_{2}}]\,[H_{q_{1}}](P^{0}_{1}\land
P^{1}_{2})\rightarrow([\mathfrak{P}^{0}_{1}](X=0)[X/0]\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}](X=0)[X/1]\vee P^{0}_{1}).$

The case when $f$ is balanced is similar.

###  0.D.2 Quantum teleportation

Quantum teleportation is a technique for transferring a qubit from a sender at
one location to a receiver at another location. The following is the circuit
representation of quantum teleportation. The circuit consumes a qubit
$|\psi\rangle$ at a location and produce $|\psi\rangle$ at another location.
The sender and receiver share a Bell state, each having one qubit. The first
two gates acting on $|0\rangle\otimes|0\rangle$ is to setup the Bell state
$\frac{1}{\sqrt{2}}(|00\rangle+|11\rangle)$. Then the sender performs a
controlled-not gate on $|\psi\rangle$ and a qubit from Bell state, a Hardmard
gate on $|\psi\rangle$, and then measurements both qubits and sends the result
of measurements to the receiver. Lastly, the receiver performs correction
according to the measurement result.

The operations can be described by the following command:

$\begin{split}&\text{Tele}:=H[q_{3}];CX[q_{3},q_{2}];CX[q_{1},q_{2}];H[q_{1}];M_{1}\leftleftarrows
q_{1};M_{2}\leftleftarrows q_{2};\\\ &\text{if }M_{2}=1\text{ then
}X[q_{3}]\text{ else skip};\text{if }M_{1}=1\text{ then }Z[q_{3}]\text{ else
skip}\end{split}$

where $X,Z,CX$ are gates. We use $\text{Tele}_{1};\text{Tele}_{2}$ to denote
the first and second line of the command.

Assuming $|\psi\rangle=|0\rangle$, we now use our proof system to prove

{ $P^{0}_{1}\land P^{0}_{2}\land P^{0}_{3}$ } Tele { $P^{0}_{3}$ }

in a bottom-up procedure.

(Claim1) { $P^{0}_{1}\land P^{0}_{2}\land P^{0}_{3}$ } $\text{Tele}_{1}$ { $V$
} (Claim2) { $V$ } $\text{Tele}_{2}$ { $P^{0}_{3}$ } (SEQ) { $P^{0}_{1}\land
P^{0}_{2}\land P^{0}_{3}$ } $\text{Tele}_{1};\text{Tele}_{2}$ { $P^{0}_{3}$ }
(definition) { $P^{0}_{1}\land P^{0}_{2}\land P^{0}_{3}$ } Tele { $P^{0}_{3}$
}

For Claim 2,

(2a) { $V\land(M_{2}=1)$ } $X[q_{3}]$ { W } (2b) { $V\land\lnot(M_{2}=1)$ }
$skip$ { W } (IF) { $V$ } $\text{if }M_{2}=1\text{ then }X[q_{3}]\text{ else
skip}$ { $W$ } (2c) { $W\land(M_{1}=1)$ } $Z[q_{3}]$ { $P^{0}_{3}$ } (2d) {
$W\land\lnot(M_{1}=1)$ } $skip$ { $P^{0}_{3}$ } (IF) { $W$ } $\text{if
}M_{1}=1\text{ then }Z[q_{3}]\text{ else skip}$ { $P^{0}_{3}$ } (SEQ) { $V$ }
$\text{if }M_{2}=1\text{ then }X[q_{3}]\text{ else skip};\text{if
}M_{1}=1\text{ then }Z[q_{3}]\text{ else skip}$ { $P^{0}_{3}$ }

where $W=((M_{1}=1)\land[Z_{q_{3}}]P_{3}^{0})\lor(\lnot(M_{1}=1)\land
P_{3}^{0})$, and $V=((M_{2}=1)\land[X_{q_{3}}]W)\lor(\lnot(M_{2}=1)\land W)$.
Here 2b and 2d is by (SKIP) and (CON), 2a and 2c is by (CON) and (UNITARY).

For Claim 1,

(UNI,SEQ) { $P^{0}_{1}\land P^{0}_{2}\land P^{0}_{3}$ }
$H[q_{3}];CX[q_{3},q_{2}];CX[q_{1},q_{2}];H[q_{1}]$ {
$[H_{q_{1}}][CX_{q_{3},q_{2}}][CX_{q_{1},q_{2}}][H_{q_{3}}](P^{0}_{1}\land
P^{0}_{2}\land P^{0}_{3})$ } (Claim3) H3 (SEQ) { $P^{0}_{1}\land
P^{0}_{2}\land P^{0}_{3}$ }
$H[q_{3}];CX[q_{3},q_{2}];CX[q_{1},q_{2}];H[q_{1}];M_{1}\leftleftarrows
q_{1};M_{2}\leftleftarrows q_{2}$ { $V$ }

where $H3=$ {
$[H_{q_{1}}][CX_{q_{3},q_{2}}][CX_{q_{1},q_{2}}][H_{q_{3}}](P^{0}_{1}\land
P^{0}_{2}\land P^{0}_{3})$ } $M_{1}\leftleftarrows q_{1};M_{2}\leftleftarrows
q_{2}$ { $V$ }. For Claim 3,

(Claim4) H4 (MEAS) { $([\mathfrak{P}^{0}_{2}]V[M_{2}/0]\vee
P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}]V[M_{2}/1]\vee P^{0}_{2})$ }
$M_{2}\leftleftarrows q_{2}$ { $V$ }  (SEQ) {
$[H_{q_{1}}][CX_{q_{3},q_{2}}][CX_{q_{1},q_{2}}][H_{q_{3}}](P^{0}_{1}\land
P^{0}_{2}\land P^{0}_{3})$ } $M_{1}\leftleftarrows q_{1};M_{2}\leftleftarrows
q_{2}$ { $V$ }

where $H4=$ { $H[q_{1}]CX[q_{1},q_{2}]CX[q_{3},q_{2}]H[q_{3}](P^{0}_{1}\land
P^{0}_{2}\land P_{3}^{0})$ } $M_{1}\leftleftarrows q_{1}$ {
$([\mathfrak{P}^{0}_{2}]V[M_{2}/0]\vee
P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}]V[M_{2}/1]\vee P^{0}_{2})$ }. For
Claim4, in order to use (MEAS), we need to prove

$\models[H_{q_{1}}][CX_{q_{1},q_{2}}][CX_{q_{3},q_{2}}][H_{q_{3}}](P^{0}_{1}\land
P^{0}_{2}\land P^{0}_{3})\rightarrow([\mathfrak{P}^{0}_{1}]\phi[M_{1}/0]\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}]\phi[M_{1}/1]\vee P^{0}_{1})$

where

$\begin{split}\phi&=([\mathfrak{P}^{0}_{2}]V[M_{2}/0]\vee
P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}]V[M_{2}/1]\vee P^{0}_{2})\\\
&=([\mathfrak{P}^{0}_{2}](((M_{2}=1)\land[X_{q_{3}}]W)\lor(\lnot(M_{2}=1)\land
W))[M_{2}/0]\vee P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}]V[M_{2}/1]\vee
P^{0}_{2})\\\ &=([\mathfrak{P}^{0}_{2}]W\vee
P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}]W\vee P^{0}_{2})\end{split}$

Note that here we abuse the notation $=$ to represent logical equivalence.
Claim 4 follows from the calculation below,

$([\mathfrak{P}^{0}_{1}]\phi[M_{1}/0]\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}]\phi[M_{1}/1]\vee P^{0}_{1})$

$=([\mathfrak{P}^{0}_{1}](([\mathfrak{P}^{0}_{2}]W\vee
P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}]W\vee
P^{0}_{2}))[M_{1}/0]\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}]\phi[M_{1}/1]\vee P^{0}_{1})$

$=([\mathfrak{P}^{0}_{1}](([\mathfrak{P}^{0}_{2}](((M_{1}=1)\land[Z_{q_{3}}]P_{3}^{0})\lor(\lnot(M_{1}=1)\land
P_{3}^{0}))\vee P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}]W\vee
P^{0}_{2}))[M_{1}/0]\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}]\phi[M_{1}/1]\vee P^{0}_{1})$

$=([\mathfrak{P}^{0}_{1}](([\mathfrak{P}^{0}_{2}](((0=1)\land[Z_{q_{3}}]P_{3}^{0})\lor(\lnot(0=1)\land
P_{3}^{0}))\vee P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}]W\vee
P^{0}_{2}))[M_{1}/0]\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}]\phi[M_{1}/1]\vee P^{0}_{1})$

$=([\mathfrak{P}^{0}_{1}](([\mathfrak{P}^{0}_{2}](P_{3}^{0}\vee
P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}]W\vee
P^{0}_{2}))[M_{1}/0]\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}]\phi[M_{1}/1]\vee P^{0}_{1})$

$=([\mathfrak{P}^{0}_{1}](([\mathfrak{P}^{0}_{2}](P_{3}^{0}\vee
P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}](((M_{1}=1)\land[Z_{q_{3}}]P_{3}^{0})\lor(\lnot(M_{1}=1)\land
P_{3}^{0}))\vee P^{0}_{2}))[M_{1}/0]\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}]\phi[M_{1}/1]\vee P^{0}_{1})$

$=([\mathfrak{P}^{0}_{1}](([\mathfrak{P}^{0}_{2}](P_{3}^{0}\vee
P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}](((0=1)\land[Z_{q_{3}}]P_{3}^{0})\lor(\lnot(0=1)\land
P_{3}^{0}))\vee P^{0}_{2}))\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}]\phi[M_{1}/1]\vee P^{0}_{1})$

$=([\mathfrak{P}^{0}_{1}](([\mathfrak{P}^{0}_{2}](P_{3}^{0}\vee
P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}](P_{3}^{0}\vee
P^{0}_{2})))\vee P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}]\phi[M_{1}/1]\vee
P^{0}_{1})$

$=([\mathfrak{P}^{0}_{1}](([\mathfrak{P}^{0}_{2}]P_{3}^{0}\vee
P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}](P_{3}^{0}\vee
P^{0}_{2})))\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}](([\mathfrak{P}^{0}_{2}]((M_{1}=1)\land[Z_{q_{3}}]P_{3}^{0})\lor(\lnot(M_{1}=1)\land
P_{3}^{0})\vee P^{1}_{2})\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}]W\vee
P^{0}_{2}))[M_{1}/1]\vee P^{0}_{1})$

$=([\mathfrak{P}^{0}_{1}](([\mathfrak{P}^{0}_{2}](P_{3}^{0}\vee
P^{1}_{2}))\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}](P_{3}^{0}\vee
P^{0}_{2})))\vee
P^{1}_{1})\wedge([\mathfrak{P}^{1}_{1}](([\mathfrak{P}^{0}_{2}][Z_{q_{3}}](P_{3}^{0}\vee
P^{1}_{2}))\wedge([\mathfrak{P}^{1}_{2}][X_{q_{3}}][Z_{q_{3}}](P_{3}^{0}\vee
P^{0}_{2})))\vee P^{0}_{1})$

$=([\mathfrak{P}^{0}_{1}](([\mathfrak{P}^{0}_{2}](P_{3}^{0}\vee
P^{1}_{2}))\wedge([\mathfrak{P}^{1}_{2}](P_{3}^{1}\vee P^{0}_{2})))\vee
P^{1}_{1})\wedge$
$([\mathfrak{P}^{1}_{1}](([\mathfrak{P}^{0}_{2}](P_{3}^{0}\vee
P^{1}_{2}))\wedge([\mathfrak{P}^{1}_{2}](P_{3}^{1}\vee P^{0}_{2})))\vee
P^{0}_{1})=:\chi$

which is implied by
$[H_{q_{1}}][CX_{q_{3},q_{2}}][CX_{q_{1},q_{2}}][H_{q_{3}}](P^{0}_{1}\land
P^{0}_{2}\land P^{0}_{3})$. The implication holds because for all pure cq-
state $\theta$,

if
$\theta\in[\\![[H_{q_{1}}][CX_{q_{3},q_{2}}][CX_{q_{1},q_{2}}][H_{q_{3}}](P^{0}_{1}\land
P^{0}_{2}\land P^{0}_{3})]\\!]$,

then
$H_{q_{3}}CX_{q_{1},q_{2}}CX_{q_{3},q_{2}}H_{q_{1}}\theta\in[\\![(P^{0}_{1}\land
P^{0}_{2}\land
P^{0}_{3})]\\!]=\\{\theta^{\prime}|\theta^{\prime}_{q}=|000\rangle\\}$,

then
$\theta\in\\{\theta^{\prime}|\theta^{\prime}_{q}=H_{q_{1}}CX_{q_{3},q_{2}}CX_{q_{1},q_{2}}H_{q_{3}}|000\rangle\\}=\\{\theta^{\prime}|\theta^{\prime}_{q}=\frac{1}{{2}}(|000\rangle+|100\rangle+|011\rangle+|111\rangle)\\}$.

That is,
$[\\![[H_{q_{1}}][CX_{q_{3},q_{2}}][CX_{q_{1},q_{2}}][H_{q_{3}}](P^{0}_{1}\land
P^{0}_{2}\land P^{0}_{3})]\\!]\subseteq[\\![\chi]\\!]$

The case for $|\phi\rangle=|1\rangle$ is similar. By linearity, we have shown
that teleportation works using QHL.