Relational Proofs for Quantum Programs

TL;DR

This paper introduces a relational program logic for quantum programs, enabling verification of complex properties like security, reliability, and equivalence in quantum computing, based on a novel quantum analogue of probabilistic couplings.

Contribution

It presents a new relational logic framework for quantum programs, expanding verification capabilities for quantum security, teleportation, and quantum walk equivalences.

Findings

Verified uniformity in quantum Bernoulli factory samples

Assessed reliability of quantum teleportation under noise

Proved security of quantum one-time pad and quantum walk equivalence

Abstract

Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a quantum analogue of probabilistic couplings. We use our logic to verify non-trivial relational properties of quantum programs, including uniformity for samples generated by the quantum Bernoulli factory, reliability of quantum teleportation against noise (bit and phase flip), security of quantum one-time pad and equivalence of quantum walks.

Equations

$$P_1\sim P_2:A\Rightarrow B$$

$$P_1\equiv q:=|0⟩;q:=H[q];Q_1,P_2\equiv q:=|0⟩;Q_2;q:=H[q].$$

$$Q_1$$

$$Q_2$$

$$\rho=\frac{2}{3}|0\rangle\langle 0|+\frac{1}{3}|+\rangle\langle+|=\frac{1}{6}\left(\begin{array}[]{cc}5&1\\ 1&1\end{array}\right).$$

$$X=\left(\begin{array}[]{cc}0&1\\ 1&0\end{array}\right),\qquad Z=\left(\begin{array}[]{cc}1&0\\ 0&-1\end{array}\right),\qquad H=\frac{1}{\sqrt{2}}\left(\begin{array}[]{cc}1&1\\ 1&-1\end{array}\right),$$

$$\displaystyle M_{0}=|0\rangle\langle 0|=\left(\begin{array}[]{cc}1&0\\ 0&0\end{array}\right),\qquad\qquad\qquad M_{1}=|1\rangle\langle 1|=\left(\begin{array}[]{cc}0&0\\ 0&1\end{array}\right),$$

$$\displaystyle M_{0}^{\prime}=|+\rangle\langle+|=\frac{1}{2}\left(\begin{array}[]{cc}1&1\\ 1&1\end{array}\right),\qquad\qquad\ \ \ M_{1}^{\prime}=|-\rangle\langle-|=\frac{1}{2}\left(\begin{array}[]{cc}1&-1\\ -1&1\end{array}\right).$$

$$p(1)=\mathit{tr}(M_{1}^{\prime}\rho)=tr\left[\frac{1}{2}\left(\begin{array}[]{cc}1&-1\\ -1&1\end{array}\right)\cdot\frac{1}{6}\left(\begin{array}[]{cc}5&1\\ 1&1\end{array}\right)\right]=\frac{1}{12}\cdot tr\left(\begin{array}[]{cc}4&0\\ -4&0\end{array}\right)=\frac{1}{3}$$

$$M_{1}^{\prime}\rho M_{1}^{\prime}/p(1)=\frac{1}{2}\left(\begin{array}[]{cc}1&-1\\ -1&1\end{array}\right)\cdot\frac{1}{6}\left(\begin{array}[]{cc}5&1\\ 1&1\end{array}\right)\cdot\frac{1}{2}\left(\begin{array}[]{cc}1&-1\\ -1&1\end{array}\right)\div\frac{1}{3}=\frac{1}{2}\left(\begin{array}[]{cc}1&-1\\ -1&1\end{array}\right).$$

$$|\Phi ⟩⟨\Phi |=\frac{1}{2}(|0⟩⟨0|\otimes |0⟩⟨0|+|0⟩⟨1|\otimes |0⟩⟨1|+|1⟩⟨0|\otimes |1⟩⟨0|+|1⟩⟨1|\otimes |1⟩⟨1|)$$

$$probabilitydistributions\iff densityoperatorsmarginaldistributions\iff partialtraces$$

$$⟨{\mathbf{Unif}}_{{\mathcal{H}}_1}=\frac{1}{2}(|0⟩⟨0|+|1⟩⟨1|),{\mathbf{Unif}}_{{\mathcal{H}}_2}=\frac{1}{2}(|0⟩⟨0|+|1⟩⟨1|)⟩.$$

$$P::=\mathbf{skip}$$

$$\begin{array}{rl}& (\mathrm{Sk})⟨\mathbf{skip},\rho ⟩\to ⟨\downarrow ,\rho ⟩(\mathrm{In})⟨q:=|0⟩,\rho ⟩\to ⟨\downarrow ,{\rho }_0^q⟩\\ & (\mathrm{UT})⟨\overline{q}:=U[\overline{q}],\rho ⟩\to ⟨\downarrow ,U\rho U^{†}⟩(\mathrm{SC})\frac{⟨P_1,\rho ⟩\to ⟨P_1^{\prime },{\rho }^{\prime }⟩}{⟨P_1;P_2,\rho ⟩\to ⟨P_1^{\prime };P_2,{\rho }^{\prime }⟩}\\ & (\mathrm{IF})⟨\mathbf{if}(\square m\cdot \mathcal{M}[\overline{q}]=m\to P_m)\mathbf{fi},\rho ⟩\to ⟨P_m,M_m\rho M_m^{†}⟩\\ & (\mathrm{L}0)⟨\mathbf{while}\mathcal{M}[\overline{q}]=1\mathbf{do}P\mathbf{od},\rho ⟩\to ⟨\downarrow ,M_0\rho M_0^{†}⟩\\ & (\mathrm{L}1)⟨\mathbf{while}\mathcal{M}[\overline{q}]=1\mathbf{do}P\mathbf{od},\rho ⟩\to ⟨P;\mathbf{while}\mathcal{M}[\overline{q}]=1\mathbf{do}P\mathbf{od},M_1\rho M_1^{†}⟩\end{array}$$

$$[[P]](\rho )=\sum \left\{|{\rho }^{\prime }:⟨P,\rho ⟩{\to }^{\ast }⟨\downarrow ,{\rho }^{\prime }⟩|\right\},$$

$$⟨Q_2,\rho ⟩\to ⟨q:=Z[q],{\rho }_0⟩\to ⟨\downarrow ,{\rho }_0^{\prime }⟩,⟨Q_2,\rho ⟩\to ⟨q:=H[q],{\rho }_1⟩\to ⟨\downarrow ,{\rho }_1^{\prime }⟩,$$

$$\displaystyle\rho_{0}=M_{0}^{\prime}\rho M_{0}^{\prime}=\frac{1}{3}\left(\begin{array}[]{cc}1&1\\ 1&1\end{array}\right),\qquad$$

$$\displaystyle\rho_{1}=M_{1}^{\prime}\rho M_{1}^{\prime}=\frac{1}{6}\left(\begin{array}[]{cc}1&-1\\ -1&1\end{array}\right),\qquad$$

$$\Gamma ⊢P_1\sim P_2:A\Rightarrow B$$

$$\Gamma \models P_1\sim P_2:A\Rightarrow B$$

$$tr(A\rho )\le tr(B\sigma )+tr(\rho )-tr(\sigma ).$$

$$⊢P_1\sim P_2:({=}_{\mathcal{B}})\Rightarrow ({=}_{sym}).$$

$$\llbracket P_{1}\rrbracket(\mathit{tr}_{\langle 2\rangle}(\rho))=\llbracket P_{2}\rrbracket(\mathit{tr}_{\langle 1\rangle}(\rho))=\frac{1}{4}\left(\begin{array}[]{cc}1&-1\\ -1&3\end{array}\right)\times{\mathrm{tr}}(\rho)$$

$$\begin{array}{rl}& \{A\}\{\mathrm{SC}:\Gamma \}\\ & P_1\sim P_2(R)\\ & \{B\}\end{array}$$

$$\{{=}_{\mathcal{B}}\}\{I\otimes I\}$$

$$q:=|0⟩;\sim q:=|0⟩;$$

$$\{I\otimes I\}\{\mathrm{SC}:{\mathcal{M}}^{\prime }\approx {\mathcal{M}}^{\prime }\}$$

$$q:=H[q];\sim \mathbf{skip};$$

$$\{I\otimes I\}\{\mathrm{SC}:\mathcal{M}\approx {\mathcal{M}}^{\prime }\}$$

$$Q_1;\sim Q_2;$$

$$\left\{B=\frac{1}{2}[I\otimes I+(I\otimes H)S(I\otimes H)]\right\}$$

$$\mathbf{skip};\sim q:=H[q];$$

$$\left\{({=}_{sym})=\frac{1}{2}[I\otimes I+S]\right\}$$

$$\begin{split}&({\rm Skip})\ \ \vdash\mathbf{Skip}\sim\mathbf{Skip}:A\Rightarrow A\\ &({\rm Init})\ \ \vdash q_{1}:=|0\rangle\sim q_{2}:=|0\rangle:\sum_{i,j}(|i\rangle_{q_{1}\langle 1\rangle}\langle 0|\otimes|j\rangle_{q_{2}\langle 2\rangle}\langle 0|)A(|0\rangle_{q_{1}\langle 1\rangle}\langle i|\otimes|0\rangle_{q_{2}\langle 2\rangle}\langle j|)\Rightarrow A\\ &({\rm UT})\ \ \vdash\overline{q_{1}}:=U_{1}\left[\overline{q_{1}}\right]\sim\overline{q_{2}}:=U_{2}\left[\overline{q_{2}}\right]:\left(U_{1}^{\dagger}\otimes U_{2}^{\dagger}\right)A\left(U_{1}\otimes U_{2}\right)\Rightarrow A\\ &({\rm SC})\ \ \ \frac{\vdash P_{1}\sim P_{2}:A\Rightarrow B\qquad\vdash P_{1}^{\prime}\sim P_{2}^{\prime}:B\Rightarrow C}{\vdash P_{1};P_{1}^{\prime}\sim P_{2};P_{2}^{\prime}:A\Rightarrow C}\\ &({\rm IF})\ \ \ \frac{\vdash P_{1m}\sim P_{2n}:B_{mn}\Rightarrow C\ {\rm for\ every}\ (m,n)\in S\qquad\forall\ m,n:\ \ \models P_{1m},P_{2n}\ {\rm lossless}}{\begin{array}[]{cc}\vdash\mathbf{if}\ (\square m\cdot\mathcal{M}_{1}[\overline{q}]=m\rightarrow P_{1m})\ \mathbf{fi}\sim\mathbf{if}\ (\square n\cdot\mathcal{M}_{2}[\overline{q}]=n\rightarrow P_{2n})\ \mathbf{fi}:\\ \sum_{(m,n)\in S}\left(M_{1m}^{{\dagger}}\otimes M_{2n}^{\dagger}\right)B_{mn}\left(M_{1m}\otimes M_{2n}\right)\Rightarrow C\end{array}}\\ &({\rm LP})\ \frac{\begin{array}[]{c}\models\mathbf{while}\ {\mathcal{M}}_{i}[\overline{q}]=1\ \mathbf{do}\ P_{i}\ \mathbf{od}\text{\ lossless}\ (i=1,2)\\ \vdash P_{1}\sim P_{2}:B\Rightarrow(M_{10}\otimes M_{20})^{\dagger}A(M_{10}\otimes M_{20})+(M_{11}\otimes M_{21})^{\dagger}B(M_{11}\otimes M_{21})\end{array}}{\begin{array}[]{l}\vdash\mathbf{while}\ {\mathcal{M}}_{1}[\overline{q}]=1\ \mathbf{do}\ P_{1}\ \mathbf{od}\sim\mathbf{while}\ {\mathcal{M}}_{2}[\overline{q}]=1\ \mathbf{do}\ P_{2}\ \mathbf{od}:\\ \qquad\qquad\qquad(M_{10}\otimes M_{20})^{\dagger}A(M_{10}\otimes M_{20})+(M_{11}\otimes M_{21})^{\dagger}B(M_{11}\otimes M_{21})\Rightarrow A\end{array}}\end{split}$$

$$\begin{split}&(\mathrm{Init\text{-}L})\ \ \ \vdash q_{1}:=|0\rangle\sim\mathbf{skip}:\sum_{i}\left(|i\rangle_{q_{1}\langle 1\rangle}\langle 0|\right)A\left(|0\rangle_{q_{1}\langle 1\rangle}\langle i|\right)\Rightarrow A\\ &({\rm UT\text{-}L})\ \ \ \vdash\overline{q_{1}}:=U_{1}\left[\overline{q_{1}}\right]\sim\mathbf{skip}:U_{1}^{\dagger}AU_{1}\Rightarrow A\\ &({\rm IF\text{-}L})\ \ \ \frac{\vdash P_{1m}\sim P:B_{m}\Rightarrow C\ {\rm for\ every}\ m}{\vdash\mathbf{if}\ (\square m\cdot M_{1}[\overline{q}]=m\rightarrow P_{1m})\ \mathbf{fi}\sim P:\sum_{m}M_{1m}^{{\dagger}}B_{m}M_{1m}\Rightarrow C}\\ &({\rm LP\text{-}L})\ \frac{\begin{array}[]{c}\models\mathbf{while}\ {\mathcal{M}}_{1}[\overline{q}]=1\ \mathbf{do}\ P_{1}\ \mathbf{od}\text{\ lossless}\quad\vdash P_{1}\sim\mathbf{skip}:B\Rightarrow M_{10}^{\dagger}AM_{10}+M_{11}^{\dagger}BM_{11}\end{array}}{\vdash\mathbf{while}\ {\mathcal{M}}_{1}[\overline{q}]=1\ \mathbf{do}\ P_{1}\mathbf{od}\sim\mathbf{skip}:M_{10}^{\dagger}AM_{10}+M_{11}^{\dagger}BM_{11}\Rightarrow A}\end{split}$$

Full text

quantum programming, verification, relational properties, coupling

††copyright: rightsretained††doi: 10.1145/3371089††journalyear: 2020††journal: PACMPL††journalvolume: 4††journalnumber: POPL††article: 21††publicationmonth: 1††ccs: Theory of computation Quantum computation theory††ccs: Theory of computation Hoare logic††ccs: Theory of computation Program verification

1. Introduction

Program verification is traditionally focused on proving properties of a single program execution. In contrast, relational verification aims to prove properties about two program executions. In some cases, such as program refinement and program equivalence, the goal is to relate executions of two different programs on equal or related inputs. However, some properties consider two executions of the same program (with related inputs); examples include information flow policies (non-interference: two runs of a program on states that only differ in their secret have equal visible effects) and robustness ($k$-Lipschitz continuity: running a program on two initial states at distance $d$ yields two final states at distance at most $k\cdot d$). In the probabilistic setting, relational verification can also show that a program outputs a uniform distribution, or that two programs yield “approximately equal” distributions. By taking suitable instantiations of approximate equality, relational verification has found success in cryptography (Barthe et al., 2009), machine learning (Barthe et al., 2018) and differential privacy (Barthe et al., 2012, 2016).

This paper develops a relational program logic, called rqPD, for a core quantum programming language. Our logic is based on the interpretation of predicates as physical observables, mathematically modelled as Hermitian operators (D’Hondt and Panangaden, 2006), and is inspired by the qPD program logic (Ying, 2011, 2016) for quantum programs. Concretely, our judgments have the form:

[TABLE]

where $P_{1}$ and $P_{2}$ are quantum programs, and precondition $A$ and postcondition $B$ are Hermitian operators over the tensor product Hilbert spaces of $P_{1}$ and $P_{2}$. We define an interpretation of these judgments, develop a rich set of sound proof rules, and show how these rules can be used to verify relational properties for quantum programs.

Technical challenges and solutions.

The central challenge for building a useful relational logic is to find an interpretation of judgments that captures properties of interest, while guaranteeing soundness of a convenient set of proof rules. This challenge is not unique to quantum programs. In the probabilistic setting (Barthe et al., 2009, 2015), one solution is to interpret judgments in terms of probabilistic couplings, a standard abstraction from probability theory (Lindvall, 2002; Thorisson, 2000; Villani, 2008). The connection with probabilistic couplings has many advantages: (i) it builds the logic on an abstraction that has proven to be useful for probabilistic reasoning; (ii) it identifies natural extensions of the logic; and (iii) it suggests other applications and properties that can be handled by similar techniques. Unfortunately, the quantum setting raises additional challenges. Notably, we may need to reason about entangled quantum states. There are some existing proposals of analogue of probabilistic couplings in the quantum setting (see (Kümmerer and Schwieger, 2016; Winter, 2016)). In particular, Zhou et al. (2019a) addressed this issue by developing a notion of quantum coupling, and validated their definition by showing an analogue of Strassen’s theorem (Strassen, 1965).111Informally, Strassen’s theorem states that there exists a $B$-coupling between two distributions $\mu$ and $\mu^{\prime}$ over sets $X$ and $X^{\prime}$ respectively iff for every subset $Y$ in the support of $\mu$, $\mu(Y)\leq\mu(B(Y))$, where $B(Y)$ is the set-theoretic image of $Y$ under $B$. In this work, we base our notion of valid judgment on this definition of quantum coupling.

Once the interpretation of the logic is fixed, the next challenge is to define a useful set of proof rules. As in other relational logics, we need structural rules and three kinds of construct-specific rules. Synchronous rules apply when $P_{1}$ and $P_{2}$ have the same top-level construct and operates on both programs, whereas the left and right rules only operate on one of the two programs. In the quantum setting, the main difficulties are:

• •

Structural rules: many useful rules are not sound in the quantum setting or require further hypotheses; in particular, in the presence of entanglement — an indispensable resource in quantum computation and communication. We generalise the core judgment to track and enforce the hypotheses required to preserve soundness.

• •

Construct-specific rules: all proof rules of quantum Hoare logic qPD can be directly generalised into quantum relational logic rqPD (see Subsection 5.2). Although these directly generalised rules are useful, they do not fully capture the essence of quantum relational reasoning (see Subsection 5.3). Synchronous proof rules for classical control-flow constructs, i.e.  conditionals and loops, generally require that the two programs follow the same control flow path, so that they execute in lockstep. In order to retain soundness in our setting, we introduce a measurement condition ensuring that corresponding branches in the control flow are taken with equal probabilities.

Simplifying side conditions.

Checking measurement conditions is often challenging. To make this step easier, we introduce a simplified version of rqPD where assertions are modelled as projective predicates, or equivalently, (closed) subspaces of the state Hilbert space — a special case of Hermitian operators. The restriction to projective predicates leads to simpler inference rules and easier program verification, at the cost of expressiveness (Zhou et al., 2019b). In particular, checking measurement conditions reduces to showing that a program condition lies in a subspace (with probability $1$), a task that is often simpler. We provide a formal comparison between the original logic system rqPD and its simplified version, and leverage this comparison to relate our work with a recent proposal for a quantum relational Hoare logic with projective predicates (Unruh, 2019b).

Applications.

To test its effectiveness, we apply rqPD to verify non-trivial relational properties of several quantum programs, including uniformity for samples generated by the quantum Bernoulli factory, reliability of quantum teleportation against noise (bit and phase flip), equivalence of quantum walks and security of quantum one-time pad. Using our simplified rqPD, we are able to verify the relational properties of some more sophisticated quantum programs, for example, equivalence of quantum walks with different coin tossing operators.

Working Example.

We will use the following pair of simple quantum programs as our working example to illustrate our basic ideas along the way:

Example 1.1.

Let $q$ be a qubit (quantum bit). Consider two programs:

[TABLE]

In both, $q$ is initialised in a basis state $|0\rangle$. $P_{1}$ applies the Hadamard gate $H$ to $q$ and executes $Q_{1}$, while $P_{2}$ first executes $Q_{2}$ and then applies $H$ to $q$. The subprograms $Q_{1},Q_{2}$ are as follows:

[TABLE]

where ${\mathcal{M}},{\mathcal{M}}^{\prime}$ are the measurement in the computational basis $|0\rangle,|1\rangle$ and the measurement in basis $|\pm\rangle=\frac{1}{\sqrt{2}}(|0\rangle\pm|1\rangle)$ respectively. Intuitively, $Q_{1}$ first performs ${\mathcal{M}}$ on $q$, then applies either the Pauli gate $X$ or Hadamard gate $H$, depending on whether the measurement outcome is [math] or $1$. But $Q_{2}$ uses the outcomes of a different measurement ${\mathcal{M}}$ to choose between the Pauli gate $Z$ and Hadamard gate $H$.

Obviously, programs $P_{1},P_{2}$ have similar structures. The logic rqPD developed in this paper will enable us to specify and prove some interesting symmetry between them.

2. Mathematical Preliminaries

We assume basic familiarity with Hilbert spaces, see Nielsen and Chuang (2002) for an introduction.

Quantum states.

The state space of a quantum system is a Hilbert space $\mathcal{H}$. In this paper, we only consider finite-dimensional $\mathcal{H}$. A pure state of the quantum system is modelled by a (column) vector in $\mathcal{H}$ of length $1$; we use the Dirac notation ($|\varphi\rangle,|\psi\rangle$) to denote pure states. For example, qubit $q$ in Example 1.1 has the $2$-dimensional Hilbert space as its state space; it can be in basis states $|0\rangle,|1\rangle$ as well as in their superpositions $|+\rangle,|-\rangle=\frac{1}{\sqrt{2}}(|0\rangle\pm|1\rangle)$. An operator $A$ in an $d$-dimensional Hilbert space $\mathcal{H}$ is represented as an $d\times d$ matrix. Its trace is defined as $\mathit{tr}(A)=\sum_{i}\langle i|A|i\rangle$, where $\{|i\rangle\}$ is an orthonormal basis of $\mathcal{H}$. A positive operator $\rho$ in $\mathcal{H}$ is called a partial density operator if its trace satisfies $\mathit{tr}(\rho)\leq 1$; if $tr(\rho)=1$, then $\rho$ is called a density operator. A mixed state of a quantum system is a distribution over pure states. If state $|\psi_{i}\rangle$ has probability $p_{i}$, the mixed state can be represented by a density operator $\rho=\sum_{i}p_{i}|\psi_{i}\rangle\langle\psi_{i}|$, where row vector $\langle\psi_{i}|$ stands for the conjugate transpose of $|\psi_{i}\rangle$. For example, if qubit $q$ is in state $|0\rangle$ with probability $\frac{2}{3}$ and in $|+\rangle$ with probability $\frac{1}{3}$, then its state can be described by density operator

[TABLE]

We write $\mathcal{D}^{\leq}(\mathcal{H})$ and $\mathcal{D}(\mathcal{H})$ for the set of partial density operators and the set of density operators in $\mathcal{H}$, respectively. For any $\rho\in\mathcal{D}^{\leq}(\mathcal{H})$, the support ${\rm supp}(\rho)$ of $\rho$ is defined as the span of the eigenvectors of $\rho$ with nonzero eigenvalues.

Operations on states.

A basic operation on a (closed) quantum system is modelled as a unitary operator $U$ such that $U^{{\dagger}}U=I_{\mathcal{H}}$, where † stands for conjugate and transpose. For example, the Pauli and Hadamard gates used in Example 1.1 are:

[TABLE]

and $X,Z,H$ transform states $|0\rangle,|1\rangle$ to $X|0\rangle=|1\rangle,\ X|1\rangle=|0\rangle;\ Z|0\rangle=|0\rangle,\ Z|1\rangle=-|1\rangle;\ H|0\rangle=|+\rangle,\ H|1\rangle=|-\rangle$, respectively.

Another basic operation is measurement. A physical observable is modelled by an operator $A$ in $\mathcal{H}$ that is Hermitian, i.e., $A^{\dagger}=A$. An operator $P$ is a projection onto a (closed) subspace of $\mathcal{H}$ if and only if it is Hermitian (i.e. $P^{\dagger}=P$) and idempotent (i.e. $P^{2}=P$). Quantum measurements are constructed from observables $A$. An eigenvector of $A$ is a non-zero vector $|\psi\rangle\in\mathcal{H}$ such that $A|\psi\rangle=\lambda|\psi\rangle$ for some complex number $\lambda$ (indeed, $\lambda$ must be real when $A$ is Hermitian). In this case, $\lambda$ is called an eigenvalue of $A$. For each eigenvalue $\lambda$, the set $\{|\psi\rangle:A|\psi\rangle=\lambda|\psi\rangle\}$ of eigenvectors corresponding to $\lambda$ and zero vector is a (closed) subspace of $\mathcal{H}$. We write $P_{\lambda}$ for the projection onto this subspace. By the spectral decomposition (Nielsen and Chuang, 2002, Theorem 2.1), $A$ can be decomposed as a sum $A=\sum_{\lambda}\lambda P_{\lambda}$ where $\lambda$ ranges over all eigenvalues of $A$. Moreover, ${\mathcal{M}}=\{P_{\lambda}\}_{\lambda}$ is a (projective) measurement.

If we perform ${\mathcal{M}}$ on the quantum system in state $\rho$, then outcome $\lambda$ is obtained with probability $p_{\lambda}=\mathit{tr}(P_{\lambda}^{\dagger}P_{\lambda}\rho)=\mathit{tr}(P_{\lambda}\rho),$ and after that, the system will be in state $(P_{\lambda}\rho P_{\lambda})/p_{\lambda}$. Therefore, the expectation of $A$ in state $\rho$ is $\llbracket A\rrbracket_{\rho}=\sum_{\lambda}p_{\lambda}\cdot\lambda=\sum_{\lambda}\lambda\mathit{tr}(P_{\lambda}\rho)=\mathit{tr}(A\rho).$ For instance, the measurements in Example 1.1 are defined as ${\mathcal{M}}=\{M_{0},M_{1}\},{\mathcal{M}}^{\prime}=\{M_{0}^{\prime},M_{1}^{\prime}\}$ with

[TABLE]

If we perform ${\mathcal{M}}^{\prime}$ on a qubit in (mixed) state $\rho$ given in equation (1), then the probability that we get outcome “$1$” is

[TABLE]

and after that, the qubit’s state will change to

[TABLE]

Similarly, the probability of outcome “[math]” is $p(0)=\frac{2}{3}$, and then the state changes to $|+\rangle\langle+|$.

We will use observables as predicates in our logic. To compare two operators $A$ and $B$ in a Hilbert space $\mathcal{H}$, we will use the Löwner order between operators defined as follows: $A\sqsubseteq B$ if and only if $B-A$ is positive. A quantum predicate (D’Hondt and Panangaden, 2006) (or an effect) in a Hilbert space $\mathcal{H}$ is an observable (a Hermitian operator) $A$ in $\mathcal{H}$ with $0\sqsubseteq A\sqsubseteq I$, where [math] and $I$ are the zero operator and the identity operator in $\mathcal{H}$, respectively.

Tensor Products of quantum states.

Let $\mathcal{H}_{1},\mathcal{H}_{2}$ be the state Hilbert spaces of two quantum systems considered in isolation. Then the composite system has state space modeled by the tensor product $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$. The notion of partial trace is needed to extract the state of a subsystem. Formally, the partial trace over $\mathcal{H}_{1}$ is a mapping $\mathit{tr}_{1}(\cdot)$ from operators on $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$ to operators in $\mathcal{H}_{2}$ defined by the following equation: $\mathit{tr}_{1}(|\varphi_{1}\rangle\langle\psi_{1}|\otimes|\varphi_{2}\rangle\langle\psi_{2}|)=\langle\psi_{1}|\varphi_{1}\rangle\cdot|\varphi_{2}\rangle\langle\psi_{2}|$ for all $|\varphi_{1}\rangle,|\psi_{1}\rangle\in\mathcal{H}_{1}$ and $|\varphi_{2}\rangle,|\psi_{2}\rangle\in\mathcal{H}_{2}$ together with linearity. The partial trace $\mathit{tr}_{2}(\cdot)$ over $\mathcal{H}_{2}$ can be defined symmetrically. Suppose that we have a composite system of two subsystems with state spaces $\mathcal{H}_{1},\mathcal{H}_{2}$, respectively, and it is in (mixed) state $\rho$. Then the states of the first and second subsystems can be described by $\mathit{tr}_{2}(\rho),\mathit{tr}_{1}(\rho)$, respectively. For example, if the subsystems are both qubits, and they are maximally entangled; i.e. in state $|\Phi\rangle=\frac{1}{\sqrt{2}}(|00\rangle+|11\rangle)$ or equivalently

[TABLE]

then the partial traces ${\mathrm{tr}}_{1}(|\Phi\rangle\langle\Phi|)=\frac{1}{2}(|0\rangle\langle 0|+|1\rangle\langle 1|)\text{\ and\ }{\mathrm{tr}}_{2}(|\Phi\rangle\langle\Phi|)=\frac{1}{2}(|0\rangle\langle 0|+|1\rangle\langle 1|)$ describe states of the second and first subsystems, respectively.

3. Quantum Couplings and Liftings

3.1. Quantum Couplings

To relate pairs of quantum programs, our program logic will rely on a quantum version of probabilistic coupling. In the probabilistic world, a coupling for two discrete distributions $\mu_{1}$ and $\mu_{2}$ over sets $A_{1}$ and $A_{2}$ is a discrete distribution $\mu$ over $A_{1}\times A_{2}$ such that the first and second marginals of $\mu$ are equal to $\mu_{1}$ and $\mu_{2}$ respectively. A coupling $\mu$ is an $R$-lifting for $\mu_{1}$ and $\mu_{2}$ if additionally its support is included in $R$, i.e.  every element outside $R$ has probability zero.

In order to define the quantum analogue of couplings, we apply a correspondence between the probabilistic and quantum worlds (Nielsen and Chuang, 2002):

[TABLE]

This leads to the following definition of quantum coupling.

Definition 3.1 (Coupling).

Let $\rho_{1}\in\mathcal{D}^{\leq}(\mathcal{H}_{1})$ and $\rho_{2}\in\mathcal{D}^{\leq}(\mathcal{H}_{2})$. Then $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$ is called a coupling for $\left\langle\rho_{1},\rho_{2}\right\rangle$ if $\mathit{tr}_{1}(\rho)=\rho_{2}$ and $\mathit{tr}_{2}(\rho)=\rho_{1}$.

Proposition 3.1 (Trace equivalence).

If $\rho$ is a coupling for $\left\langle\rho_{1},\rho_{2}\right\rangle$, then they have the same trace: ${\mathrm{tr}}(\rho)={\mathrm{tr}}(\rho_{1})={\mathrm{tr}}(\rho_{2})$.

The following are examples of quantum couplings. They are quantum generalisations of several typical examples of (discrete) probabilistic couplings (see (Barthe et al., 2019)). From these simple examples, we can see a close and natural correspondence as well as some essential differences between probabilistic coupling and their quantum counterparts. Our first example shows that couplings always exist.

Example 3.1.

Let $\rho_{1}\in\mathcal{D}(\mathcal{H}_{1})$ and $\rho_{2}\in\mathcal{D}(\mathcal{H}_{2})$ be density operators. The tensor product $\rho_{\otimes}=\rho_{1}\otimes\rho_{2}$ is a coupling for $\left\langle\rho_{1},\rho_{2}\right\rangle$.

Just like the case for probabilistic couplings, there can be more than one quantum coupling between two operators.

Example 3.2.

Let $\mathcal{H}$ be a $d$-dimensional Hilbert space. Let $\mathcal{B}=\{|i\rangle\}$ be an orthonormal basis of $\mathcal{H}$. Then the uniform density operator over $\mathcal{H}$ is $\mathbf{Unif}_{\mathcal{H}}=\frac{1}{d}\sum_{i}|i\rangle\langle i|.$ For each unitary operator $U$ in $\mathcal{H}$, we write $U(\mathcal{B})=\{U|i\rangle\}$, which is also an orthonormal basis of $\mathcal{H}$. Then $\rho_{U}=\frac{1}{d}\sum_{i}(|i\rangle U|i\rangle)(\langle i|\langle i|U^{\dagger})$ is a coupling for $\left\langle\mathbf{Unif}_{\mathcal{H}},\mathbf{Unif}_{\mathcal{H}}\right\rangle$. Indeed, the arbitrariness of $U$ shows that there are (uncountably) infinitely many couplings for $\left\langle\mathbf{Unif}_{\mathcal{H}},\mathbf{Unif}_{\mathcal{H}}\right\rangle$. For instance, the maximally entangled state $|\Phi\rangle\langle\Phi|$ in equation (2) is such a coupling for

[TABLE]

Example 3.3.

Let $\rho$ be a partial density operator in $\mathcal{H}$. Then by the spectral decomposition theorem (Nielsen and Chuang, 2002, Theorem 2.1), $\rho$ can be written as $\rho=\sum_{i}p_{i}|i\rangle\langle i|$ for some orthonormal basis $\mathcal{B}=\{|i\rangle\}$ and $p_{i}\geq 0$ with $\sum_{i}p_{i}\leq 1$. We define $\rho_{{\rm id}(\mathcal{B})}=\sum_{i}p_{i}|ii\rangle\langle ii|.$ Then it is easy to see that $\rho_{{\rm id}(\mathcal{B})}$ is a coupling for $\left\langle\rho,\rho\right\rangle$. An essential difference between this example and its classical counterpart (see (Hsu, 2017) Example 2.1.5) is that $\rho$ might be decomposed with other orthonormal bases, say $\mathcal{D}=\{|j\rangle\}$: $\rho=\sum_{j}q_{j}|j\rangle\langle j|.$ In general, $\rho_{{\rm id}(\mathcal{B})}\neq\rho_{{\rm id}(\mathcal{D})}$, and we can define a different coupling for $\left\langle\rho,\rho\right\rangle$: $\rho_{{\rm id}(\mathcal{D})}=\sum_{j}q_{j}|jj\rangle\langle jj|.$

3.2. Quantum Lifting

Although there can be many couplings for two operators, it is usually not simple to find one suited to our application. As said at the beginning of this section, lifting can help for this purpose. The definition of liftings smoothly generalises to the quantum case.

Definition 3.2.

Let $\rho_{1}\in\mathcal{D}^{\leq}(\mathcal{H}_{1})$ and $\rho_{2}\in\mathcal{D}^{\leq}(\mathcal{H}_{2})$, and let $\mathcal{X}$ be (the projection onto) a (closed) subspace of $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$. Then $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$ is called a witness of the lifting $\rho_{1}\mathcal{X}^{\#}\rho_{2}$ if:

1. (1)

$\rho$* is a coupling for $\left\langle\rho_{1},\rho_{2}\right\rangle$;* 2. (2)

${\rm supp}(\rho)\subseteq\mathcal{X}$.

Example 3.4.

The following are examples of quantum liftings.

1. (1)

The coupling $\rho_{U}$ for the uniform density operator and itself in Example 3.2 is a witness for the lifting $\mathbf{Unif}_{\mathcal{H}}\mathrel{\mathcal{X}(\mathcal{B},U)^{\#}}\mathbf{Unif}_{\mathcal{H}}$, where $\mathcal{X}(\mathcal{B},U)={\rm span}\{|i\rangle U|i\rangle\}$ is a subspace of $\mathcal{H}\otimes\mathcal{H}.$ 2. (2)

The coupling $\rho_{{\rm id}(\mathcal{B})}$ in Example 3.3 is a witness of the lifting $\rho(=_{\mathcal{B}})^{\#}\rho$, where $(=_{\mathcal{B}})\equiv{\rm span}\{|ii\rangle\}$ defined by the orthonormal basis $\mathcal{B}=\{|i\rangle\}$ is a subspace of $\mathcal{H}\otimes\mathcal{H}$. It is interesting to note that the maximally entangled state $|\Psi\rangle=\frac{1}{\sqrt{d}}\sum_{i}|ii\rangle$ is in $=_{\mathcal{B}}$. 3. (3)

The coupling $\rho_{{\rm id}(\mathcal{B})}$ in Example 3.3 is a witness of the lifting $\rho(=_{\mathit{sym}})^{\#}\rho$, defining $=_{\mathit{sym}}$ to be the symmetrisation operator, i.e. $(=_{\mathit{sym}})\equiv\frac{1}{2}(I\otimes I+S),$ where $S$ is the SWAP operator defined by $S|\varphi,\psi\rangle=|\psi,\varphi\rangle$ for any $|\varphi\rangle,|\psi\rangle\in\mathcal{H}$ together with linearity. Operator $S$ is independent of the basis, and given any orthonormal basis $\{|i\rangle\}$ of $\mathcal{H}$, $S$ has the following form: $\mathrm{S}=\sum_{ij}|i\rangle\langle j|\otimes|j\rangle\langle i|.$ 4. (4)

The coupling $\rho_{1}\otimes\rho_{2}$ in Example 3.1 is a witness of the lifting $\rho_{1}\mathrel{(\mathcal{H}_{1}\otimes\mathcal{H}_{2})^{\#}}\rho_{2}$.

The two operators $=_{\mathcal{B}}$ and $=_{\mathit{sym}}$ in the above example represents two different kind of symmetry between two quantum systems with the same state Hilbert space $\mathcal{H}$. They will be used to describe relational properties of the two quantum programs $P_{1},P_{2}$ in Example 1.1. Liftings of equality are especially interesting for verification, since they can be interpreted as relating equivalent quantum systems. The following proposition characterizes these liftings.

Proposition 3.2.

Let $\rho_{1},\rho_{2}\in\mathcal{D}^{\leq}(\mathcal{H})$. The following statements are equivalent:

$\rho_{1}=\rho_{2}$; 2. 2.

there exists an orthonormal basis $\mathcal{B}$ s.t. $\rho_{1}(=_{\mathcal{B}})^{\#}\rho_{2}$; 3. 3.

$\rho_{1}(=_{\mathit{sym}})^{\#}\rho_{2}$.

We see from Example 3.4 and Proposition 3.2 that in the quantum world, equality has different generalisations $=_{\mathcal{B}}$ and $=_{\mathit{sym}}$. Our logic will establish the existence of a lifting of equality, which then implies equality of density operators, i.e., equivalence of quantum states.

The notion of quantum lifting can be further generalised to a quantitative version, which will be more convenient in defining the semantics of our logic. We first recall a notation introduced in D’Hondt and Panangaden (2006): $\rho\models_{\lambda}A\ {\rm means}\ \mathit{tr}(A\rho)\geq\lambda$. It can be understood as a quantitative satisfaction relation between a state $\rho$ and an observable $A$ with a real number $\lambda>0$ as a threshold.

Definition 3.3.

Let $\rho_{1}\in\mathcal{D}^{\leq}(\mathcal{H}_{1})$ and $\rho_{2}\in\mathcal{D}^{\leq}(\mathcal{H}_{2})$, let $A$ be an observable in $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$, and let $\lambda>0$. Then $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$ is called a witness of the $\lambda$-lifting $\rho_{1}A^{\#}\rho_{2}$ if:

1. (1)

$\rho$* is a coupling for $\left\langle\rho_{1},\rho_{2}\right\rangle$;* 2. (2)

$\rho\models_{\lambda}A$.

It is obvious that whenever $A$ is the projection onto subspace $\mathcal{X}$ and $\lambda=\mathit{tr}(\rho)$, then the above definition degenerates to Definition 3.2.

3.3. Separable versus Entangled Liftings

Entanglement presents a major difference between classical and quantum systems and is responsible for most of the advantages of quantum computing and communication over their classical counterparts. A partial density operator $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$ is said to be separable if there exist $\rho_{mi}\in\mathcal{D}^{\leq}(\mathcal{H}_{i})$ $(i=1,2)$ such that $\rho=\sum_{m}\left(\rho_{m1}\otimes\rho_{m2}\right).$ A (mixed) state $\rho$ in $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$ is said to be entangled if it is not separable. Indeed, the notions of separability and entanglement can be defined for a general positive operator (rather than density operator).

The following proposition shows that entanglement can provide a stronger witness of lifting even with respect to a separable observable $A$; that is, sometimes an entangled witness is possible but separable witness does not exist (the proof is given in (Barthe et al., 2019)).

Proposition 3.3.

There are states $\rho_{i}$ in $\mathcal{H}_{i}$ $(i=1,2)$, separable observable $A$ over $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$, entangled state $\rho$ in $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$, and $\lambda>0$ such that:

1. (1)

$\rho$* is a witness of $\lambda$-lifting $\rho_{1}A^{\#}\rho_{2}$; and* 2. (2)

any separable state $\sigma$ in $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$ is not a witness of $\lambda$-lifting $\rho_{1}A^{\#}\rho_{2}$.

4. Quantum Programming Language

We recall the syntax and semantics for a quantum programming language given in (Ying, 2011, 2016). Let $\mathit{Var}$ be a set of quantum variables. For each $q\in\mathit{Var}$, we write $\mathcal{H}_{q}$ for its state Hilbert space.

Definition 4.1 (Syntax).

Quantum programs are defined by the following syntax:

[TABLE]

The initialisation $q:=|0\rangle$ sets quantum variable $q$ to a basis state $|0\rangle$. The statement $\overline{q}:=U[\overline{q}]$ means that unitary transformation $U$ is applied to register $\overline{q}$. The $\mathbf{if}$-statement is a quantum generalisation of a classical case statement. In executing it, measurement ${\mathcal{M}}=\{M_{m}\}$ is performed on $\overline{q}$, and then a subprogram $P_{m}$ is selected to be executed next according to the outcome $m$ of measurement. The $\mathbf{while}$-statement is a quantum generalisation of the classical while loop. The measurement in it has only two possible outcomes [math], $1$; if the outcome [math] is observed then the program terminates, otherwise the program executes the subprogram $P$ and continues.

We write $\mathit{var}(P)$ for the set of quantum variables occurring in a quantum program $P$. Then tensor product $\mathcal{H}_{P}=\bigotimes_{q\in\mathit{var}(P)}\mathcal{H}_{q}$ is the state Hilbert space of $P$. A configuration is a pair $C=\langle P,\rho\rangle,$ where $P$ is a program or the termination symbol $\downarrow$, and $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P})$ is a partial density operator modeling the state of quantum variables.

Definition 4.2 (Operational Semantics).

The operational semantics of quantum programs is defined as a transition relation $\rightarrow$ by the transition rules in Fig. 1.

The transitions in rules (IF), (L0) and (L1) are essentially probabilistic. In both if and while statements, a measurement is performed at the beginning, and then the program enters different branches based on the measurement outcome. For each outcome $m$, the transition in (IF) happens with probability $p_{m}=\mathit{tr}(M_{m}^{\dagger}M_{m}\rho),$ and the program state $\rho$ is changed to $\rho_{m}=M_{m}\rho M_{m}^{\dagger}/p_{m}.$ In rule (L0) and (L1) the outcome “[math]” occurs with the probability $p_{0}={\mathrm{tr}}(M_{0}\rho M_{0}^{\dagger})$, and the program terminates in state $M_{0}\rho M_{0}^{\dagger}/p_{0}$; otherwise, with the probability $p_{1}={\mathrm{tr}}(M_{1}\rho M_{1}^{\dagger})$, the outcome “$1$” occurs, the program state is changed to $M_{1}\rho M_{1}^{\dagger}/p_{1}$, and then the program executes the loop body $P$ and goes back to the beginning of the loop. We follow a convention suggested by Selinger (2004a) to combine probability $p_{m}$ and density operator $\rho_{m}$ into a partial density operator $M_{m}\rho M_{m}^{\dagger}=p_{m}\rho_{m}.$ This convention is useful for presenting the operational semantics as a non-probabilistic transition system, simplifying the presentation.

Definition 4.3 (Denotational Semantics).

For any quantum program $P$, its semantic function is the mapping $\llbracket P\rrbracket:\mathcal{D}^{\leq}(\mathcal{H}_{P})\rightarrow\mathcal{D}^{\leq}(\mathcal{H}_{P})$ defined as follows: for every $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P})$,

[TABLE]

where $\rightarrow^{\ast}$ is the reflexive and transitive closure of $\rightarrow$, and $\left\{\!|\cdot|\!\right\}$ denotes a multi-set.

For instance, let us consider program $Q_{2}$ in our working example 1.1 with input $\rho$ given in equation (1). According to Definition 4.2, it has two transitions:

[TABLE]

where:

[TABLE]

According to Definition 4.3, the output is \llbracket Q_{2}\rrbracket(\rho)=\rho_{0}^{\prime}+\rho_{1}^{\prime}=\frac{1}{3}\left(\begin{array}[]{cc}1&-1\\ -1&2\end{array}\right). Furthermore, one can show that for any possible input $\rho$ with trace one, programs $P_{1},P_{2}$ in Example 1.1 have the same output: \llbracket P_{1}\rrbracket(\rho)=\llbracket P_{2}\rrbracket(\rho)=\frac{1}{4}\left(\begin{array}[]{cc}1&-1\\ -1&3\end{array}\right).

The soundness of some of the proof rules in probabilistic relational Hoare logic requires programs to terminate (Barthe et al., 2009). The same is true in the quantum setting.

Definition 4.4.

A quantum program $P$ is called lossless, written $\models P\ {\rm lossless}$, if its semantics function $\llbracket P\rrbracket$ is trace-preserving; that is, $\mathit{tr}(\llbracket P\rrbracket(\rho))=\mathit{tr}(\rho)$ for all $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P})$.

For example, programs $P_{1}$ and $P_{2}$ in Example 1.1 are both lossless.

Remark 4.1.

The lossless property of quantum loop $\mathbf{while}\ {\mathcal{M}}[\overline{q}]=1\ \mathbf{do}\ P\ \mathbf{od}$ was previously studied (Ying et al., 2013). Let the semantic function of loop body $P$ be given in Kraus operator-sum form: $\llbracket P\rrbracket(\rho)=\sum_{i}E_{i}\rho E_{i}^{\dagger}.$ We define (super-)operator $\mathcal{E}$ by $\mathcal{E}(\rho)=\sum_{i}(M_{1}^{{\dagger}}E_{i}^{\dagger})\rho(E_{i}M_{1})$ for every $\rho$. A square matrix $X$ is called an eigenvector of $\mathcal{E}$ corresponding to an eigenvalue $\lambda$ if $\mathcal{E}(X)=\lambda X$. It was shown that the loop is lossless if and only if any eigenvector of $\mathcal{E}$ corresponding to an eigenvalue with modulus $1$ is traceless.

5. Relational program logic

We adopt standard conventions and notations for relational program logics. For each quantum variable $q\in\mathit{Var}$, we assume two tagged copies $q\langle 1\rangle$ and $q\langle 2\rangle$, and their state Hilbert spaces are the same as that of $q$: $\mathcal{H}_{q\langle 1\rangle}=\mathcal{H}_{q\langle 2\rangle}=\mathcal{H}_{q}$. For $i=1,2$, if $X\subseteq\mathit{Var}$, then we write $X\langle i\rangle=\{q\langle i\rangle\mid q\in X\}$. Furthermore, for every quantum program $P$ with $\mathit{var}(P)\subseteq\mathit{Var}$, we write $P\langle i\rangle$ for the program obtained by replacing each quantum variable $q$ in $P$ with $q\langle i\rangle$. Also, for each operator $A$ in $\mathcal{H}_{X}=\bigotimes_{q\in X}\mathcal{H}_{q}$, we write $A\langle i\rangle$ for the corresponding operator of $A$ in $\mathcal{H}_{X\langle i\rangle}=\bigotimes_{q\in X}\mathcal{H}_{q\langle i\rangle}$. For simplicity, we will drop the tags whenever they can be understood from the context; for example, we often simply write $A\otimes B$ instead of $A\langle 1\rangle\otimes B\langle 2\rangle$.

5.1. Judgments and Satisfaction

Judgments in our logic are of the form

[TABLE]

where $P_{1}$ and $P_{2}$ are quantum programs, $A$ and $B$ are quantum predicates in $\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}$, and $\Gamma$ is a set of measurement or separability conditions. If $\Gamma=\{\Sigma_{1},...,\Sigma_{n}\}$, then for any $\rho\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}\right)$, $\rho\models\Gamma$ means $\rho\models\Sigma_{i}$ for all $i=1,...,n$. We defer the definition of measurement or separability condition $\Sigma_{i}$ for now, simply assuming a given notion of satisfaction $\rho\models\Sigma_{i}$. In particular, if $\Gamma=\emptyset$, then we simply write $\vdash P_{1}\sim P_{2}:A\Rightarrow B$ for $\Gamma\vdash P_{1}\sim P_{2}:A\Rightarrow B$.

Definition 5.1.

The judgment $\Gamma\vdash P_{1}\sim P_{2}:A\Rightarrow B$ is valid, written:

[TABLE]

if for every $\rho\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}\right)$ such that $\rho\models\Gamma$, there exists a quantum coupling $\sigma$ for $\left\langle\llbracket P_{1}\rrbracket(\mathit{tr}_{\langle 2\rangle}(\rho)),\llbracket P_{2}\rrbracket(\mathit{tr}_{\langle 1\rangle}(\rho))\right\rangle$ such that

[TABLE]

We will often use $\rho\models P_{1}\sim P_{2}:A\Rightarrow B$ as shorthand.

The above definition differs from validity in probabilistic relational Hoare logic in several ways. Except the set $\Gamma$ of measurability and separability conditions (explained below), lifting does not appear explicitly. However, the existence of a lifting can be established from inequality (5) under mild conditions, as we now explain. First, we note that $\mathit{tr}(\rho)-\mathit{tr}(\sigma)$ captures the non-termination probability of the programs, as in the (non-relational) quantum program logic qPD. To see a clearer probabilistic-quantum correspondence, let us consider the simple case where both $P_{1}$ and $P_{2}$ are lossless. Then $\mathit{tr}(\rho)-\mathit{tr}(\sigma)=0$ and inequality (5) is simplified to $\mathit{tr}(A\rho)\leq\mathit{tr}(B\sigma)$, or equivalently: ${\rm for\ any}\ \lambda>0,\ \rho\models_{\lambda}A\Rightarrow\sigma\models_{\lambda}B.$ This is a real number-valued analogue of boolean-valued proposition “$\rho\in A\Rightarrow\sigma\in B$”. Therefore, for any $\lambda>0$, if $\rho\models_{\lambda}A$, then $\sigma\models_{\lambda}B$ and combined with the assumption that $\sigma$ is a coupling for $\left\langle\llbracket P_{1}\rrbracket(\mathit{tr}_{\langle 2\rangle}(\rho)),\llbracket P_{2}\rrbracket(\mathit{tr}_{\langle 1\rangle}(\rho))\right\rangle$, we see that $\sigma$ is a witness for $\lambda$-lifting $\llbracket P_{1}\rrbracket(\mathit{tr}_{\langle 2\rangle}(\rho))B^{\#}\llbracket P_{2}\rrbracket(\mathit{tr}_{\langle 1\rangle}(\rho))$.

An interesting symmetry between programs $P_{1},P_{2}$ in our working example 1.1 can be expressed as the following judgment:

[TABLE]

where precondition $=_{\mathcal{B}}$ is the equality defined by the computational basis $\mathcal{B}=\{|0\rangle,|1\rangle\}$ of a qubit; i.e. $(=_{\mathcal{B}})=\mathit{span}\{|00\rangle,|11\rangle\}=|00\rangle\langle 00|+|11\rangle\langle 11|$ [see Example 3.4 2)], and postcondition $=_{\mathit{sym}}$ is the projector onto the symmetric space [see Example 3.4 3)]. The validity of this judgment can be checked by the denotational semantics of $P_{1},P_{2}$. We first observe that for any $\rho\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}}\right)$, ${\mathrm{tr}}(=_{\mathcal{B}}\rho)\leq{\mathrm{tr}}(\rho)$. Moreover, we have:

[TABLE]

by noting that ${\mathrm{tr}}(\mathit{tr}_{\langle 2\rangle}(\rho))={\mathrm{tr}}(\mathit{tr}_{\langle 1\rangle}(\rho))={\mathrm{tr}}(\rho)$. As shown in Example 3.4 (3), lifting $\llbracket P_{1}\rrbracket(\mathit{tr}_{\langle 2\rangle}(\rho))$ $(=_{\mathit{sym}})^{\#}\llbracket P_{2}\rrbracket(\mathit{tr}_{\langle 1\rangle}(\rho))$ holds and, suppose $\sigma$ is a witness, then we have ${\mathrm{tr}}(=_{sym}\sigma)={\mathrm{tr}}(\sigma)$ and therefore, ${\mathrm{tr}}(=_{\mathcal{B}}\rho)\leq{\mathrm{tr}}(=_{sym}\sigma)$ as ${\mathrm{tr}}(\rho)={\mathrm{tr}}(\sigma)$ according to Proposition 3.1, which actually implies the validity of judgment (6).

In the remainder of this section, we gradually develop the proof system for our logic rqPD. At the same time, we will see how the proof rules in rqPD can be used to verify judgment (6). For readability, we first give a proof outline of judgment (6) in Fig. 2, where a judgment $\Gamma\vdash P_{1}\sim P_{2}:A\Rightarrow B$ derived by an inference rule $R$ in rqPD is displayed as

[TABLE]

5.2. Basic Construct-Specific Rules

As usual, the proof system consists of two categories of rules: construct-specific rules and structural rules. Let us start from a set of construct-specific rules that can be directly adapted from quantum Hoare logic qPD (Ying, 2011, 2016). They include two-side rules and one-side rules given in Figs. 3 and 4, respectively. It is worth noting that all of these rules do not introduce any measurement or separability condition. These rules are easy to understand if compared with the corresponding rules of qPD, which are displayed in (Barthe et al., 2019), and those of probabilistic logic pRHL. For the working example 1.1, these rules are used to prove the following judgments in Fig. 2:

1. (1)

$\vdash q:=|0\rangle\sim q:=|0\rangle:(=_{{\mathcal{B}}})\Rightarrow I\otimes I$ by rule (Conseq) and (Init); 2. (2)

$\vdash q:=H[q]\sim\mathbf{skip}:I\otimes I\Rightarrow I\otimes I$ by rule (UT-L); 3. (3)

$\vdash\mathbf{skip}\sim q:=H[q]:B\Rightarrow(=_{sym})$ by rule (UT-R); and 4. (4)

$\vdash q:=X[q]\sim q:=Z[q]:A_{00}\Rightarrow B$ and $\vdash q:=H[q]\sim q:=H[q]:A_{11}\Rightarrow B$ by rule (UT).

As we will see in Section 6, these basic rules are already enough to verify interesting relational properties of quantum programs, including security of quantum one-time pad.

Remark 5.1.

Note that in rule (IF) the branches of two case statements are not required to match exactly. Whenever there is an one-to-one correspondence between the outcomes of measurement $\mathcal{M}_{1}$ and $\mathcal{M}_{2}$, then (IF) can be simplified to (IF-w) in Fig. 5.

5.3. Measurement Conditions

The straightforward generalisations of the proof rules for case statements and loops in qPD given in the above subsection are not strong enough for more complicated applications of rqPD. In particular, they do not reveal the subtle differences between the relational and non-relational properties of quantum programs. To understand this point, let us take a closer look at derivation of the judgment about two if statements $Q_{1}$ and $Q_{2}$ in Fig. 2. Let us first list all derivable judgments of possible combinations of branches as follows:

1. (1)

$\vdash q:=X[q]\sim q:=Z[q]:A_{00}\Rightarrow B$ and $\vdash q:=H[q]\sim q:=H[q]:A_{11}\Rightarrow B$; 2. (2)

$\vdash q:=X[q]\sim q:=H[q]:A_{01}\Rightarrow B$ and $\vdash q:=H[q]\sim q:=Z[q]:A_{10}\Rightarrow B$

where $A_{00},A_{11}$ and $B$ are given as in Fig. 2 and

[TABLE]

Applying rule (IF) directly we obtain: $\vdash Q_{1}\sim Q_{2}:\ A\Rightarrow B,$ where

[TABLE]

Then, using rule (UT-L), (UT-R) and (Init) for the rest parts of the programs, we are only able to derive $\vdash P_{1}\sim P_{2}:\ \frac{7}{8}I\otimes I\Rightarrow\ =_{sym}.$ However, $=_{\mathcal{B}}\ \not\sqsubseteq\frac{7}{8}I\otimes I$, so the rule (IF) is too weak to derive judgment (6) as we desire. A similar argument shows that rules (IF-L) and (IF-R) are also too weak.

We have more examples (e.g., Example 6.1) showing that some important relational properties cannot be verified simply using rules (IF) and (LP). The reason can be seen from the soundness proof of (IF) and (LP) (Barthe et al., 2019), where we only use a part of the output states to construct the coupling, so for a given postcondition, the derivable preconditions are sometimes too weak. To resolve this issue, we need to capture more relational information between two programs. A crucial issue in developing inference rules for relational reasoning is to guarantee that two programs $P_{1}$ and $P_{2}$ under comparison execute in lockstep. In probabilistic relational Hoare logic, a side-condition $\Theta\Rightarrow e_{1}=e_{2}$ is introduced for this purpose, where $\Theta$ is the precondition, $e_{1}$ and $e_{2}$ are the guards in $P_{1}$ and $P_{2}$, respectively. In the quantum case, branching (control flow) is determined by the measurement outcomes. So, more sophisticated rules for case analysis, loops, and conditionals in rqPD involve measurement conditions.

Definition 5.2.

Let ${\mathcal{M}}_{1}=\{M_{1m}\}$ and ${\mathcal{M}}_{2}=\{M_{2m}\}$ be two measurements with the same set $\{m\}$ of possible outcomes in $\mathcal{H}_{P_{1}}$ and $\mathcal{H}_{P_{2}}$, respectively, and let $\rho\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}\right)$. Then we say that $\rho$ satisfies ${\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}$, written $\rho\models{\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}$, if ${\mathcal{M}}_{1}$ and ${\mathcal{M}}_{2}$ produce equal probability distributions when applied to $\rho$. That is, for all $m$, we have: $\mathit{tr}(M_{1m}\mathit{tr}_{\langle 2\rangle}(\rho)M_{1m}^{\dagger})=\mathit{tr}(M_{2m}\mathit{tr}_{\langle 1\rangle}(\rho)M_{2m}^{\dagger}).$

Intuitively, the above measurement conditions mean that $P_{1}$ and $P_{2}$ enter the corresponding branches with the same probability (and thus execute in lockstep).

The above definition is enough for relating measurements in case statements. But when dealing with loops, we have to consider the measurements in the loop guards together with the loop bodies. To address this issue, we further introduce the following definition:

Definition 5.3.

Let $P_{1}$ and $P_{2}$ be two programs, and let ${\mathcal{M}}_{1}=\{M_{10},M_{11}\}$, ${\mathcal{M}}_{2}=\{M_{20},M_{21}\}$ be boolean-valued measurements in $\mathcal{H}_{P_{1}},\mathcal{H}_{P_{2}}$, respectively. Then for any $\rho\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}\right)$, we say that $\rho$ satisfies $({\mathcal{M}}_{1},P_{1})\approx({\mathcal{M}}_{2},P_{2})$, written

[TABLE]

if ${\mathcal{M}}_{1}$ and ${\mathcal{M}}_{2}$ produce equal probability distributions in iterations of $P_{1}$ and $P_{2}$, respectively; that is, for all $n\geq 0$:

[TABLE]

where $\mathcal{E}_{ij}(\cdot)=M_{ij}(\cdot)M_{ij}^{\dagger}$ for $i=1,2$ and $j=0,1$.

In the above definition, equation (7) is required to hold for all $n\geq 0$ (and thus, for infinitely many $n$). But the next lemma shows that it can be actually checked within a finite number of steps when the state Hilbert spaces are finite-dimensional, as in our setting. Therefore, an algorithm for checking the measurement condition $({\mathcal{M}}_{1},P_{1})\approx({\mathcal{M}}_{2},P_{2})$ can be designed and incorporated into the tools (e.g. theorem prover) implementing our logic in the future.

Lemma 5.1.

Let $d_{i}=\dim\mathcal{H}_{P_{i}}$ $(i=1,2)$. If (7) holds for any $0\leq n\leq d_{1}^{2}+d_{2}^{2}-1$, then it holds for all $n\geq 0$.

Note that a branching structure appears after a measurement is performed. To describe it, we introduce the following:

Definition 5.4.

Let ${\mathcal{M}}_{1}=\{M_{1m}\}$ and ${\mathcal{M}}_{2}=\{M_{2m}\}$ be as in Definition 5.2, and let $A$ and $B_{m}$ be quantum predicates in $\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}.$ We define:

[TABLE]

if for any $\rho\models{\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}$, and for each $m$, there exists a coupling $\sigma_{m}$ for \big{\langle}M_{1m}\mathit{tr}_{\langle 2\rangle}(\rho)M_{1m}^{\dagger}, M_{2m}\mathit{tr}_{\langle 1\rangle}(\rho)M_{2m}^{\dagger}\big{\rangle} such that

[TABLE]

For the working example 1.1, one may check ${\mathcal{M}}\approx{\mathcal{M}}^{\prime}\models I\otimes I\Rightarrow\{A_{00},A_{11}\}$ as shown in Fig. 2. To see this, suppose $\rho\models{\mathcal{M}}\approx{\mathcal{M}}^{\prime}$. For $m=0$, $M_{0}\mathit{tr}_{\langle 2\rangle}(\rho)M_{0}=p_{0}|0\rangle\langle 0|$ and $M_{0}^{\prime}\mathit{tr}_{\langle 1\rangle}(\rho)M_{0}^{\prime}=p_{0}|+\rangle\langle+|$ with parameter $p_{0}={\mathrm{tr}}(M_{0}\mathit{tr}_{\langle 2\rangle}(\rho)M_{0})$, and it is straightforward to check $\sigma_{0}=p_{0}|0\rangle\langle 0|\otimes|+\rangle\langle+|$ is a witness of lifting $(M_{0}\mathit{tr}_{\langle 2\rangle}(\rho)M_{0}){A_{00}}^{\#}(M_{0}^{\prime}\mathit{tr}_{\langle 1\rangle}(\rho)M_{0}^{\prime})$, which leads to ${\mathrm{tr}}(A_{00}\sigma_{0})=p_{0}$. Similar arguments hold for $m=1$, with $p_{1}={\mathrm{tr}}(M_{1}\mathit{tr}_{\langle 2\rangle}(\rho)M_{1})$, witness $\sigma_{1}=p_{1}|1\rangle\langle 1|\otimes|-\rangle\langle-|$ and ${\mathrm{tr}}(A_{11}\sigma_{1})=p_{1}$. Observe that ${\mathrm{tr}}(I\otimes I\rho)={\mathrm{tr}}(\rho)$ and ${\mathrm{tr}}(\rho)=p_{0}+p_{1}$. Thus, we conclude that ${\mathrm{tr}}(I\otimes I\rho)={\mathrm{tr}}(A_{00}\sigma_{0})+{\mathrm{tr}}(A_{11}\sigma_{1})$.

A one-side variant of the above definition will also be useful.

Definition 5.5.

Let ${\mathcal{M}}_{1}=\{M_{1m}\}$, $A$ and $B_{m}$ be as in Definition 5.4. We define

[TABLE]

where $I_{2}$ stands for the identity operator in $\mathcal{H}_{P_{2}}$, if for any $\rho\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}\right)$, and for each $m$, there exist $\rho_{2m}\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{2}\langle 2\rangle}\right)$ and a coupling $\sigma_{m}$ for $\left\langle M_{1m}\mathit{tr}_{\langle 2\rangle}(\rho)M_{1m}^{\dagger},\rho_{2m}\right\rangle$ such that $\sum_{m}\rho_{2m}=\mathit{tr}_{\langle 1\rangle}(\rho)$ and

[TABLE]

Similarly, we can define $I_{1}\approx{\mathcal{M}}_{2}\models A\Rightarrow\{B_{m}\}$, where $I_{1}$ is the identity operator in $\mathcal{H}_{P_{1}}$.

Now we are ready to present our new rules for case statements and loops in Fig. 6. As pointed out in the Introduction, synchronous rules in non-probabilistic relational Hoare logic RHL and probabilistic logic pRHL for control-flow constructs (conditionals and loops) require that the two programs under comparison execute in lockstep. The control flows of quantum programs studied in this paper are determined by the outcome of measurements. Thus, measurement conditions ${\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}$ and $({\mathcal{M}}_{1},P_{1})\approx({\mathcal{M}}_{2},P_{2})$ in our rules (IF1) and (LP1) and their one-side variants are introduced to warrant that the two programs execute in lockstep; more precisely, they enter the same branch in their control flows with equal probabilities.

Using rule (IF1), we are able to derive ${\mathcal{M}}\approx{\mathcal{M}}^{\prime}\vdash Q_{1}\sim Q_{2}:I\otimes I\Rightarrow B$ for our working example, shown in Fig. 2. Also in Example 6.1, correctness of Quantum Bernoulli Factory is verified using (LP1) while (LP) is too weak to derive the desired judgment.

Comparison between Rules (IF), (LP) and (IF1), (LP1): A careful comparison between the rules without and with measurement conditions is helpful for us to determine where the rules with measurement conditions are needed.

1. (1)

First, we notice that the appearance of the special case (IF-w) of (IF) is similar to (IF1). Indeed, whenever the measurement conditions are true and each branch is terminating, then (IF1) degenerates to (IF-w) provided we set: $A=\sum_{m}\left(M_{1m}^{{\dagger}}\otimes M_{2m}^{\dagger}\right)B_{m}\left(M_{1m}\otimes M_{2m}\right).$ However, this choice of $A$ is much weaker than the best possible choice. To see this, suppose $\rho$ is a coupling of inputs that satisfy the premises, and let $\rho_{1m}=M_{1m}{\mathrm{tr}}_{2}(\rho)M_{1m}^{\dagger}$ and $\rho_{2m}=M_{2m}{\mathrm{tr}}_{1}(\rho)M_{2m}^{\dagger}$ for all $m$. Actually, (IF-w) uses $\sum_{m}\rho_{1m}\otimes\rho_{2m}$ as part of the coupling of the output states to derive the precondition. However, this state represents only $1/d$ of the output in general, where $d$ is the dimension of the quantum register being measured. More precisely, the set $\left\{\left(M_{1m}\otimes M_{2m}\right)\right\}_{m}$ is a part of quantum measurement $\mathcal{M}_{1}\otimes\mathcal{M}_{2}=\left\{\left(M_{1m}\otimes M_{2n}\right)\right\}_{m,n}$ and only contains about $1/d$ measurement operators of $\mathcal{M}_{1}\otimes\mathcal{M}_{2}$. Consequently, the trace of the coupling state (probability of occurrence) is smaller than possible, which leads to a weaker precondition. 2. (2)

The above defect was remedied in the general rule (IF) by allowing all possible combinations $(m,n)$ rather than only diagonal $(m,m)$. But there is another issue that sometimes prevents (IF) to derive relational properties as strong as those by (IF1). As can be seen in its soundness proof, (IF) simply relates two programs in a manner of tensor product, which does not captures the possible correlation between these programs. Recall that in probabilistic logic pRHL, coupling was introduced to warrant that two programs be executed in a lockstep manner so that sharing randomness can be achieved. The rule (IF1) is proposed for the same purpose and can be used to reason about stronger relational properties of quantum programs, as shown in Example 1.1 as well as Example 6.1. On the other hand, whenever a strong correlation between two programs does not exist or is unnecessary for our purpose (see for instance, Example 6.5 - quantum one-time pad), we prefer to use (IF) because it is simpler. 3. (3)

The same argument applies to the rules (LP) and (LP1) for loops.

5.4. Separability Conditions

We now turn to the structural rules for our logic rqPD. The rules (Conseq), (Weaken) and (Case) of probabilistic relation Hoare logic (pRHL) can be straightforwardly generalised to the quantum setting and are shown in Fig. 7. In (Conseq), we use the Löwner order between quantum predicates (Hermitian operators) in place of boolean implication. The meanings of rules (Weaken) and (Case) are obvious.

However, the (Frame) rule requires special care.

A typical difficulty in reasoning about a quantum system is entanglement between its subsystems. The notions of bipartite separability and entanglement considered in Subsection 3.3 can be generalised to the case of more than two subsystems. A partial density operator $\rho$ in $\bigotimes_{i=1}^{n}\mathcal{H}_{i}$ is separable between $\mathcal{H}_{i}$ $(i=1,...,n)$ if there exist partial density operators $\rho_{mi}\in\mathcal{D}^{\leq}(\mathcal{H}_{i})$ such that $\rho=\sum_{m}\left(\bigotimes_{i=1}^{n}\rho_{mi}\right)$. The following separability condition can be introduced to specify that certain entanglement is not provided (as a resource) or not allowed (e.g. between an adversary and a storage containing sensitive information).

Definition 5.6.

Let $P_{1},P_{2}$ be two programs and $\Sigma=[X_{1},...,X_{n}]$ a partition of $\mathit{var}(P_{1}\langle 1\rangle)\cup\mathit{var}(P_{2}\langle 2\rangle)$. Then we say that a state $\rho\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}\right)$ satisfies separability condition $\Sigma$, written $\rho\models\Sigma$, if $\rho$ is separable between $\mathcal{H}_{X_{i}}$ $(i=1,...,n)$.

With the above definition, we can define the (Frame) rule for quantum programs in Fig. 7 where a separability condition between the programs $P_{1},P_{2}$ and the new predicate $C$. Recall that in probabilistic logic pRHL, the frame rule allows an assertion $C$ to be carried from the precondition through to the postcondition. The validity of the frame rule is based on the assumption that the two programs $P_{1}$ and $P_{2}$ cannot modify the (free) variables in $C$; or mathematically speaking, $\mathit{var}(P_{1},P_{2})\cap\mathit{var}(C)=\emptyset$. In the quantum setting, however, the syntactic disjointness between $\mathit{var}(P_{1},P_{2})$ and $\mathit{var}(C)$ is not enough. Indeed, an entanglement can occur between them even if they are disjoint, and some properties of the subsystem denoted by the variables in $C$ can be changed by certain actions, say measurements of $P_{1}$ or $P_{2}$. So, the separability condition $\Gamma=[V,\mathit{var}(P_{1},P_{2})]$ is introduced in the conclusion part of the frame rule to exclude such an entanglement between $P_{1},P_{2}$ and $C$, where $V$ is the set of quantum variables appearing in $C$.

5.5. Entailment between Side-Conditions

In the above two subsections, measurement and separability conditions are introduced into our logic rqPD. But the (SC) rule for sequential composition in Fig. 3 does not contain these conditions. So, it must be accordingly strengthened to accommodate the propagation of measurement and separability conditions. To this end, we need the following:

Definition 5.7.

Let $\Gamma,\Delta$ be two sets of measurement or separability conditions, and $P_{1},P_{2}$ two programs. We say that $\Delta$ is couple-entailed by $\Gamma$ through $(P_{1},P_{2})$, written

[TABLE]

if for any $\rho\models\Gamma$, whenever $\sigma$ is a coupling for $\left\langle\llbracket P_{1}\rrbracket\left(\mathit{tr}_{\langle 2\rangle}(\rho)\right),\llbracket P_{2}\rrbracket\left(\mathit{tr}_{\langle 1\rangle}(\rho)\right)\right\rangle$, then $\sigma\models\Delta$.

Using the above definition, a strengthened version of (SC) is presented as rule (SC+) in Fig. 8.

Let us go back to the working example 1.1. After a direct calculation, we are able to show

[TABLE]

Now, using rule (SC+) we can combine all the segment judgments shown in last few sections together to reason about judgment (6), as shown in Fig. 2.

In general, it is not easy to use this rule because it is hard to check a side condition of the form (10). However, in most of the applications, we do not need the full power of (SC+) because most of conditionals and loops can be dealt with by using (IF) and (LP) where no measurement conditions are introduced and thus $\Gamma=\Delta=\emptyset$, and (IF1) and (LP1) are only employed for a few times. In particular, if we only need (IF1) or (LP1) to reason about a single conditional or loop, then $\Delta=\emptyset$ and side condition (10) is trivially valid; for instance, Example 6.1 is actually this case. The difficulty of applying (SC+) will arise only when (IF1) and (LP1) are needed to reason about many conditionals and loops. In the case of finite-dimensional state Hilbert spaces, for a large class of quantum programs, this difficulty can be significantly eased by a back-tracking strategy for collecting a set of measurement or separability conditions at the beginning of a sequence of consecutive judgments in order to warrant that all side-conditions of the form (10) are valid. An elaboration of this strategy is given in (Barthe et al., 2019).

5.6. Auxiliary Rules for General Quantum Operations

Our programming language only contains two simple kinds of quantum operations: unitary transformations and quantum measurements. Also, the post-measurement states are recorded in the semantics so that the dimension of the state Hilbert space is fixed. In applications, however, it is often convenient to apply general quantum operations; for example, quantum noises and communication channels. Principally, a general quantum operation can be implemented by unitary transformations and measurements through introducing ancilla systems and discarding post-measurement states (see (Nielsen and Chuang, 2002), Section 8.2.2 for the system-environment model). But the implementations are usually quite complicated. So, for convenience, we choose to expand the programming language by explicitly adding program constructs of the form:

[TABLE]

where $\mathcal{E}$ is a general quantum operation. Mathematically, $\mathcal{E}$ is modelled as trace-preserving super-operator with Hilbert space $\mathcal{H}_{\overline{q}}$ as its domain, but its codomain can be a different Hilbert space, even with a different dimension, e.g. $\mathcal{H}_{\overline{q}\setminus\overline{q^{\prime}}}$ or $\mathcal{H}_{\overline{q}\cup\overline{q^{\prime}}}$. It is well-known that a super-operator $\mathcal{E}$ can be represented by a set of operators $\{E_{i}\}$ (Kraus operator-sum representation): $\mathcal{E}(\rho)=\sum_{i}E_{i}\rho E_{i}^{\dagger}$ for every state $\rho$ in $\mathcal{H}_{\overline{q}}$.

The operational semantics of program $\overline{q}:=\mathcal{E}[\overline{q}]$ is defined by the following transition rule:

[TABLE]

Based on this, the denotational semantics of quantum programs containing super-operators can be defined in the same way as Definition 4.3, provided allowing that the domain and codomain of the semantic function of a quantum program can be different.

We present three inference rules for general quantum operations in Fig. 9, generalising rules (UT), (UT-L) and (UT-R), respectively.

Remark 5.2.

It is worth mentioning that allowing different dimensions of the domain and codomain of $\mathcal{E}$ in (11) has a benefit; that is, it enables us to introduce auxiliary quantum variables or discard a quantum variable. The construct of introducing auxiliary variables can be defined as cylinder extension, i.e. tensor product with the identity operator of the state Hilbert space of the auxiliary variables (divided by its dimension for normalisation), and the construct of discarding a quantum variable $q\in\overline{q}$ is indeed included in Selinger’s quantum programming language QPL (Selinger, 2004b). It can be defined as a partial trace $\mathbf{Tr}[q]$, with its semantics described as a special super-operator: $\mathcal{E}(\rho)=\sum_{i}\langle i|\rho|i\rangle\in\mathcal{D}(\mathcal{H}_{\overline{q}\setminus\{q\}})$ for any $\rho\in\mathcal{D}(\mathcal{H}_{\overline{q}})$, where $\{|i\rangle\}$ is an orthonormal basis of $\mathcal{H}_{q}$. Then rules (SO) and its one-side variants (SO-L), (SO-R) warrant that introducing auxiliary variables and discarding a variable can be safely done in relational reasoning.

5.7. Soundness Theorem

We can prove that our proof system is sound with respect to validity of judgments. The proof of soundness is given in the complete version of this paper (Barthe et al., 2019).

Theorem 5.1 (Soundness).

Derivable judgments are valid:

[TABLE]

Completeness of relational logics is a challenging problem. In the deterministic setting, relational Hoare logic can be shown to be relatively complete for terminating programs provided it includes sufficiently many one-sided rules. Relative completeness fails for probabilistic relational Hoare logic; a further potential complication is that the coupling method — upon which probabilistic relational Hoare logic builds — is itself not complete for proving convergence Markov chains (Anil Kumar and Ramesh, 2001).

6. Examples

In this section, we give several examples to illustrate the power of rqPD. We mainly show how their relational properties can be formally specified as rqPD judgments. Due to the limited space, only a proof outline of the first example is given, and the formal derivations of other judgments are deferred to (Barthe et al., 2019).

6.1. Symmetry between Simple Programs

Let us start from our working example 1.1. In last section, we already proved judgment (6) in our logic rqPD. A symmetry between programs $P_{1}$ and $P_{2}$ modelled by judgment (6) is more interesting than their similarity we can observe at the first glance. It worth noting that two different kinds of “quantum equality” are used in the precondition and postcondition. To understand this judgment better, let recall Proposition 3.2, which give us an intuition of what $=_{\mathcal{B}}$ and $=_{\mathit{sym}}$ mean. The judgment tell us that, if the inputs of $P_{1}$ and $P_{2}$ are the same, then the outputs are also same, or in other words, program $P_{1}$ and $P_{2}$ are actually equal.

Remark 6.1.

As discussed before, rule (IF1) is necessary to derive judgment (6) while using rule (IF-w) or more general (IF) is impossible to prove it. A strong correlation between two programs can be detected only if we run them in a lockstep manner. This is why rule (IF1) works. However, (IF) only requires that two programs run simultaneously while lockstep is not guaranteed. Therefore, it is not surprising to see (IF) fails here.

6.2. Uniformity

An elegant characterisation of uniform probability distribution with coupling was given in (Barthe et al., 2017). Unfortunately, the characterisation does not directly carry over to the quantum setting. In this subsection, we show how an alternative approach based on quantum coupling can be used to describe uniformity in quantum systems. Let $\mathcal{H}$ be a Hilbert space and $\mathcal{B}=\{|i\rangle\}$ be an orthonormal basis of $\mathcal{H}$. For each $i$, we write $M_{i}=|i\rangle\langle i|$. Then the measurement in basis $\mathcal{B}$ is defined as ${\mathcal{M}}_{\mathcal{B}}=\{M_{i}\}$.

Definition 6.1.

A density operator $\rho$ in $\mathcal{H}$ with $d=\dim\mathcal{H}$ is called uniform in basis $\mathcal{B}$ if the outcome of measurement ${\mathcal{M}}_{\mathcal{B}}$ on $\rho$ is uniformly distributed; i.e. for every $i$,

[TABLE]

The following proposition gives a characterization of uniformity of a program’s outputs in terms of quantum coupling.

Proposition 6.1 (Uniformity by coupling).

Let $P$ be a quantum program, $\mathcal{B}=\{|i\rangle\}$ be an orthonormal basis of $\mathcal{H}_{P}$ and $d=\dim\mathcal{H}_{P}$. Then the following three statements are equivalent:

1. (1)

for any input density operator $\rho$ in $\mathcal{H}_{P}$, output $\llbracket P\rrbracket(\rho)$ is uniform in basis $\mathcal{B}$; 2. (2)

for any basis state $|i\rangle$ in $\mathcal{B}$,

[TABLE]

where $I$ is the identity operator in $\mathcal{H}_{P}$; 3. (3)

for any basis state $|i\rangle$ in $\mathcal{B}$,

[TABLE]

where $\mathcal{C}=\{|j\rangle\}$ is an arbitrary orthonormal basis of $\mathcal{H}_{P}$, and the equality operator $\mathit{=}^{e}_{\mathcal{C}}$ is defined to be $|\Phi\rangle\langle\Phi|$, where $\Phi$ is the maximally entangled state $|\Phi\rangle=\frac{1}{\sqrt{d}}\sum_{j}|jj\rangle.$ More precisely, $\mathit{=}^{e}_{\mathcal{C}}$ is (the projection onto) the one-dimensional subspace spanned by the maximally entangle state $|\Phi\rangle$. It is interesting to see that in judgment (13), a separability condition is enforced on inputs, but entanglement appears in the precondition $\mathit{=}^{e}_{\mathcal{C}}$. This suggests that entanglement cannot be avoid in such a characterisation of uniformity.

Now, we consider uniformity for a concrete quantum protocol. The Bernoulli factory (BF) (Keane and O’Brien, 1994) is a protocol for random number generation. It uses a coin with an unknown probability $p$ of heads to simulate a new coin that has probability $f(p)$ of heads for a given function $f:[0,1]\to[0,1]$. The Quantum Bernoulli factory (QBF) (Dale et al., 2015) also generates classical randomness (e.g., a biased coin with probability $f(p)$), but it uses quantum coins instead of classical coins. Interestingly, QBF can simulate a strictly larger class of functions $f$ than those simulated by BF. As a direct application of the above proposition, we can verify a simplified version of quantum Bernoulli factory in our logic.

Example 6.1 (Simplified Quantum Bernoulli Factory).

Suppose we have a two-qubit system with state Hilbert space $\mathcal{H}_{q_{x}}\otimes\mathcal{H}_{q_{y}}$ and an initial state $|0\rangle_{q_{x}}|0\rangle_{q_{y}}$. We are allowed to perform projective measurement ${\mathcal{M}}=\{M_{0},M_{1}\}$:

[TABLE]

and apply a given—but unknown—one-qubit unitary transformation $U$ such that $0<|\langle 0|U|0\rangle|<1$ on system $x$ or $y$.222In the classical BF, this condition means that the coin must be non-trivial—it cannot always return [math] or always return $1$. How can we produce the uniform state $\frac{1}{2}I_{q_{x}}$? The following quantum program accomplishes this task:

[TABLE]

where ${\bf Tr}$ stands for the partial trace over system $q_{y}$.

Note that state $\frac{1}{2}I_{q_{x}}$ is the only density operators being uniform in any orthonormal basis $\mathcal{B}$. With Proposition 6.1, QBF can be verified by proving that for any $|\psi\rangle\in\mathcal{H}_{q_{x}}$:

[TABLE]

Since this judgment is valid for all $|\psi\rangle$, the output is uniform in all basis so the output state must be $\frac{1}{2}I_{q_{x}}$.

It is worth pointing out that rule (LP1) plays an essential role in the proof. All registers are initialised before the loop and therefore, we are able to run two of the same QBF in a lockstep manner. Thus, rule (LP) is too weak to derive judgment (14). Rule (SO) is also needed in the verification of (14) because $\mathbf{Tr}[q_{y}]$ appears at the end of QBF. Indeed, if we do not trace out system $q_{y}$ at the end, then QBF outputs the Bell state $\frac{1}{\sqrt{2}}(|0\rangle_{q_{x}}|1\rangle_{q_{y}}+|1\rangle_{q_{x}}|0\rangle_{q_{y}}).$ This fact can also be realized in our logic. Moreover, it implies that our program QBF is not a trivial generalisation of classical Bernoulli factory because it is capable of producing the maximally entangled state.

6.3. Quantum Teleportation

Now we consider a more sophisticated example. Quantum teleportation (Bennett et al., 1993) is arguably the most famous quantum communication protocol. With it, quantum information (e.g. the exact state of an atom or a photon) can be transmitted from one location to another, only through classical communication, but with the help of previously shared entanglement between the sender and the receiver. The correctness of quantum teleportation has been formally verified by several different methods in the literature, e.g. using categorical formalism of quantum mechanics (Abramsky and Coecke, 2004). Our logic provides a new way for verifying the correctness of quantum teleportation; more importantly, it can be used to verify the reliability of quantum teleportation against various kinds of quantum noise. To the best of our knowledge, this is the first formal verification of its reliability.

Example 6.2.

Suppose that Alice possesses two qubits $p,q$ and Bob possesses qubit $r$, and there is entanglement, i.e. the EPR (Einstein-Podolsky-Rosen) pair: $|\beta_{00}\rangle=\frac{1}{\sqrt{2}}(|00\rangle+|11\rangle)$ between $q$ and $r$. Then Alice can send an arbitrary qubit state $|\psi\rangle=\alpha|0\rangle+\beta|1\rangle$ to Bob, i.e. from $p$ to $r$, by two-bit classical communication (for detailed description, see (Nielsen and Chuang, 2002), Section 1.3.7). If we regard $p$ as the input state and $r$ the output state, then this protocol can be modeled by a quantum program:

[TABLE]

where $H$ is the Hadamard gate, $X$ and $Z$ are the Pauli gates, ${\rm CNOT}$ is the controlled-NOT:

[TABLE]

$I,0$* are the $2\times 2$ unit and zero matrices, respectively, and ${\mathcal{M}}$ is the measurement in the computational basis, i.e. ${\mathcal{M}}=\{M_{0},M_{1}\}$, where $M_{0}=|0\rangle\langle 0|$, $M_{1}=|1\rangle\langle 1|$.*

6.3.1. Correctness of Quantum Teleportation

In this subsection, we show how our logic can be used to verify the correctness of quantum teleportation. The correctness of QTEL can be described as the judgment:

[TABLE]

where $\mathcal{B}=\{|\psi\rangle,|\phi\rangle\}$ is an arbitrary othornormal basis of the state Hilbert space of a qubit, and $(=_{\mathcal{B}})=|\psi\rangle|\psi\rangle\langle\psi|\langle\psi|+|\phi\rangle|\phi\rangle\langle\phi|\langle\phi|$ is the projector onto the subspace ${\rm span}\{|\psi\rangle|\psi\rangle,|\phi\rangle|\phi\rangle\}$ [see Example 3.4 (2)]. Indeed, for any input states $\rho$, there always exists an orthonormal basis $\mathcal{B}$ such that $\rho(=_{\mathcal{B}})^{\#}\rho$, and we assume that a witness for this lifting is $\sigma$. From judgment (15), we know that there exists a coupling $\sigma^{\prime}$ for $\left\langle\llbracket{\rm QTEL}\rrbracket(\rho),\llbracket{\bf skip}\rrbracket(\rho)\right\rangle$ such that $\mathit{tr}(=_{\mathcal{B}}\sigma^{\prime})\geq\mathit{tr}(=_{\mathcal{B}}\sigma)=1.$ So, $\sigma^{\prime}$ is a witness of lifting: $\llbracket{\rm QTEL}\rrbracket(\rho)(=_{\mathcal{B}})^{\#}\llbracket{\bf skip}\rrbracket(\rho),$ which, together with Proposition 3.2, implies $\llbracket{\rm QTEL}\rrbracket(\rho)=\llbracket{\bf skip}\rrbracket(\rho)=\rho.$

Interestingly, the correctness of QTEL can also be described as the following judgment:

[TABLE]

using a different equality $=_{\mathit{sym}}$, that is, the projector onto the symmetric subspace [see Example 3.4 (3)]. A similar argument shows that for any input $\rho$, we have $\llbracket{\rm QTEL}\rrbracket(\rho)=\llbracket{\bf skip}\rrbracket(\rho)=\rho$.

The proof of these two judgments are somewhat easy. Unlike the previous two examples, the basic construct-specific rule (IF-L) is enough to derive the results.

6.3.2. Reliability of Quantum Teleportation

In this subsection, we further show that our logic can be used to deduce not only correctness but also reliability of quantum teleportation when its actual implementation suffers certain physical noise.

Quantum noise are usually modelled by super-operators, a more general class of quantum operations than unitary transformations.

Example 6.3 (Noise of Qubits, (Nielsen and

Chuang, 2002), Section 8.3).

2. (1)

The bit flip noise flips the state of a qubit from $|0\rangle$ to $|1\rangle$ and vice versa with probability $1-p$, and can be modelled by super-operator:

[TABLE]

for all $\rho$, where

[TABLE] 3. (2)

The phase flip noise can be modelled by the super-operator $\mathcal{E}_{\it PF}$ with

[TABLE] 4. (3)

The bit-phase flip noise is modelled by the super-operator $\mathcal{E}_{\it BPF}$ with

[TABLE]

where $X,Y,Z$ are Pauli matrices.

We sometimes write the bit flip super-operators as $\mathcal{E}_{\it BF}(p)$ in order to explicitly specify the flip probability $p$. The same convention is applied to the phase flip $\mathcal{E}_{\it PF}$ and bit-phase flip $\mathcal{E}_{\it BPF}$.

Example 6.4.

If the bit flip noise occurs after the Hadamard gates on both qubit $p$ and $q$, then the teleportation programs becomes:

[TABLE]

where $\mathcal{E}_{\rm BF}$ is the bit flip super-operator. Moreover, we write ${\rm QTEL}_{\mathit{PF}}$ and ${\rm QTEL}_{\mathit{BPF}}$ for the phase flip and bit-phase flip occurring at the same positions.

Now the reliability of QTEL with the different noises—bit flip, phase flip and bit-phase flip—is modelled by the judgments:

[TABLE]

To understand these judgments better, let us choose pure state $|\psi\rangle$ as the input of both QTELBF and QTEL as an example. The correctness of QTEL has been verified and therefore, $\llbracket{\rm QTEL}\rrbracket(|\psi\rangle\langle\psi|)=|\psi\rangle\langle\psi|.$ We assume that $\llbracket{\rm QTEL}_{\mathit{BF}}\rrbracket(|\psi\rangle\langle\psi|)=\rho$. There exists a unique coupling $\rho\otimes|\psi\rangle\langle\psi|$ for the outputs $\langle\rho,|\psi\rangle\langle\psi|\rangle$, and according to the judgment (18), we know that:

[TABLE]

that is, $\langle\psi|\rho|\psi\rangle\geq p+(1-p)|\langle\psi|Z|\psi\rangle|^{2}.$ Whenever $p$ is close to 1, then $\rho$ is also close to $|\psi\rangle\langle\psi|$, and this is what reliability actually means.

Judgemens (18), (19) and (20) can be verified in our logic rqPD using rule (SO-L) for general quantum operations and rule (IF) for all pairwise comparisons.

6.4. Quantum One-Time Pad

In this subsection, we show that our logic can be used to specify and verify correctness and security of a basic quantum encryption scheme, namely the quantum one-time pad (QOTP) (Mosca et al., 2000; Boykin and Roychowdhury, 2003). Similar to the classical one-time pad, it uses a one-time pre-shared secret key to encrypt and decrypt the quantum data, providing the information-theoretic security. We first consider the simplest case, for protecting one-qubit data.

Example 6.5.

The QOTP scheme includes three parts: key generation $\mathbf{KeyGen}$, encryption $\mathbf{Enc}$ and decryption $\mathbf{Dec}$, which can be written as programs:

[TABLE]

Here, registers $a$ and $b$ are used as the secret key, and measurement

[TABLE]

is introduced to detect the value of secret key, which has two-bit classical outcome. Register $p$ is the input quantum data which we want to protect. $H$ is the Hadamard gate and $X,Z$ are Pauli gates as usual. As the secret key is not considered when analysing the correctness and security of the protocol, we further introduce $\mathbf{DisKey}$ to discard the key.

6.4.1. Correctness of Quantum One-Time Pad

The correctness of QOTP can be formulated as the following judgment:

[TABLE]

where $=_{sym}$ represents the projector onto the symmetric space. By an argument similar to that for the correctness of quantum teleportation in Section 6.3.1, we can show that if judgment (21) is valid, then for any possible input $\rho$ of register $p$,

[TABLE]

that is, the input state is the same as the output after QOTP.

Judgment (21) can be verified mainly with rule (IF-L). But note that the initialisations of registers $a$ and $b$ are regarded as the creation of new local qubits. So, rules (SO-L) and (SO-R) are needed here instead of (Init-L).

6.4.2. Security of Quantum One-Time Pad

Using the characterisation of uniformity given in Section 6.2, we may verify the security of QOTP by proving that for any $|\psi\rangle\in\mathcal{H}_{p}$:

[TABLE]

In fact, if judgment (22) is valid for all $|\psi\rangle$, then the output is uniform in all bases; that is, the output of register $p$ is $\frac{1}{2}I_{p}$, which is actually the maximally mixed state and nothing can be inferred from it. To derive this judgment, we need rule (SO) and (IF-w).

6.4.3. General Quantum One-Time Pad

Now let us generalise Example 6.5 to the general case for protecting $n$-qubit data. In this case, QOTP can be written as the following quantum program:

[TABLE]

Again, if we regard register $\bar{p}=p_{1},\cdots,p_{n}$ as the input and output of QOTP and consider the trivial program $\bf skip$ with the duplicated register $\bar{p}^{\prime}=p_{1}^{\prime},\cdots,p_{n}^{\prime}$, then the judgment

[TABLE]

is derivable using the basic rules of logic rqPD, where $=_{sym}$ is the projector onto the symmetric space between $\bar{p}$ and $\bar{p}^{\prime}$. Indeed, this judgment implies the correctness of QOTP; that is, the input and output quantum data on register $\bar{p}=p_{1},\cdots,p_{n}$ (might be entangled) are conserved. Similarly, we can also prove that for any $|\psi\rangle\in\mathcal{H}_{\bar{p}}$:

[TABLE]

The above judgment actually implies the output after the encryption is the maximally mixed state and it is impossible for the eavesdropper to obtain any information about the quantum data.

7. Reasoning about Projective Predicates

The logic rqPD was developed for reasoning about the equivalence between quantum programs with respect to general preconditions and postconditions represented by Hermitian operators. But in some applications, it is more convenient to use a simplified version of rqPD with preconditions and postconditions being projective predicates (equivalently, subspaces of the state Hilbert spaces). In this section, we present such a simplified version of rqPD and give an example to show its utility. As one may expect, a price for this simplification is a weaker expressive power of the logic. The coefficients $\frac{1}{d}$ and $\frac{1}{2}$ in the preconditions of judgments (12) and (14) are not expressible in rqPD with projective predicates, indicating that the expressive power of rqPD with projective predicates is strictly weaker than that of full rqPD.

7.1. Inference Rules

In this subsection, we develop inference rules for judgments with projective preconditions and postconditions. We consider judgments of the form:

[TABLE]

where $A,B$ are two projections in (or equivalently, subspaces of) $\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}$.

Definition 7.1.

Judgment (25) is projectively valid, written:

[TABLE]

if for any $\rho_{1}\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{1}\langle 1\rangle}\right)$ and $\rho_{2}\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{2}\langle 2\rangle}\right)$ such that $\rho_{1}\mathrel{A^{\#}}\rho_{2}$, there exists a lifting of $B$ relating the output quantum states: $\llbracket P_{1}\rrbracket(\rho_{1})\mathrel{B^{\#}}\llbracket P_{2}\rrbracket(\rho_{2}).$

The following proposition clarifies the relationship between projective validity and the notion of validity introduced in Definition 5.1.

Proposition 7.1.

For any two program $P_{1}$ and $P_{2}$, and projective predicates $A$ and $B$:

[TABLE]

To present rules for proving projectively valid judgments, we need the following modifications of Definitions 5.4 and 5.5.

Definition 7.2.

Let ${\mathcal{M}}_{1}=\{M_{1m}\}$ and ${\mathcal{M}}_{2}=\{M_{2m}\}$ be two measurements with the same set $\{m\}$ of possible outcomes in $\mathcal{H}_{P_{1}}$ and $\mathcal{H}_{P_{2}}$, and let $A$ and $B_{m}$ be projective predicates in $\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}.$ Then the assertion

[TABLE]

holds if for any $\rho_{1}\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{1}\langle 1\rangle}\right)$ and $\rho_{2}\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{2}\langle 2\rangle}\right)$ such that $\rho_{1}\mathrel{A^{\#}}\rho_{2}$, there exists a sequence of lifting of $B_{m}$ relating the post-measurement states with the same outcomes: for all $m$,

[TABLE]

Definition 7.3.

Let ${\mathcal{M}}_{1}=\{M_{1m}\}$ be a measurements in $\mathcal{H}_{P_{1}}$, and let $A$ and $B_{m}$ be projective predicates in $\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}.$ Then the assertion

[TABLE]

holds if for any $\rho_{1}\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{1}\langle 1\rangle}\right)$ and $\rho_{2}\in\mathcal{D}^{\leq}\left(\mathcal{H}_{P_{2}\langle 2\rangle}\right)$ such that $\rho_{1}\mathrel{A^{\#}}\rho_{2}$, there exist $\rho_{2m}$ such that $\sum_{m}\rho_{2m}=\rho_{2}$ and for all $m$,

[TABLE]

Now the proof system for judgments with projective preconditions and postconditions consists of rules (Skip), (UT), (SC), (UT-L/R), (Conseq), (Equiv) and (Frame) in Figs. 3, 4 and 7 with $\vdash$, $\models$ being replaced by $\vdash_{P}$ and $\models_{P}$, respectively, together with the rules given in Fig. 10.

Let us carefully compare this simplified proof system for projective predicates with the original rqPD for general predicates of Hermitian operators:

• •

In rules (Init-P), (Init-P-L), (Init-P-R), (SO-P), (SO-P-L) and (SO-P-R), we have to use the operation ${\rm proj}(\cdot)$ because the operators in its operand there are not necessarily projective.

• •

Rule (Case) has no counterpart for projective predicates because probabilistic combination $\sum_{i}p_{i}A_{i}$ of a family of projective predicates $A_{i}$ is usually not projective.

• •

The main simplification occurs in the rules for control-flow constructs (i.e. conditionals and loops). We only consider rule (IF-P); the same explanation applies to other control-flow rules. First, the measurement condition $\models_{P}{\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}:A\Rightarrow\{B_{m}\}$ in the premise of (IF-P) is weaker than the measurement condition ${\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}\models A\Rightarrow\{B_{m}\}$ in the premise of (IF). Second, the measurement condition ${\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}$ is the conclusion of (IF) is removed in (IF-P). As already pointed out in the Introduction, this is biggest reward of the projective simplification of our logic.

Proposition 7.2.

The proof system for judgments with projective preconditions and postconditions are sound.

As will be seen in the next subsection, this simplified proof system, in particular, the simplified rules for control-flow constructs, whenever they are applicable, can significantly ease the verification of relational properties of quantum programs. On the other hand, some relational properties of quantum programs, e.g. judgments (12), (14) and (18-20), can be verified by the original rqPD but not by this simplified system. Even for the same quantum programs, the original rqPD usually can prove stronger relational properties in the case where the weakest preconditions or strongest postconditions are not projective.

7.2. Example: Quantum Walks

In this subsection, we present an example to show the effectiveness of the inference rules given in the previous subsection. Quantum (random) walks (Kempe, 2003; Venegas-Andraca, 2012) are quantum analogues of random walks, and have been widely used in the design of quantum algorithms, including quantum search and quantum simulation. There are two key ideas in defining a quantum walk that are fundamentally different from that of a classical random walk: (1) a “quantum coin” is introduced to govern the movement of the walker, which allows the walker to move to two different directions, say left and right, simultaneously; (2) an absorbing boundary is realised by a quantum measurement. Here, we show how our logic can be applied to verify a certain equivalence of two one-dimensional quantum walks with absorbing boundaries: the quantum coins used in these two quantum walks are different, but they terminate at the same position.

Example 7.1.

Let $\mathcal{H}_{c}$ be the coin space, the $2$-dimensional Hilbert space with orthonormal basis state $|L\rangle$ (or $|0\rangle_{c}$) and $|R\rangle$ (or $|1\rangle_{c}$), indicating directions Left and Right, respectively. Let $\mathcal{H}_{p}$ be the $(n+1)$-dimensional Hilbert space with orthonormal basis states $|0\rangle,|1\rangle,...,|n-1\rangle,|n\rangle$, where vector $|i\rangle$ denotes position $i$ for each $0\leq i\leq n$; in particular, positions [math] and $n$ are the absorbing boundaries. The state space of the walk is then $\mathcal{H}=\mathcal{H}_{c}\otimes\mathcal{H}_{p}$. Each step of the walk consists of:

1. (1)

Measure the position of the system to see whether it is [math] or $n$. If the outcome is “yes”, then the walk terminates; otherwise, it continues. The measurement can be described as ${\mathcal{M}}=\{M_{\mathit{yes}},M_{\mathit{no}}\}$, where the measurement operators are: $\,M_{\mathit{yes}}=|0\rangle\langle 0|+|n\rangle\langle n|$, $M_{\mathit{no}}=I_{p}-M_{yes}=\sum_{i=1}^{n-1}|i\rangle\langle i|$ , and $I_{p}$ is the identity in position space $\mathcal{H}_{p}$; 2. (2)

Apply a “coin-tossing” operator $C$ is in the coin space $\mathcal{H}_{c}$. 3. (3)

Apply a shift operator $S=\sum_{i=1}^{n-1}|L\rangle\langle L|\otimes|i-1\rangle\langle i|+\sum_{i=1}^{n-1}|R\rangle\langle R|\otimes|i+1\rangle\langle i|$ in the space $\mathcal{H}$. Intuitively, operator $S$ moves the position one step to the left or to the right according to the direction state.

A major difference between a quantum walk and a classical random walk is that a superposition of movement to the left and a movement to the right can happen in the quantum case. The quantum walk can be written as a quantum program with the initial state in $\mathcal{H}_{c}\otimes\mathcal{H}_{p}$ as the input:

[TABLE]

We consider two frequently used “coin-tossing” operators here: the Hadamard operator $H$ and the balanced operator: Y=\frac{1}{\sqrt{2}}\left(\begin{array}[]{cc}1&{\bm{i}}\\ {\bm{i}}&1\end{array}\right). We use $\mathbf{while}(H)$ and $\mathbf{while}(Y)$ to denote program (28) with $C=H$ or $Y$, respectively. What interests us is: with what kind of initial states do the quantum walks with different “coin-tossing” operators $H$ and $Y$ produce the same output position? To this end, we add a measurement to determine the exact position of the walks after their termination, and discard the coin. So, programs $\mathbf{while}(H)$ and $\mathbf{while}(Y)$ are modified to:

[TABLE]

where measurement ${\mathcal{M}}^{\prime}=\{M_{i}^{\prime}\}$ with $M_{i}^{\prime}=|i\rangle\langle i|$ for $i=0,1,\cdots,n$.

Before formulating our result in our logic, let us fix the notations. Whenever comparing programs $QW(H)$ and $QW(Y)$ and using, say $x$, to denote a variable in the former, then we shall use $x^{\prime}$ for the same variable in the latter. For simplicity, we use $|d,i\rangle_{c,p}$ as an abbreviation of $|d\rangle_{c}|i\rangle_{p}$, $I_{c,p}$ is the identity over the whole space $\mathcal{H}_{c}\otimes\mathcal{H}_{p}$, and $S_{c,p;c^{\prime},p^{\prime}}$ is the SWAP operator between two systems $\mathcal{H}_{c}\otimes\mathcal{H}_{p}$ and $\mathcal{H}_{c^{\prime}}\otimes\mathcal{H}_{p^{\prime}}$. Furthermore, we introduce the following unitary operator $U$ and projective predicates $(=_{\mathit{sym}})$ and $(=_{sym}^{p})$:

[TABLE]

In (Barthe et al., 2019), we show how to derive the following judgment in the projective version of rqPD:

[TABLE]

This judgment means that if walks $QW(H)$ and $QW(Y)$ start from states $\rho_{1}$ and $\rho_{2}=U\rho_{1}U^{\dagger}$, respectively, then they terminate at exactly the same position.

8. Related work

The formal verification of quantum programs is an active area of research, and many expressive formalisms have been proposed in the literature (Chadha et al., 2006; D’Hondt and Panangaden, 2006; Feng et al., 2007; Kakutani, 2009; Ying, 2011, 2016). However, previous work largely considers single program executions. Security of quantum one-time pad (our Example 6.5) was verified in (Unruh, 2019a) using a variant of quantum Hoare logic rather than relational logic. Other formalisms explicitly target equivalence of quantum programs (Ardeshir-Larijani et al., 2013; Feng and Ying, 2015; Kubota et al., 2013). However, these works are based on bisimulations and symbolic methods, which have a more limited scope and are less powerful than general relational program logics. Finally, some works develop specialized methods for proving concrete properties of quantum programs; for instance, Hung et al (Hung et al., 2018) reason about quantitative robustness of quantum programs. It would be interesting to cast the latter into our more general framework. This seems possible although may not be straightforward; indeed, in Subsection 6.3.2, we showed that our logic can be used to reason about the reliability of quantum teleportation against several kinds of quantum noise.

Our work is most closely related to the quantum relational Hoare logic recently proposed by Unruh (2019b); Li and Unruh (2019). Both works are inspired by probabilistic relational Hoare logic (Barthe et al., 2009) and share the long-term objective of providing a convenient framework for formal verification of quantum cryptography. However, the two works explore different points in the design space of relational logics for quantum programs. There are several fundamental differences between our logic and Unruh’s one, including expressiveness, entanglement in defining the validity of judgments and inference rules. A careful comparison of them is given in (Barthe et al., 2019).

9. Conclusion

We have introduced a relational program logic for a core quantum programming language; our logic is based on a quantum analogue of probabilistic couplings, and is able to verify several non-trivial examples of relational properties for quantum programs.

There are several promising directions for future work. First, we would like to further develop the theory of quantum couplings, and in particular to define a quantum version of approximate couplings. An extension apRHL of probabilistic relational Hoare logic pRHL was defined in (Barthe et al., 2013) for verification of differential privacy. A surprising connection between quantum differential privacy and gentle measurements recently observed by Aaronson and Rothblum (2019) presents a further possible application of a quantum counterpart of apRHL in quantum physics. Second, we would like to explore variants and applications of our logic to other areas, including the convergence of quantum Markov chains, quantum cryptography, and translation validation of quantum programs; in particular, the correctness of optimising quantum compilers for NISQ (Noisy Intermediate Quantum) devices.

Acknowledgements.

This work is partially supported by the University of Wisconsin, a Facebook TAV award, the Australian Research Council (Grant No: DE180100156 and DP180100691), the National Key R&D Program of China (Grant No: 2018YFA0306701), and the National Natural Science Foundation of China (Grant No: 61832015). We are grateful to the Max Planck Institute for Software Systems for hosting some of the authors.

A10. Probabilistic couplings

In this section, we briefly recall the basics of probabilistic couplings so that the reader will see a close and natural correspondence as well as some essential differences between probabilistic coupling and their quantum counterparts.

Let $\mathcal{A}$ be a countable set. Then a sub-distribution over $\mathcal{A}$ is a mapping $\mu:\mathcal{A}\rightarrow[0,1]$ such that $\sum_{a\in\mathcal{A}}\mu(a)\leq 1$. In paricular, if $\sum_{a\in\mathcal{A}}\mu(a)=1$, then $\mu$ is called a distribution over $\mathcal{A}$. We can define:

1. (1)

the weight of $\mu$ is

[TABLE] 2. (2)

the support of $\mu$ is ${\rm supp}(\mu)=\{a\in\mathcal{A}:\mu(a)>0\};$ 3. (3)

the probability of an event $S\subseteq\mathcal{A}$ is

[TABLE]

If $\mu$ be a join sub-distribution, i.e. a sub-distribution over Cartesian product $\mathcal{A}_{1}\times\mathcal{A}_{2}$, then its marginals over $\mathcal{A}_{1}$ is defined by

[TABLE]

Similarly, we can define its marginals $\pi_{2}(\mu)$ over $\mathcal{A}_{2}$.

Definition A10.1 (Coupling).

Let $\mu_{1},\mu_{2}$ be sub-distributions over $\mathcal{A}_{1},\mathcal{A}_{2}$, respectively. Then a sub-distribution over $\mathcal{A}_{1}\times\mathcal{A}_{2}$ is called a coupling for $\left\langle\mu_{1},\mu_{2}\right\rangle$ if $\pi_{1}(\mu)=\mu_{1}$ and $\pi_{2}(\mu)=\mu_{2}$.

Example A10.1.

For any distributions $\mu_{1},\mu_{2}$ over $\mathcal{A}_{1},\mathcal{A}_{2}$, respectively, the independent or trivial coupling is: $\mu_{\times}(a_{1},a_{2})=\mu_{1}(a_{1})\cdot\mu_{2}(a_{2}).$

Example A10.2.

Let $\mathbf{Flip}$ be the uniform distribution over booleans, i.e.

[TABLE]

Then the following are two couplings for $\left\langle\mathbf{Flip},\mathbf{Flip}\right\rangle$:

1. (1)

Identity coupling: $\mu_{\rm id}(a_{1},a_{2})=\begin{cases}\frac{1}{2}\ &{\rm if}\ a_{1}=a_{2},\\ 0\ &{\rm otherwise}.\end{cases}$ 2. (2)

Negation coupling: $\mu_{\neg}(a_{1},a_{2})=\begin{cases}\frac{1}{2}\ &{\rm if}\ \neg a_{1}=a_{2},\\ 0\ &{\rm otherwise}.\end{cases}$

Example A10.3.

As a generalisation of Example A10.2, let $\mathbf{Unif}_{\mathcal{A}}$ be the uniform distribution over a finite nonempty set $\mathcal{A}$, i.e.

[TABLE]

for every $a\in\mathcal{A}$. Then each bijection $f:\mathcal{A}\rightarrow\mathcal{A}$ yields a coupling for $\left\langle\mathbf{Unif}_{\mathcal{A}},\mathbf{Unif}_{\mathcal{A}}\right\rangle$:

[TABLE]

Example A10.4.

For any sub-distribution $\mu$ over $\mathcal{A}$, the identity coupling for $\left\langle\mu,\mu\right\rangle$ is:

[TABLE]

Definition A10.2 (Lifting).

Let $\mu_{1},\mu_{2}$ be sub-distributions over $\mathcal{A}_{1},\mathcal{A}_{2}$, respectively, and let $\mathcal{A}\subseteq\mathcal{A}_{1}\times\mathcal{A}_{2}$ be a relation. Then a sub-distribution $\mu$ over $\mathcal{A}_{1}\times\mathcal{A}_{2}$ is called a witness for the $\mathcal{R}$-lifting of $\left\langle\mu_{1},\mu_{2}\right\rangle$ if:

1. (1)

$\mu$* is a coupling for $\left\langle\mu_{1},\mu_{2}\right\rangle$;* 2. (2)

${\rm supp}(\mu)\subseteq\mathcal{R}$.

Whenever a witness exists, we say that $\mu_{1}$ and $\mu_{2}$ are related by the $\mathcal{R}$-lifting and write $\mu_{1}\mathcal{R}^{\#}\mu_{2}$.

Example A10.5.

1. (1)

Coupling $\mu_{f}$ in Example A10.3 is a witness for the lifting:

[TABLE] 2. (2)

Coupling $\mu_{\rm id}$ in Example A10.4 is a witness for the lifting $\mu=^{\#}\mu.$ 3. (3)

Coupling $\mu_{\times}$ in Example A10.1 is a witness for the lifting $\mu_{1}T^{\#}\mu_{2}$, where $T=\mathcal{A}_{1}\times\mathcal{A}_{2}.$

Proposition A10.1.

Let $\mu_{1},\mu_{2}$ be sub-distributions over $\mathcal{A}_{1},\mathcal{A}$, respectively. If there exists a coupling for $\left\langle\mu_{1},\mu_{2}\right\rangle$, then their weight are equal: $|\mu_{1}|=|\mu_{2}|.$

Proposition A10.2.

Let $\mu_{1},\mu_{2}$ be sub-distributions over the same $\mathcal{A}$. Then $\mu_{1}=\mu_{2}$ if and only if $\mu_{1}=^{\#}\mu_{2}$.

A11. Hoare logic for quantum programs

In this section, we review the Hoare-like logic for quantum programs developed in (Ying, 2011, 2016).

A11.1. Partial Correctness and Total Correctness

D’Hondt and Panangaden (D’Hondt and Panangaden, 2006) suggested to use effects as quantum predicates. Then a correctness formula (or a Hoare triple) is a statement of the form $\{A\}P\{B\}$, where $P$ is a quantum program, and both $A,B$ are quantum predicates in $\mathcal{H}_{P}$, called the precondition and postcondition, respectively.

Definition A11.1 (Partial and Total Correctness).

1. (1)

The correctness formula $\{A\}P\{B\}$ is true in the sense of total correctness, written $\models_{\mathit{tot}}\{A\}P\{B\},$ if for all $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P})$ we have:

[TABLE] 2. (2)

The correctness formula $\{A\}P\{B\}$ is true in the sense of partial correctness, written $\models_{\mathit{par}}\{A\}P\{B\},$ if for all $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P})$ we have:

[TABLE]

The defining inequalities of total and partial correctness can be easily understood by observing that the interpretation of ${\mathrm{tr}}(A\rho)$ in physics is the expectation (i.e. average value) of observable $A$ in state $\rho$, and ${\mathrm{tr}}(\rho)-{\mathrm{tr}}(\llbracket P\rrbracket(\rho))$ is indeed the probability that with input $\rho$ program $P$ does not terminate.

A11.2. Proof System

The proof system qPD for partial correctness consists of the axioms and inference rules presented in Figure 11.

It was proved in (Ying, 2011) to be sound and (relatively) complete.

Theorem A11.1 (Soundness and Completeness).

For any quantum program $P$, and for any quantum predicates $A,B$:

[TABLE]

A sound and (relatively) complete proof system for total correctness was also developed in (Ying, 2011, 2016).

A12. Deferred Proofs and Verifications

A12.1. Proof of Proposition 3.2

Proof.

(1$\Rightarrow$2) Obvious.

(2$\Rightarrow$3) It is trivial if we realize the fact $=_{\mathcal{B}}\ \subseteq\ =_{sym}$ for any othornormal basis $\mathcal{B}$.

(3$\Rightarrow$1) Suppose that $\sigma$ is a witness of $\rho_{1}=_{sym}^{\#}\rho_{2}$. Then we have

[TABLE]

which imply $S\sigma=\sigma$ and $\sigma S=\sigma$. Therefore $\sigma=S\sigma S$, and moreover,

[TABLE]

∎

A12.2. Proof of Proposition 3.3

For two Hilbert space $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$, we write $\mathcal{S}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$ for the set of separable states $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$. It is clear from the definition of separability that $\mathcal{S}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$ is a convex set. For any $\rho_{1}\in\mathcal{D}^{\leq}(\mathcal{H}_{1})$ and $\rho_{2}\in\mathcal{D}^{\leq}(\mathcal{H}_{2})$ with the same trace, let $\mathcal{C}(\rho_{1},\rho_{2})$ be the set of all couplings for $\left\langle\rho_{1},\rho_{2}\right\rangle$. It is easy to see that

[TABLE]

is non-empty.

Proposition 3.3 is an immediate corollary of the following:

Fact A12.1.

There are states $\rho_{1}$ in $\mathcal{H}_{1}$, $\rho_{2}$ in $\mathcal{H}_{2}$ and separable quantum predicate $A$ over $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$ such that

[TABLE]

Proof.

Let both $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$ be the two dimensional Hilbert space, and

[TABLE]

In the $2\times 2$ case, the Peres-Horodecki criterion (also called the PPT criterion, for Positive Partial Transpose) is a necessary and sufficient condition for the separability of a density matrix (see (Peres, 1996) for more details). We can check that both $A$ and $\rho_{s}$ are separable using this criterion. Moreover, $A$ is a quantum predicate as $0\sqsubseteq A\sqsubseteq I$, and $\rho_{s},\rho_{e}$ are both the couplings for $\left\langle\rho_{1},\rho_{2}\right\rangle$. We are going to show that

[TABLE]

The right hand side is obvious as ${\mathrm{tr}}(A\rho_{e})$ already achieves the maximum 1. What remains to show is that for any separable state $\sigma$ that couples $(\rho_{1},\rho_{2})$, ${\mathrm{tr}}(A\sigma)\leq\frac{2}{3}$. Write $\sigma$ and its partial transpose (with respect to $\mathcal{H}_{2}$) in the matrix form using the fact that it is a coupling for $\left\langle\rho_{1},\rho_{2}\right\rangle$:

[TABLE]

with real parameter $x$ and complex number $y$ while ‘$\cdot$’ represents the parameters we are not interested in. Note that $\sigma$ is non-negative so that $0\leq x\leq\frac{1}{2}$ and $x^{2}\geq yy^{*}$. On the other hand, $\sigma$ is separable, so $\sigma^{T_{2}}$ is non-negative, which implies $(\frac{1}{2}-x)^{2}\geq yy^{*}$. Thus,

[TABLE]

∎

A12.3. Proof of Lemma 5.1

For any two Hilbert spaces $\mathcal{X}$ and $\mathcal{Y}$. We write $\mathrm{L}(\mathcal{X},\mathcal{Y})$ for the set of linear operators from $\mathcal{X}$ to $\mathcal{Y}$. Then we can introduce an operator-vector correspondence; i.e. the mapping:

[TABLE]

defined by

[TABLE]

for the standard basis elements $|a\rangle$ and $|b\rangle$. Intuitively, it represents a change of bases from the standard basis of $\mathrm{L}(\mathcal{X},\mathcal{Y})$ to the standard basis of $\mathcal{Y}\otimes\mathcal{X}$ (see (Watrous, 2018), Chapter 2). This mapping is a bijection, and indeed an isometry, in the sense that

[TABLE]

for all $M,N\in\mathrm{L}(\mathcal{X},\mathcal{Y})$. Moreover, for any linear map $A:\mathcal{D}^{\leq}(\mathcal{H})\mapsto\mathcal{D}^{\leq}(\mathcal{H})$ with $d=\dim\mathcal{H}$, we can define a new linear map by a $d^{2}\times d^{2}$ matrix $\hat{A}$ in the following way:

[TABLE]

Now, let us write $Y_{1}=M_{10}M_{10}^{\dagger}$ and $Y_{2}=M_{20}M_{20}^{\dagger}$, and define linear maps $\hat{A}_{1}$ and $\hat{A}_{2}$ from the respective linear maps $A_{1}=\llbracket P_{1}\rrbracket\circ\mathcal{E}_{11}$ and $A_{2}=\llbracket P_{2}\rrbracket\circ\mathcal{E}_{21}$. Then the following facts are trivial:

[TABLE]

Moreover, if we define two vectors $|\alpha\rangle=\mathrm{vec}(Y_{1})\oplus\mathrm{vec}(Y_{2})$, $|\beta\rangle=\mathrm{vec}(\rho_{1})\oplus(-\mathrm{vec}(\rho_{2}))$ and $\hat{A}=\hat{A}_{1}\oplus\hat{A}_{2}$, then we obtain:

[TABLE]

using the fact that $\hat{A}^{n}=\hat{A}^{n}_{1}\oplus\hat{A}^{n}_{2}$. With Cayley-Hamilton theorem (see Chapter XV, §112 in (Van der Waerden, 1953)), we know that a matrix power of any order $k$ can be written as a matrix polynomial of degree at most $N-1$ where $N$ is the dimension of the matrix. So, for any $n\geq 0$, there exists coefficients $c_{0},c_{1},\cdots,c_{d_{1}^{2}+d_{2}^{2}-1}$ such that

[TABLE]

noting that $\hat{A}$ is a $(d_{1}^{2}+d_{2}^{2})\times(d_{1}^{2}+d_{2}^{2})$ matrix. Thus, if $Z_{n}=0$ holds for any $0\leq n\leq d_{1}^{2}+d_{2}^{2}-1$, then for any $n\geq 0$,

[TABLE]

A12.4. Proof of Soundness Theorem (Theorem 5.1)

Let us first prove soundness of rules (SO), (SO-L) and (SO-R) because some conclusions obtained in this proof will be used in the proof of other rules. Given a quantum operation $\mathcal{E}$ with its Kraus representation

[TABLE]

its dual map $\mathcal{E}^{*}$ is defined by

[TABLE]

for any operator $A$.

Proposition A12.1.

For any quantum predicate $A$ and trace-preserving quantum operation $\mathcal{E}$, $\mathcal{E}^{*}(A)$ is still a quantum predicate. That is, $0\leq\mathcal{E}^{*}(A)\leq I$ is ture for any $0\leq A\leq I$.

Moreover, we introduce a mathematical (rather than logical) version of Definition 5.1: for any quantum operations $\mathcal{E}$ and $\mathcal{F}$ in a Hilbert space $\mathcal{H}_{1}$, $\mathcal{H}_{2}$, respectively, and for any quantum predicates $A$ and $B$ in $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$, we write:

[TABLE]

if for any $\rho\in\mathcal{D}^{\leq}\left(\mathcal{H}_{1}\otimes\mathcal{H}_{2}\right)$, there exists a coupling $\sigma\in\mathcal{D}^{\leq}\left(\mathcal{H}_{1}\otimes\mathcal{H}_{2}\right)$ for $\left\langle\mathcal{E}({\mathrm{tr}}_{\langle 2\rangle}\rho),\mathcal{F}({\mathrm{tr}}_{\langle 1\rangle}\rho)\right\rangle$ such that

[TABLE]

Lemma A12.1.

For any trace-preserving quantum operations $\mathcal{E},\mathcal{F}$, we have:

[TABLE]

where $(\mathcal{E}\otimes\mathcal{F})^{*}=\mathcal{E}^{*}\otimes\mathcal{F}^{*}$ is the dual map of $\mathcal{E}\otimes\mathcal{F}$.

Proof.

(Outline) We only need to prove that for any input $\rho\in\mathcal{D}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$, $(\mathcal{E}\otimes\mathcal{F})(\rho)$ is a coupling for $\left\langle\mathcal{E}({\mathrm{tr}}_{\langle 2\rangle}\rho),\mathcal{F}({\mathrm{tr}}_{\langle 1\rangle}\rho)\right\rangle$. This fact can be better understood by a physical argument. Suppose Alice and Bob share a bipartite state $\rho\in\mathcal{D}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$. Next, Alice and Bob do the quantum operation $\mathcal{E}$ (mapping states in $\mathcal{H}_{1}$ to $\mathcal{H}_{1^{\prime}}$) and $\mathcal{F}$ (mapping states in $\mathcal{H}_{2}$ to $\mathcal{H}_{2^{\prime}}$) respectively. After that, the state they shared is $(\mathcal{E}\otimes\mathcal{F})(\rho)$. As a quantum operation can be realized by the unitary transformation over the principle system and the environment, in Alice’s view, she cannot gain any information about what Bob does on his part of the state without any classical communication. So, ${\mathrm{tr}}_{\mathcal{H}_{2^{\prime}}}[(\mathcal{E}\otimes\mathcal{F})(\rho)]=\mathcal{E}({\mathrm{tr}}_{\mathcal{H}_{2}}\rho)$. Therefore, $(\mathcal{E}\otimes\mathcal{F})(\rho)$ is still a coupling for $\left\langle\mathcal{E}({\mathrm{tr}}_{\langle 2\rangle}\rho),\mathcal{F}({\mathrm{tr}}_{\langle 1\rangle}\rho)\right\rangle$, and we have:

[TABLE]

(Details) Mathematical details for proving that $(\mathcal{E}\otimes\mathcal{F})(\rho)$ is a coupling for $\left\langle\mathcal{E}({\mathrm{tr}}_{\langle 2\rangle}\rho),\mathcal{F}({\mathrm{tr}}_{\langle 1\rangle}\rho)\right\rangle$ for all $\rho\in{\mathcal{D}}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$. As ${\mathcal{E}}$ and ${\mathcal{F}}$ are both trace-preserving quantum operations, their Kraus operators $\{E_{i}\}$ and $\{F_{j}\}$ must satisfy:

[TABLE]

On the other hand, for any $\rho\in{\mathcal{D}}(\mathcal{H}_{1}\otimes\mathcal{H}_{2})$, due to the Schmidt decomposition theorem (see for example (Nielsen and Chuang, 2002), Theorem 2.7), it can be written as:

[TABLE]

where $p_{l}\in[0,1]$, $\lambda_{l_{k}}$ are complex numbers, and $\{|\alpha_{l_{k}}\rangle\}_{k}$ and $\{|\beta_{l_{k}}\rangle\}_{k}$ are orthonormal basis of $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$ respectively for all $l$. Observe the following fact by straightforward calculations:

[TABLE]

[TABLE]

and similarly, ${\mathrm{tr}}_{\mathcal{H}_{1^{\prime}}}\left[({\mathcal{E}}\otimes{\mathcal{F}})(\rho)\right]={\mathcal{F}}({\mathrm{tr}}_{\mathcal{H}_{1}}(\rho)),$ which complete the proof. ∎

Remark A12.1.

1. (1)

The above lemma can help to simplify the proofs of of the validity of rules (Init) and (UT). Furthermore, we can use it to create/trace-out qubits. 2. (2)

Note that the trace-preserving condition in the above lemma is necessary. So, it doesn’t help when we deal with a single outcome of a measurement. But when we encounter an equivalence between two $\mathbf{if}$ statements of the form $\mathbf{if}\cdots\sim\mathbf{if}\cdots$, all of the sub-programs are all trace-preserving and have simple Kraus representations, we can regard the whole $\mathbf{if}$ statements as a quantum operation, and the above lemma applies.

Now soundness of rules (SO), (SO-L) and (SO-R) can be easily proved. The validity of (SO) is just a corollary of Lemma A12.1. Realise that the semantic function of ${\bf skip}$ is the identity operation, so (SO-L) and (SO-R) are two special cases of (SO).

In addition, the following technical lemma will be needed in the remainder of this subsection.

Lemma A12.2.

Consider a bipartite system $A$ and $B$ with state Hilbert space $\mathcal{H}_{A}$ and $\mathcal{H}_{B}$, respectively. Given two linear operators $M:\mathcal{H}_{A}\mapsto\mathcal{H}_{A^{\prime}}$ and $N:\mathcal{H}_{B}\mapsto\mathcal{H}_{B^{\prime}}$ such that $N^{\dagger}N\leq I_{\mathcal{H}_{B}}$. Then for any $\rho\in{\mathcal{D}}(\mathcal{H}_{A}\otimes\mathcal{H}_{B})$, it holds that:

[TABLE]

In particular, if linear operators $N_{1},N_{2},\cdots,N_{n}$ mapping from $\mathcal{H}_{B}$ to $\mathcal{H}_{B^{\prime}}$ satisfy $\sum_{i=1}^{n}N_{i}^{\dagger}N_{i}\sqsubseteq I_{\mathcal{H}_{B}}$, then:

[TABLE]

More generally, for any quantum operations ${\mathcal{E}}_{A}:{\mathcal{D}}^{\leq}(\mathcal{H}_{A})\mapsto{\mathcal{D}}^{\leq}(\mathcal{H}_{A^{\prime}})$ and ${\mathcal{F}}_{B}:{\mathcal{D}}^{\leq}(\mathcal{H}_{B})\mapsto{\mathcal{D}}^{\leq}(\mathcal{H}_{B^{\prime}})$, it holds that

[TABLE]

Proof.

Actually, if the dimensions of $\mathcal{H}_{A}$ and $\mathcal{H}_{B}$ are not same, then we can always enlarge the small one to the same dimension. So, without of generality, we assume $\mathcal{H}_{A}$ and $\mathcal{H}_{B}$ are the same $\mathcal{H}$ of dimension $d$ (finite or infinite). Then, it is possible to define the maximal entangled operator $\Phi$:

[TABLE]

where $\{|i\rangle\}$ is an orthonormal basis of $\mathcal{H}$. For any pure state $|\psi\rangle$ in $\mathcal{H}\otimes\mathcal{H}$, there exists linear operator $X$ such that:

[TABLE]

It is straightforward to show that

[TABLE]

using the assumption $N^{\dagger}N\leq I_{\mathcal{H}}$ which leads to $(N^{\dagger}N)^{T}\leq I_{\mathcal{H}}$. Therefore, for any density operators, inequality (31) holds.

If linear operators $N_{1},N_{2},\cdots,N_{n}$ over $\mathcal{H}_{B}$ satisfy $\sum_{i=1}^{n}N_{i}^{\dagger}N_{i}=I_{\mathcal{H}_{B}}$, then for any pure state $|\psi\rangle$ in $\mathcal{H}\otimes\mathcal{H}$, we have:

[TABLE]

The linearity ensures the truth of Eqn. (32).

Assume that ${\mathcal{E}}_{A}(\cdot)=\sum_{m}E_{m}(\cdot)E_{m}^{\dagger}$ and ${\mathcal{F}}_{A}(\cdot)=\sum_{n}F_{n}(\cdot)F_{n}^{\dagger}$, then for any $\rho$:

[TABLE]

as $\sum_{n}F_{n}^{\dagger}F_{n}\sqsubseteq I_{\mathcal{H}}$ (${\mathcal{F}}$ is a quantum operation). ∎

Now we are ready to prove the whole Theorem 5.1. It suffices to prove validity of all axioms and inference rules in Figures 3, 4, 6, 7 and 8:

$\bullet$ (Skip) Obvious.

$\bullet$ (Init) For any $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}})$, set:

[TABLE]

where $\mathcal{E}$ and $\mathcal{F}$ are two initial quantum operations with Kraus operators $\{|0\rangle_{q_{1}\langle 1\rangle}\langle i|\}$ and $\{|0\rangle_{q_{2}\langle 2\rangle}\langle i|\}$, respectively. As $\mathcal{E}$ and $\mathcal{F}$ are all trace-preserving, we know that ${\mathrm{tr}}(\rho)={\mathrm{tr}}(\sigma)$, and $(\mathcal{E}\otimes\mathcal{F})(\rho)$ is a coupling for

[TABLE]

Moreover, we have:

[TABLE]

$\bullet$ (UT) For any $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}})$, we set

[TABLE]

Of course, ${\mathrm{tr}}(\rho)={\mathrm{tr}}(\sigma)$. Due to the unitarity of $U_{1}$ and $U_{2}$, we have:

[TABLE]

and

[TABLE]

which ensure that $\sigma$ is a coupling for

[TABLE]

Moreover, it holds that

[TABLE]

$\bullet$ (SC+) For $j=1,2$, we write $\mathcal{H}_{\langle j\rangle}$ for the input state Hilbert space of program $P_{j};P_{j}^{\prime}$. Assume that

[TABLE]

We are going to show that

[TABLE]

For any $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{\langle 1\rangle}\otimes\mathcal{H}_{\langle 2\rangle})$, if $\rho\models\Gamma$, then it follows from assumption (i) that there exists a coupling $\sigma$ for $\left\langle\llbracket P_{1}\rrbracket({\mathrm{tr}}_{\langle 2\rangle}\rho),\llbracket P_{2}\rrbracket({\mathrm{tr}}_{\langle 1\rangle}\rho)\right\rangle$ such that

[TABLE]

Thus, by assumption (iii) and Definition 5.7 we see that $\sigma\models\Delta$. This together with assumption (ii) implies that there exists a coupling $\delta$ for $\left\langle\llbracket P_{1}^{\prime}\rrbracket({\mathrm{tr}}_{\langle 2\rangle}\sigma),\llbracket P_{2}^{\prime}\rrbracket({\mathrm{tr}}_{\langle 1\rangle}\sigma)\right\rangle$ such that

[TABLE]

Consequently, it holds that

[TABLE]

Therefore, it suffices to show that $\delta$ is a coupling for $\left\langle\llbracket P_{1};P_{1}^{\prime}\rrbracket({\mathrm{tr}}_{\langle 2\rangle}\rho),\llbracket P_{2};P_{2}^{\prime}\rrbracket({\mathrm{tr}}_{\langle 1\rangle}\rho)\right\rangle$. This is obvious as

[TABLE]

and similarly ${\mathrm{tr}}_{\langle 1\rangle}\delta=\llbracket P_{2};P_{2}^{\prime}\rrbracket({\mathrm{tr}}_{\langle 1\rangle}\rho)$.

$\bullet$ (IF) Suppose that $\models P_{1m}\sim P_{2n}:B_{mn}\Rightarrow C$ for every $(m,n)\in S$. Then for any input $\rho$ with reduced density matrices $\rho_{1}={\mathrm{tr}}_{\langle 2\rangle}(\rho),\rho_{2}={\mathrm{tr}}_{\langle 1\rangle}(\rho)$, if $(m,n)\in S$, then there exists a coupling $\sigma_{mn}$ for

[TABLE]

such that

[TABLE]

Now we set $\sigma=\sum_{(m,n)\in S}\sigma_{mn}$. Then using Proposition 3.3.1(v) in (Ying, 2016) and Lemma A12.2 we obtain:

[TABLE]

and set the difference $\delta_{1}=\llbracket\mathbf{if}\ (\square m\cdot M_{1}[\overline{q}]=m\rightarrow P_{1m})\ \mathbf{fi}\rrbracket(\rho_{1})-{\mathrm{tr}}_{\langle 2\rangle}(\sigma)$. Similarly, we have:

[TABLE]

and set $\delta_{2}=\llbracket\mathbf{if}\ (\square n\cdot M_{1}[\overline{q}]=n\rightarrow P_{2n})\ \mathbf{fi}\rrbracket(\rho_{2})-{\mathrm{tr}}_{\langle 1\rangle}(\sigma).$ The premises of lossless guarantee the existence of coupling for outputs, and therefore, $\delta_{1}$ and $\delta_{2}$ has the same trace. So, $\sigma+\delta_{1}\otimes\delta_{2}/tr(\delta_{1})$ is a coupling for

[TABLE]

Moreover, it holds that

[TABLE]

Therefore, it holds that

[TABLE]

$\bullet$ (IF1) For any $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}})$ satisfying the condition ${\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}$, due to the assumption that

[TABLE]

for each possible outcome $m$, there exists a coupling $\sigma_{m}$ for $\left\langle M_{1m}({\mathrm{tr}}_{\langle 2\rangle}\rho)M_{1m}^{\dagger},M_{2m}({\mathrm{tr}}_{\langle 1\rangle}\rho)M_{2m}^{\dagger}\right\rangle,$ such that ${\mathrm{tr}}(\rho)=\sum_{m}{\mathrm{tr}}(\sigma_{m})$ and

[TABLE]

Moreover, according to the second assumption that

[TABLE]

for each $\sigma_{m}$, there exists a coupling $\delta_{m}$ for $\left\langle\llbracket P_{1m}\rrbracket({\mathrm{tr}}_{\langle 2\rangle}\sigma_{m}),\llbracket P_{2m}\rrbracket({\mathrm{tr}}_{\langle 1\rangle}\sigma_{m})\right\rangle$ such that

[TABLE]

Set $\delta=\sum_{m}\delta_{m}$. Then we obtain:

[TABLE]

Moreover, it is straightforward to see

[TABLE]

and similarly

[TABLE]

$\bullet$ (LP) For simplicity, let us use $Q_{1}$ to denote the while-statement:

[TABLE]

and $Q_{2}$ to denote

[TABLE]

We also introduce an auxiliary notation: for $i=1,2$, quantum operation $\mathcal{E}_{i0}$ and $\mathcal{E}_{i1}$ are defined by the measurement ${\mathcal{M}}_{i}$

[TABLE]

The lossless condition ensures that both $P_{1}$ and $P_{2}$ are terminating subprograms. For simplicity, we use notations $M_{0}=M_{10}\otimes M_{20}$ and $M_{1}=M_{11}\otimes M_{21}$. For any $\rho\in\mathcal{D}(\mathcal{H}_{Q_{1}}\otimes\mathcal{H}_{Q_{2}})$, we inductively define the following sequence of states:

1. (1)

$\sigma_{0}=\rho$; 2. (2)

for input $M_{1}\sigma_{n}M_{1}^{\dagger}$, due to the second assumption, $\sigma_{n+1}$ is the coupling of the outputs

[TABLE]

such that:

[TABLE]

We first prove by induction that for all $n\geq 0$, it holds that

[TABLE]

It is trivial for $n=0$. Suppose it holds for $n=k$, then for $n=k+1$, we have

[TABLE]

using Lemma A12.2.

Actually, the assumption that $Q_{1}$ is lossless ensures that $\lim_{n\rightarrow\infty}(\llbracket P_{1}\rrbracket\circ{\mathcal{E}}_{11})^{n}({\mathrm{tr}}_{\langle 2\rangle}\rho)=0$ as its trace characterizes the probability of nontermination. Therefore, $\lim_{n\rightarrow\infty}\sigma_{n}=0$. Together with the choice of $\sigma_{n}$, we have

[TABLE]

Let us define $\tau=\sum_{n=0}^{\infty}(M_{0}\sigma_{n}M_{0}^{\dagger})$. According to Lemma A12.2 again, the following inequality holds:

[TABLE]

Similarly, ${\mathrm{tr}}_{\langle 1\rangle}(\tau)\sqsubseteq\llbracket Q_{2}\rrbracket({\mathrm{tr}}_{\langle 1\rangle}\rho)$. Set:

[TABLE]

the terminating condition of both $\bf while$ programs guarantees that $\delta_{1}$ and $\delta_{2}$ have the same trace, and therefore, $\tau+\delta_{1}\otimes\delta_{2}/{\mathrm{tr}}(\delta_{1})$ is a coupling of $\left\langle\llbracket Q_{1}\rrbracket({\mathrm{tr}}_{\langle 2\rangle}\rho),\llbracket Q_{2}\rrbracket({\mathrm{tr}}_{\langle 1\rangle}\rho)\right\rangle$ and satisfies

[TABLE]

$\bullet$ (LP1) We use the same notations as in above proof of (LP). For any input state $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{Q_{1}}\otimes\mathcal{H}_{Q_{2}})$ satisfying the condition

[TABLE]

and for any $n\geq 0$, we must have:

[TABLE]

which implies that any coupling for

[TABLE]

must satisfies the condition ${\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}$. Choose $\delta_{0}=\rho$ so that $\delta_{0}$ is a coupling for $\left\langle{\mathrm{tr}}_{\langle 2\rangle}\rho,{\mathrm{tr}}_{\langle 1\rangle}\rho\right\rangle$, the following statement holds for $n\geq 0$:

[TABLE]

The above statement can be proved by induction. For basis $n=0$, of course, $\rho$ satisfies ${\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}$, due to the assumption

[TABLE]

we must have two couplings $\sigma_{00}$ and $\sigma_{10}$ for $\left\langle\mathcal{E}_{10}({\mathrm{tr}}_{\langle 2\rangle}\rho),\mathcal{E}_{20}({\mathrm{tr}}_{\langle 1\rangle}\rho)\right\rangle$ and $\left\langle\mathcal{E}_{11}({\mathrm{tr}}_{\langle 2\rangle}\rho),\mathcal{E}_{21}({\mathrm{tr}}_{\langle 1\rangle}\rho)\right\rangle$ respectively, such that

[TABLE]

as we set $\delta_{0}=\rho$.

According to the second assumption $\vdash P_{1}\sim P_{2}:B_{1}\Rightarrow A$, there exists a coupling $\delta_{1}$ for $\left\langle\llbracket P_{1}\rrbracket({\mathrm{tr}}_{\langle 2\rangle}\sigma_{10}),\llbracket P_{2}\rrbracket({\mathrm{tr}}_{\langle 1\rangle}\sigma_{10})\right\rangle$ such that

[TABLE]

Note that

[TABLE]

so $\delta_{1}$ is a coupling for

[TABLE]

So the induction basis is true.

Suppose the statement holds for $n=k-1\ (k\geq 1)$ , we will show that the statement also holds for $n=k$. From the assumption, we know that $\delta_{k}$ is a coupling for

[TABLE]

and it also satisfies ${\mathcal{M}}_{1}\approx{\mathcal{M}}_{2}$, so due to the assumption

[TABLE]

we must have two couplings $\sigma_{0k}$ for

[TABLE]

and $\sigma_{1k}$ for

[TABLE]

such that

[TABLE]

According to the second assumption

[TABLE]

there exists a coupling $\delta_{k+1}$ for

[TABLE]

such that

[TABLE]

So the statement holds for any $n\geq 0$. From the statement, we have the following equations for $N\geq 0$:

[TABLE]

and also for $N\geq 0$,

[TABLE]

Notice that

[TABLE]

Therefore, $\lim_{N\rightarrow\infty}\sum_{n=0}^{N}\sigma_{n}$ does exist. Set

[TABLE]

and let $N\rightarrow\infty$ in the above inequality. Then we have:

[TABLE]

Moreover, it is straightforward that $\sigma$ is a coupling for

[TABLE]

$\bullet$ (Init-L) For any $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}})$, set:

[TABLE]

where $\mathcal{E}$ is the initial quantum operation with Kraus operators $\{|0\rangle_{q_{1}\langle 1\rangle}\langle i|\}$ and $\mathcal{I}$ is the identity operation. As $\mathcal{E}$ and $\mathcal{I}$ are all trace-preserving, we know that ${\mathrm{tr}}(\rho)={\mathrm{tr}}(\sigma)$, and $(\mathcal{E}\otimes\mathcal{I})(\rho)$ is a coupling for

[TABLE]

Moreover,

[TABLE]

$\bullet$ (UT-L) Similar to (UT) if we regard $\llbracket\mathbf{skip}\rrbracket$ as $\llbracket q:=I[q]\rrbracket$ where $I$ is the identity matrix of the Hilbert space of all variables.

$\bullet$ (IF-L) Very similar to (IF); omitted.

$\bullet$ (IF1-L) Similar to (IF1). For any $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}})$, due to the assumption

[TABLE]

so there exists a serial of states $\sigma_{m}$ and $\rho_{2m}$ with

[TABLE]

such that for all $m$, $\sigma_{m}$ is a coupling for

[TABLE]

and

[TABLE]

Moreover, according to the second assumption

[TABLE]

for each $\sigma_{m}$, there exists a coupling $\delta_{m}$ for

[TABLE]

such that

[TABLE]

Set $\delta=\sum_{m}\delta_{m}$, then

[TABLE]

Moreover, it is straightforward to see

[TABLE]

and

[TABLE]

$\bullet$ (LP-L) Similar to (LP1). We use notations:

[TABLE]

${\mathcal{E}}_{10}(\cdot)=M_{10}(\cdot)M_{10}^{\dagger}$ and ${\mathcal{E}}_{11}(\cdot)=M_{11}(\cdot)M_{11}^{\dagger}$. The lossless condition of $Q_{1}$ ensures that $P_{1}$ is a terminating subprogram. For simplicity, we use notations $M_{0}=M_{10}\otimes I_{2}$ and $M_{1}=M_{11}\otimes I_{2}$. For any $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{Q_{1}}\otimes\mathcal{H}_{Q_{2}})$, we inductively define the following sequence of states:

1. (1)

$\sigma_{0}=\rho$; 2. (2)

for input $M_{1}\sigma_{n}M_{1}^{\dagger}$, due to the second assumption, $\sigma_{n+1}$ is the coupling of the outputs

[TABLE]

such that:

[TABLE]

We first prove by induction that for all $n\geq 0$, it holds that

[TABLE]

It is trivial for $n=0$ according to Lemma A12.2. Suppose it holds for $n=k$, then for $n=k+1$, using Lemma A12.2 we have:

[TABLE]

and:

[TABLE]

Actually, the assumption that $Q_{1}$ is lossless ensures that $\lim_{n\rightarrow\infty}(\llbracket P_{1}\rrbracket\circ{\mathcal{E}}_{11})^{n}({\mathrm{tr}}_{\langle 2\rangle}\rho)=0$ as its trace characterizes the probability of nontermination. Therefore, $\lim_{n\rightarrow\infty}\sigma_{n}=0$. Together with the choice of $\sigma_{n}$, we have

[TABLE]

Let us define $\tau=\sum_{n=0}^{\infty}(M_{0}\sigma_{n}M_{0}^{\dagger})$. According to Lemma A12.2 again, we can show that $\tau$ is a coupling of the outputs:

[TABLE]

and

[TABLE]

$\bullet$ (LP1-L) Similar to (LP1). Let us use $Q_{1}$ to denote the left while program

[TABLE]

and $Q_{2}$ to denote the right program $\mathbf{skip}$ for simplicity, and introduce an auxiliary notation: for $i=1,2$, the quantum operation $\mathcal{E}_{0}$ and $\mathcal{E}_{1}$ are defined by the measurement ${\mathcal{M}}_{1}$

[TABLE]

For any input state $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{Q_{1}}\otimes\mathcal{H}_{Q_{2}})$, choose $\delta_{0}=\rho$ so that $\delta_{0}$ is a coupling for $\left\langle{\mathrm{tr}}_{\langle 2\rangle}\rho,{\mathrm{tr}}_{\langle 1\rangle}\rho\right\rangle$, and $\varrho_{1,-1}={\mathrm{tr}}_{\langle 1\rangle}\rho$, then the following statement holds for $n\geq 0$:

[TABLE]

The above statement can be proved by induction. For basis $n=0$, due to the assumption ${\mathcal{M}}_{1}\approx I_{2}\models A\Rightarrow\{B_{0},B_{1}\}$, there exist $\varrho_{00}$, $\varrho_{10}$ and two couplings $\sigma_{00}$ for $\left\langle\mathcal{E}_{0}({\mathrm{tr}}_{\langle 2\rangle}\rho),\varrho_{00}\right\rangle$ and $\sigma_{10}$ for $\left\langle\mathcal{E}_{1}({\mathrm{tr}}_{\langle 2\rangle}\rho),\varrho_{10}\right\rangle,$ such that

[TABLE]

as we set $\delta_{0}=\rho$ and $\varrho_{1,-1}={\mathrm{tr}}_{\langle 1\rangle}\rho$. According to the second assumption $\vdash P_{1}\sim\mathbf{skip}:B_{1}\Rightarrow A$, there exists a coupling $\delta_{1}$ for $\left\langle\llbracket P_{1}\rrbracket({\mathrm{tr}}_{\langle 2\rangle}\sigma_{10}),{\mathrm{tr}}_{\langle 1\rangle}\sigma_{10}\right\rangle$ such that

[TABLE]

Note that

[TABLE]

so $\delta_{1}$ is a coupling for $\langle(\llbracket P_{1}\rrbracket\circ\mathcal{E}_{1})({\mathrm{tr}}_{\langle 2\rangle}\rho),\varrho_{10}\rangle.$ So the basis is true.

Suppose the statement holds for $n=k-1(k\geq 1)$, we will show that the statement also holds for $n=k$. From the assumption ${\mathcal{M}}_{1}\sim I_{2}\models A\Rightarrow\{B_{0},B_{1}\}$, there exist $\varrho_{0k}$, $\varrho_{1k}$ and two couplings $\sigma_{0k}$ for

[TABLE]

and $\sigma_{1k}$ for

[TABLE]

such that

[TABLE]

According to the second assumption $\vdash P_{1}\sim\mathbf{skip}:B_{1}\Rightarrow A$, there exists a coupling $\delta_{k+1}$ for

[TABLE]

such that

[TABLE]

So the statement holds for any $n\geq 0$. From the statement, we have the following inequality for $N\geq 0$ (similar to the proof of (LP-E)):

[TABLE]

We can notice that $\lim_{N\rightarrow\infty}\sum_{n=0}^{N}\sigma_{0n}$ does exist via similar arguments of of (LP). Set $\sigma=\lim_{N\rightarrow\infty}\sum_{n=0}^{N}\sigma_{0n}$, and let $N\rightarrow\infty$ in the above inequality, we have:

[TABLE]

Moreover, we can check the following equation:

[TABLE]

The last equality holds because

[TABLE]

followed from the assumption $\models\mathbf{while}\ {\mathcal{M}}_{1}[\overline{q}]=1\ \mathbf{do}\ P_{1}\ \mathbf{od}\text{\ lossless}$, therefore, $\lim_{N\rightarrow\infty}\varrho_{1N}=0$. Now, it is straightforward that $\sigma$ is a coupling for

[TABLE]

$\bullet$ (Conseq) It follows immediately from the fact that $A\sqsubseteq B$ implies ${\mathrm{tr}}(A\rho)\leq{\mathrm{tr}}(B\rho)$ for all $\rho$.

$\bullet$ (Weaken) Obvious.

$\bullet$ (Case) For any $\rho\in\mathcal{D}^{\leq}(\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}})$, if $\rho\models\Gamma$, then it follows from the assumption that for each $i$, there exists a coupling $\sigma_{i}$ for $\left\langle\llbracket P_{1}\rrbracket({\mathrm{tr}}_{2}(\rho)),\llbracket P_{2}\rrbracket({\mathrm{tr}}_{1}(\rho))\right\rangle$ such that

[TABLE]

We set $\sigma=\sum_{i=1}^{n}p_{i}\sigma_{i}$. Then

[TABLE]

and ${\mathrm{tr}}_{2}(\sigma)=\llbracket P_{1}\rrbracket({\mathrm{tr}}_{2}(\rho))$. Therefore, it holds that $\Gamma\models P_{1}\sim P_{2}:\sum_{i=1}^{n}p_{i}A_{i}\Rightarrow B$.

$\bullet$ (Frame) Assume that $\Gamma\models P_{1}\sim P_{2}:A\Rightarrow B$. Moreover, suppose $V=V_{1}\cup V_{2}$ where $V_{1}$ represents the extended variables of $P_{1}$ and $V_{2}$ of $P_{2}$. Of course, $V_{1}\cap V_{2}=\emptyset$ and $\mathcal{H}_{V}=\mathcal{H}_{V_{1}}\otimes\mathcal{H}_{V_{2}}$. We prove $\Gamma\cup\left\{[V,\mathit{var}(P_{1},P_{2})]\right\}\models P_{1}\sim P_{2}:A\otimes C\Rightarrow B\otimes C$; that is, for any separable state $\rho$ between $\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}}$ and $\mathcal{H}_{V}$, if $\rho\models$, then there exists a coupling $\rho^{\prime}$ in $\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}}\otimes\mathcal{H}_{V}$ for

[TABLE]

such that

[TABLE]

First of all, by separability of $\rho$, we can write:

[TABLE]

where $\rho_{i}\in\mathcal{D}^{\leq}(\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}})$, $\sigma_{i}\in\mathcal{D}^{\leq}(\mathcal{H}_{V})$ and $p_{i}\geq 0$. Since $V\cap\mathrm{var}(P_{1},P_{2})=\emptyset$, it holds that

[TABLE]

For each $i$, since $\rho\models\Gamma$ and $\Gamma\models P_{1}\sim P_{2}:A\Rightarrow B$, there exists a coupling $\rho_{i}^{\prime}$ for

[TABLE]

such that ${\mathrm{tr}}(A\rho_{i})\leq{\mathrm{tr}}(B\rho_{i}^{\prime})+{\mathrm{tr}}(\rho_{i})-{\mathrm{tr}}(\rho_{i}^{\prime})$. We set:

[TABLE]

Then we can check that

[TABLE]

and ${\mathrm{tr}}_{\langle 1\rangle}(\rho^{\prime})=\llbracket P_{2}\rrbracket({\mathrm{tr}}_{\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{V_{1}}}(\rho))$. Therefore, $\rho^{\prime}$ is a coupling for

[TABLE]

Furthermore, we have:

[TABLE]

∎

A12.5. Verification of Example 1.1

First, the applications of axiom (UT-R) and (UT) yields:

[TABLE]

[TABLE]

[TABLE]

where:

[TABLE]

Now we need the following technical lemma:

Lemma A12.3.

Let $B_{0}=|0\rangle\langle 0|\otimes I$, $B_{1}=|1\rangle\langle 1|\otimes I,$ and $B=B_{0}+B_{1}=I\otimes I.$ Then we have:

[TABLE]

Proof.

For any $\rho\models{\mathcal{M}}\approx{\mathcal{M}}^{\prime}$, it must holds that:

[TABLE]

Set $\sigma_{0}=\langle 0|{\mathrm{tr}}_{2}(\rho)|0\rangle\cdot|0\rangle\langle 0|\otimes|+\rangle\langle+|$ and $\sigma_{1}=\langle 1|{\mathrm{tr}}_{2}(\rho)|1\rangle\cdot|1\rangle\langle 1|\otimes|-\rangle\langle-|$, which are exactly the coupling of $\left\langle M_{0}{\mathrm{tr}}_{2}(\rho)M_{0},M_{0}^{\prime}{\mathrm{tr}}_{1}(\rho)M_{0}^{\prime}\right\rangle$ and $\left\langle M_{1}{\mathrm{tr}}_{2}(\rho)M_{1},M_{1}^{\prime}{\mathrm{tr}}_{1}(\rho)M_{1}^{\prime}\right\rangle$, respectively. So, ${\mathrm{tr}}(A_{00}\sigma_{0})=\langle 0|{\mathrm{tr}}_{2}(\rho)|0\rangle$ and ${\mathrm{tr}}(A_{11}\sigma_{1})=\langle 1|{\mathrm{tr}}_{2}(\rho)|1\rangle$. On the other hand,

[TABLE]

Similarly, we have ${\mathrm{tr}}(B_{1}\rho)={\mathrm{tr}}(A_{11}\sigma_{1})$. Therefore, ${\mathrm{tr}}(B\rho)={\mathrm{tr}}(A_{00}\sigma_{0})+{\mathrm{tr}}(A_{11}\sigma_{1}).$ ∎

Combining (34), (35) and (36), we obtain:

[TABLE]

Furthermore, we have:

[TABLE]

It holds that

[TABLE]

because

[TABLE]

Then (6) is proved by combining (33) and (37) to (39) using rule (SC+) by checking the entailment between side-conditions:

[TABLE]

Deduction without (IF1) Now, we use rule (IF) to derive the precondition of two ${\bf if}$ statements.

[TABLE]

where:

[TABLE]

Applying rule (IF) directly we obtain:

[TABLE]

where

[TABLE]

Similarly, using rule (UT-L) and (Init), we are only able to derive

[TABLE]

However, $=_{\mathcal{B}}\ \not\sqsubseteq\frac{7}{8}I\otimes I$, so the rule of (IF) is too weak to derive the judgment we desired.

A12.6. Proof of Proposition 6.1

Proof.

For simplicity, we write

[TABLE]

First of all, we notice that for any $\rho\in{\mathcal{D}}^{\leq}(\mathcal{H}_{P}\otimes\mathcal{H}_{P})$ and any basis state $|i\rangle$ in $\mathcal{B}$,

[TABLE]

(1) $\Rightarrow$ (2): If (1) is valid, then

[TABLE]

for any basis state $|i\rangle$ in $\mathcal{B}$ and any $\rho_{1}\in{\mathcal{D}}(\mathcal{H}_{P})$ with $tr(\rho_{1})=1$. Therefore, $\llbracket P\rrbracket$ is a terminating quantum program which ensures the existence of the coupling for the outputs.

On the other hand, for any $\rho$ with unit trace, suppose $\sigma$ is a coupling for the outputs

[TABLE]

then it holds that

[TABLE]

(2) $\Rightarrow$ (1): If equation (12) is true for every $i$, then for any $\rho_{1},\rho_{2}\in{\mathcal{D}}(\mathcal{H}_{P})$ with unit trace, there exist couplings $\rho$ and $\sigma$ for $\left\langle\rho_{1},\rho_{2}\right\rangle$ and $\left\langle\llbracket P\rrbracket(\rho_{1}),\llbracket P\rrbracket(\rho_{2})\right\rangle$ respectively such that

[TABLE]

On the other hand, we have:

[TABLE]

Consequently, we obtain:

[TABLE]

for every $i$; that is, $\llbracket P\rrbracket(\rho_{1})$ is uniform in $\mathcal{B}=\{|i\rangle\}$ for any $\rho_{1}$.

(1) $\Rightarrow$ (3): Suppose (1) is valid. Similar to the above proof for (1) $\Rightarrow$ (2), it is sufficient to show that, for any $\rho_{1},\rho_{2}\in{\mathcal{D}}(\mathcal{H}_{P})$ with unit trace, by linearity we have

[TABLE]

(3) $\Rightarrow$ (1): If equation (13) is true for every $i$, then for any pure state $\rho_{1}=|\alpha\rangle\langle\alpha|\in{\mathcal{D}}(\mathcal{H}_{P})$, we set $\rho_{2}=\rho_{1}^{T}$. There must exist a coupling $\sigma$ for $\left\langle\llbracket P\rrbracket(\rho_{1}),\llbracket P\rrbracket(\rho_{2})\right\rangle$ such that

[TABLE]

On the other hand, we have:

[TABLE]

which implies

[TABLE]

for every $i$; that is, $\llbracket P\rrbracket(\rho_{1})$ is uniform in $\mathcal{B}=\{|i\rangle\}$ for any pure state $\rho_{1}$. By linearity, we know that $\llbracket P\rrbracket(\rho)$ is uniform in $\mathcal{B}=\{|i\rangle\}$ for any state $\rho$.

Remark A12.2.

Note that the maximally entangled state $|\Phi\rangle$ and thus $=_{\mathcal{C}}^{e}$ are determined by the given orthonormal basis $\mathcal{C}$. From the above proof, we see that if clause (3) in the above proposition is valid for some orthonormal basis $\mathcal{C}$, then it must be valid for any other orthonormal basis $\mathcal{C}^{\prime}$.

∎

A12.7. Verification of Example 6.1

For simplicity of the presentation, a judgment $\Gamma\vdash P_{1}\sim P_{2}:A\Rightarrow B$ using an inference rule $R$ in rqPD is displaced as

[TABLE]

A formal proof of judgment (14) using the inference rules of rqPD is presented in Figure 12 together with the following parameters:

[TABLE]

Before using the (LP1) rules, we need first to check the validity of

[TABLE]

To see this, for any $\rho$ satisfies ${\mathcal{M}}\approx{\mathcal{M}}$, we choose the coupling $\sigma_{0}$ and $\sigma_{1}$

[TABLE]

for $\left\langle M_{0}{\mathrm{tr}}_{\langle 2\rangle}(\rho)M_{0}^{\dagger},\ M_{0}{\mathrm{tr}}_{\langle 1\rangle}(\rho)M_{0}^{\dagger})\right\rangle$ and $\left\langle M_{1}{\mathrm{tr}}_{\langle 2\rangle}(\rho)M_{1}^{\dagger},\ M_{1}{\mathrm{tr}}_{\langle 1\rangle}(\rho)M_{1}^{\dagger})\right\rangle$ respectively, and suppose that the matrix form of $\rho_{1}={\mathrm{tr}}_{\langle 2\rangle}(\rho)$ is

[TABLE]

Then we can calculate the following equations carefully:

[TABLE]

The side condition of equal probability $({\mathcal{M}},P)\approx({\mathcal{M}},P)$ (where $P\equiv q_{x}:=U[q_{x}];\ q_{y}:=U[q_{y}];$ is the loop body) is trivially holds as the two programs are the same and independent of inputs; that is,

[TABLE]

Therefore, we can regard $A$ as the pre-condition and $B_{0}$ as the post-condition of the while loop, and together with the ${\rm(SC+)}$ rule we conclude that judgment (14) is valid.

Impossibility of Using (LP) to derive judgment (14)

As shown in Fig. 12, if $D=\frac{1}{2}I_{q_{x}}\otimes I_{q_{y}}\otimes I_{q_{x}^{\prime}}\otimes I_{q_{y}^{\prime}}$ is derivable, then the precondition $A$ before the ${\bf while}$ loops must satisfy:

[TABLE]

To simplify the calculation, let us choose a special case to see that above inequality does not holds for all possible $|\psi\rangle$ and non-trivial $U$. We set:

[TABLE]

Suppose $A$ is derivable using rule (LP) for two ${\bf while}$ programs with postcondition $B_{0}$, we must have the following proof outline:

[TABLE]

It is straightforward to observe:

[TABLE]

and

[TABLE]

which implies that:

[TABLE]

Therefore,

[TABLE]

which violates Eqn. (40). So we conclude that judgment (14) is not derivable using (LP) and the use of (LP1) is needed.

A12.8. Verification of Judgment (15)

This subsection gives a verification of the first formulation of correctness of quantum teleportation. The verification is presented in Figure 13.

Let us carefully explain the notations and several key steps in the proof. We use $s$ to denote the state space of the second program $\bf{skip}$. Therefore we can write:

[TABLE]

Note that

[TABLE]

So, our goal is to prove:

[TABLE]

For any vectors $|\alpha\rangle$ and $|\beta\rangle$, we have the following:

[TABLE]

So, we can calculate $D$ directly:

[TABLE]

Therefore, the judgment is valid.

A12.9. Verification of Judgment (16)

This subsection gives a verification of the second formulation of correctness of quantum teleportation. A formal proof of judgment (16) using the inference rules of rqPD is presented in Figure 14.

Similarly to the proof of judgment (15) above, we use $s$ to denote the state space of the second program $\bf{skip}$ and introduce a different symbol $A$:

[TABLE]

Using the same definition of $E$ in Eqn. (41), our goal is to prove:

[TABLE]

We can calculate $D$ directly from $C$ according to the facts in Eqns. (A12.8):

[TABLE]

Therefore, the judgment is valid.

A12.10. Verification of Judgments (18), (19) and (20)

In this subsection, we verify the reliability of quantum teleportation against several models of quantum noise.

Now, using the inference rules in Figure 3, 4 and 9, we present the formal proof in Figure 15. We can calculate the following equations directly. For simplicity, $[\cdot]$ is a copy of the context between the previous $[$ and $]$.

[TABLE]

Our aim is to calculate what is S:

[TABLE]

using the following fact (of course, it also holds with superscript primes over each index):

[TABLE]

$\bullet$ ${\rm QTEL_{\it BF}}\sim{\rm QTEL}$

For the bif flip noise, the following fact can be easily realized:

[TABLE]

Thus,

[TABLE]

Therefore, the precondition $S$ is:

[TABLE]

$\bullet$ ${\rm QTEL_{\it PF}}\sim{\rm QTEL}$

For the phase flip noise, the following fact can be easily realized:

[TABLE]

Thus,

[TABLE]

Therefore, the precondition $S$ is:

[TABLE]

$\bullet$ ${\rm QTEL_{\it BPF}}\sim{\rm QTEL}$

For the phase flip noise, the following fact can be easily realized:

[TABLE]

Thus,

[TABLE]

Therefore, the precondition $S$ is:

[TABLE]

A12.11. Proof of Judgment (21), (22), (23) and (24)

In this subsection, we verify the correctness and security of quantum one-time pad. The proof outlines for judgments (21), (22), (23) and (24) are shown in Figs. 16, 17, 18 and 19, respectively.

It is worth noting that the initializations of registers $a$ (or $a_{i}$) and $b$ (or $b_{i}$) are regarded as the creation of new local qubits, so the rules (SO-L) / (SO) are used instead of (Init-L) / (Init). All the calculations are straightforward, except the following equation:

[TABLE]

for all possible pure state $|\psi\rangle\in\mathcal{H}_{\bar{p}}$. This fact has already been proved in (Mosca et al., 2000) (see Theorem 4.1 there) if we realize the relationship between Pauli matrices $ZX=-iY$.

A12.12. Proof of Proposition 7.1

Proof.

(1) If $\models P_{1}\sim P_{2}:A\Rightarrow B$, then for any input $\rho\in A$, there exists a coupling $\sigma$ for $\left\langle\llbracket P_{1}\rrbracket({\mathrm{tr}}_{2}(\rho)),\llbracket P_{2}\rrbracket({\mathrm{tr}}_{2}(\rho))\right\rangle$ such that

[TABLE]

which implies ${\mathrm{tr}}(B\sigma)={\mathrm{tr}}(\sigma)$, or equivalently, $\sigma\in B$. Therefore, $\models_{P}P_{1}\sim P_{2}:A\Rightarrow B$.

(2) We show a counterexample here. Let us consider a qubit $q$ and two programs $P_{1}$ and $P_{2}$

[TABLE]

and choose projective predicates $A=B=|\Psi\rangle\langle\Psi|$ where $|\Psi\rangle$ is the maximally entangled state $\frac{1}{\sqrt{2}}(|00\rangle+|11\rangle)$.

If $\rho\in A$, then $\rho=\lambda|\Psi\rangle$ for some real number $0\leq\lambda\leq 1$. Consequently,

[TABLE]

and $\llbracket P_{1}\rrbracket({\mathrm{tr}}_{2}(\rho))=\frac{\lambda}{2}I$. Therefore, $\rho$ is still a coupling of $\left\langle\llbracket P_{1}\rrbracket,({\mathrm{tr}}_{2}(\rho)),\llbracket P_{2}\rrbracket({\mathrm{tr}}_{2}(\rho))\right\rangle$, which shows that

[TABLE]

On the other hand, if we choose a separable input $\rho=|00\rangle\langle 00|$, then the output of two programs are $\llbracket P_{1}\rrbracket({\mathrm{tr}}_{2}(\rho))=|1\rangle\langle 1|$ and $\llbracket P_{2}\rrbracket({\mathrm{tr}}_{2}(\rho))=|0\rangle\langle 0|$. They have a unique coupling $\sigma=|10\rangle\langle 10|$. However,

[TABLE]

which rules out that $\models P_{1}\sim P_{2}:A\Rightarrow B$. ∎

A12.13. Proof of Proposition 7.2

Proof.

The validity of axioms (Skip-P), (UT-P) and rules (SC-P), (Conseq-P) and (Equiv) are trivial. We only show the validity of rules in Figure 10 together with (Frame-P) here.

$\bullet$ (SO-P) As shown in the proof of Lemma A12.1, for any inputs $\rho_{1}\in{\mathcal{D}}^{\leq}(\mathcal{H}_{P_{1}\langle 1\rangle})$ and $\rho_{2}\in{\mathcal{D}}^{\leq}(\mathcal{H}_{P_{2}\langle 2\rangle})$ with a witness $\rho$ of the lifting $\rho_{1}A^{\#}\rho_{2}$, then $({\mathcal{E}}_{1}\otimes{\mathcal{E}}_{2})(\rho)$ is a coupling for

[TABLE]

Moreover, as ${\rm supp}(\rho)\subseteq A$, then trivially

[TABLE]

which implies the validity of (SO-P).

$\bullet$ (Init-P), (Init-P-L) and (SO-P-L) Special cases of (SO-P).

$\bullet$ (IF-P) From the first assumptions we know that, for any $\rho_{1}\in{\mathcal{D}}^{\leq}(\mathcal{H}_{P_{1}\langle 1\rangle})$ and $\rho_{2}\in{\mathcal{D}}^{\leq}(\mathcal{H}_{P_{2}\langle 2\rangle})$ such that $\rho_{1}A^{\#}\rho_{2}$, there exists a sequence of lifting of $B_{m}$ relating the post-measurement states with the same outcomes; that is, for all $m$,

[TABLE]

Together with the second assumption, we must have:

[TABLE]

Due to the linearity of partial trace, we conclude that

[TABLE]

or equivalently,

[TABLE]

$\bullet$ (IF-P-L) Similar to (IF-P).

$\bullet$ (LP-P) We first introduce an auxiliary notation: for $i=1,2$, quantum operation $\mathcal{E}_{i0}$ and $\mathcal{E}_{i1}$ are defined by the measurement ${\mathcal{M}}_{i}$

[TABLE]

For any $\rho_{1}\in{\mathcal{D}}^{\leq}(\mathcal{H}_{P_{1}\langle 1\rangle})$ and $\rho_{2}\in{\mathcal{D}}^{\leq}(\mathcal{H}_{P_{2}\langle 2\rangle})$ such that $\rho_{1}A^{\#}\rho_{2}$, we claim that for all $n\geq 0$, the following statement holds:

[TABLE]

We prove it by induction on $n$. For $n=0$, $\rho_{1}A^{\#}\rho_{2}$ is already assumed. The first assumption of measurement ensures that

[TABLE]

or in other words, ${\mathcal{E}}_{10}(\rho_{1})B_{0}^{\#}{\mathcal{E}}_{20}(\rho_{2})$. Suppose the statement holds for $n=k$. Then for $n=k+1$, because

[TABLE]

the assumption of measurement implies that

[TABLE]

and followed by the second assumption $\models_{P}P_{1}\sim P_{2}:B_{1}\Rightarrow A$, we have

[TABLE]

or equivalently

[TABLE]

Applying the assumption of measurement on the above formula, it is trivial that

[TABLE]

and this complete the proof the statement.

Now, suppose that the witness of the lifting

[TABLE]

is $\sigma_{n}$ for all $n\geq 0$. We set $\sigma=\sum_{n}\sigma_{n}$ whose convergence is guaranteed by

[TABLE]

Then, it is straightforward to show that $\sigma$ is a coupling of

[TABLE]

and ${\rm supp}(\sigma)\subseteq B_{0}$.

$\bullet$ (LP-P-L) Similar to (LP-P).

$\bullet$ (Frame-P) Suppose $V=V_{1}\cup V_{2}$ where $V_{1}$ represents the extended variables of $P_{1}$ and $V_{2}$ of $P_{2}$. Of course, $V_{1}\cap V_{2}=\emptyset$ and $\mathcal{H}_{V}=\mathcal{H}_{V_{1}}\otimes\mathcal{H}_{V_{2}}$. We prove:

[TABLE]

that is, for any separable state $\rho$ between $\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}}$ and $\mathcal{H}_{V}$ satisfies ${\rm supp}(\rho)\subseteq A\otimes C$,

[TABLE]

First of all, by separability of $\rho$, we can write:

[TABLE]

where $\rho_{i}\in\mathcal{D}^{\leq}(\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{P_{2}})$, $\sigma_{i}\in\mathcal{D}^{\leq}(\mathcal{H}_{V})$ and $p_{i}>0$. Since $V\cap\mathrm{var}(P_{1},P_{2})=\emptyset$, it holds that

[TABLE]

As ${\rm supp}(\rho)\subseteq A\otimes C$, so for all $i$, ${\rm supp}(\rho_{i})\subseteq A$ and ${\rm supp}(\sigma_{i})\subseteq C$. For each $i$, since $\models_{P}P_{1}\sim P_{2}:A\Rightarrow B$, then

[TABLE]

and we assume $\rho_{i}^{\prime}$ is a witness.

We set:

[TABLE]

Then we can check that

[TABLE]

and ${\mathrm{tr}}_{\langle 1\rangle}(\rho^{\prime})=\llbracket P_{2}\rrbracket({\mathrm{tr}}_{\mathcal{H}_{P_{1}}\otimes\mathcal{H}_{V_{1}}}(\rho))$. Therefore, $\rho^{\prime}$ is a coupling for

[TABLE]

Furthermore, as ${\rm supp}(\rho_{i}^{\prime})\subseteq B$ and ${\rm supp}(\sigma_{i})\subseteq C$, we conclude that ${\rm supp}(\rho^{\prime})\subseteq B\otimes C$. ∎

A12.14. Verification of Judgment (29)

In this subsection, we verify the equivalence of two quantum random walkers with different coin-tossing operators. The formal proof is displayed in Figure 20 together with two extra notations:

[TABLE]

The use of (SO-P) for the last line of the program is obvious:

[TABLE]

For the ${\bf if}$ sentence, we first show that the following assertion holds:

[TABLE]

where $F_{1}=F_{2}=\cdots=F_{n-1}=0$ and

[TABLE]

It is not difficult to realize that, for any

[TABLE]

it must have following properties:

[TABLE]

The second property ensures that for $i=1,2,\cdots,n-1$,

[TABLE]

or equivalently to say

[TABLE]

as $F_{i}=0$. Moreover, for $i=0,n$, we note that

[TABLE]

where $\rho_{1,c,i},\rho_{2,c,i}\in\mathcal{D}^{\leq}(\mathcal{H}_{c})$, which implies

[TABLE]

or equivalently

[TABLE]

Therefore, assertion (43) holds.

As $F_{i}\sqsubseteq D$ for all $i$, using rules (Skip-P) and (Conseq-P), we have:

[TABLE]

Note that all subprograms of $\bf{if}$ statement are ${\bf skip}$, and therefore with the precondition $B_{0}$, the precondition $D$ of the $\bf{if}$ statement is valid using rule (IF-P) directly according to assertions (43) and (44).

Now, we focus on the proof of $C\sqsubseteq A$. For simplicity, we use bold ${\bm{i}}$ to denote the imaginary unit, that is $\bm{i}=(-1)^{\frac{1}{2}}$. First of all, the following equations are trivial:

[TABLE]

Secondly, we can calculate $C$ directly from the above equations:

[TABLE]

Next, we show that $C$ is invariant under the premultiplication of $U_{c^{\prime},p^{\prime}}S_{c,p;c^{\prime},p^{\prime}}U^{\dagger}_{c^{\prime},p^{\prime}}$:

[TABLE]

Finally, let calculate $AC$:

[TABLE]

which implies that $C\sqsubseteq A$, as both $A$ and $C$ are projectors.

What remains to be shown is:

[TABLE]

Actually, this one is not difficult to realize as measurement $\mathcal{M}$ and $U$ are commutative, that is, $M_{i}U=UM_{i}$ for $i=0,1$. Therefore, for any $\rho\in A=U_{c^{\prime},p^{\prime}}(=_{sym})U^{\dagger}_{c^{\prime},p^{\prime}}$,

[TABLE]

Moreover, realize that

[TABLE]

so

[TABLE]

which implies that

[TABLE]

Similarly, we have:

[TABLE]

Combining the above fact $C\sqsubseteq A$ and Eqn. (45), we conclude that with precondition $A$, the postcondition $B_{0}$ of the while loop is valid.

A12.15. Proof of Proposition A15.1

Let us first present a technical lemma:

Lemma A12.4.

Suppose $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$ are both two dimensional Hilbert spaces and $|\Phi\rangle$ is a maximally entangled state between $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$. Then for any separable state $\rho$ between $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$,

[TABLE]

Proof.

Suppose $|\Phi\rangle=\frac{1}{\sqrt{2}}(|00\rangle+|11\rangle)$ and write $\rho$ and $\rho^{T_{2}}$ in the matrix forms:

[TABLE]

with non-negative real numbers $x,y,z,w$ and complex number $v$ while ‘$\cdot$’ represents the parameters we are not interested in. As $\rho$ is separable, so $\rho^{T_{2}}$ is non-negative which implies $yz\geq vv^{*}$. Therefore, we obtain:

[TABLE]

∎

Now we are ready to prove Proposition A15.1.

Proof.

(i) It is sufficient to use the same counterexample shown in the proof of Proposition 7.1 (2) [see Appendix A12.12] to prove this. Actually, that example not only rules out $\models P_{1}\sim P_{2}:A\Rightarrow B$, but also $\models_{S}P_{1}\sim P_{2}:A\Rightarrow B$ (see Definition A15.1).

(ii) Let us still consider two one-qubit programs

[TABLE]

and two projective predicate $A=B=|\Psi\rangle\langle\Psi|$. According to Lemma A12.4 we know that for any separable state $\rho$ between $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$, ${\mathrm{tr}}(A\rho)\leq\frac{1}{2}{\mathrm{tr}}(\rho)$. The output states of two programs are both ${\mathrm{tr}}(\rho)|0\rangle\langle 0|$, which have the unique coupling $\sigma={\mathrm{tr}}(\rho)|00\rangle\langle 00|$, therefore,

[TABLE]

which concludes the validity of $\models_{S}P_{1}\sim P_{2}:A\Rightarrow B$.

On the other hand, choosing $\rho=|\Psi\rangle\langle\Psi|\in A$ as the input, the coupling $\sigma$ of outputs is still unique and $\sigma=|00\rangle\langle 00|$, whose support is not in $B$; that is, $\models_{p}P_{1}\sim P_{2}:A\Rightarrow B$ is not valid.

(iii) Obvious.

(iv) Let us consider two one-qubit programs

[TABLE]

with their two-dimensional Hilbert space $\mathcal{H}_{1}$ and $\mathcal{H}_{2}$ respectively, and the separable quantum predicates

[TABLE]

and $B=\frac{2}{3}I\otimes I$ over $\mathcal{H}_{1}\otimes\mathcal{H}_{2}$ where $|\Psi\rangle$ is the maximally entangled state $\frac{1}{\sqrt{2}}(|00\rangle+|11\rangle)$.

$B$ is trivially separable and the separability of $A$ is already shown in the proof of Fact A12.1 [see Appendix 3.3]. Now, it is straightforward to see that for any separable input $\rho$ the following inequality holds:

[TABLE]

according to Fact A12.4. Note that $P_{1}$ and $P_{2}$ are $\mathbf{skip}$, so $\rho$ is still a coupling for $\left\langle\llbracket P_{1}\rrbracket({\mathrm{tr}}_{2}(\rho)),\llbracket P_{2}\rrbracket({\mathrm{tr}}_{1}(\rho))\right\rangle$, which implies the validity of the judgment $\models_{S}P_{1}\sim P_{2}:A\Rightarrow B$.

On the other hand, however, if we choose $|\Psi\rangle\langle\Psi|$ as the input, then

[TABLE]

for any possible couplings $\sigma$ for the output states, which rules out the validity of judgment $\models P_{1}\sim P_{2}:A\Rightarrow B$. ∎

A13. A Strategy for Collecting Measurement and Separability Conditions

In this section, we propose a strategy for collecting measurement and separability conditions in order to warrant the side-conditions of the form (10) in a sequence of applications of the strong sequential rule (SC+). Separability conditions are relatively easier to deal with. So, we focus on measurement conditions.

We first observe that for each quantum program containing if and while, it naturally includes branches in execution. We can generate a (potentially) infinite probabilistic branching tree for any input state as follows:

• •

$({\rm IF})\ \langle\mathbf{if}\ (\square m\cdot{\mathcal{M}}[\overline{q}]=m\rightarrow P_{m})$ is executed with input $\rho$. The current node has $M$ children nodes, where $M$ is the number of possible outcomes $m$ of the measurement $\mathcal{M}$, such that the edge connected to the $m$-th child has probability weight ${\mathrm{tr}}(M_{m}^{{\dagger}}M_{m}\rho)$.

• •

$\mathbf{while}\ {\mathcal{M}}[\overline{q}]=1\ \mathbf{do}\ P\ \mathbf{od}$ is executed with input $\rho$. The current node has two children nodes such that the edge connected to the $i$-th child has probability weight ${\mathrm{tr}}(M_{i}^{{\dagger}}M_{i}\rho)$ $(i=0,1)$. The second node then will have two children nodes such that the edge connected to the $i$-th child has probability weight ${\mathrm{tr}}(M_{i}^{{\dagger}}M_{i}P(M_{1}\rho M_{1}^{{\dagger}}))$. $\cdots$. Repeating this process, each while loop would generate an infinite probabilistic branching tree.

Now we can define comparability between two quantum programs.

Definition A13.1.

Let $P_{1}$ and $P_{2}$ be two quantum programs and $\rho_{1}$ and $\rho_{2}$ two input states. We say that $(P_{1},\rho_{1})$ and $(P_{2},\rho_{2})$ are comparable, if the probabilistic branching tree generated from $P_{1}$ executing on $\rho_{1}$ is the same as the probabilistic branching tree generated from $P_{2}$ executing on $\rho_{2}$.

The measurement conditions used in verifying relational properties between two programs $P_{1}$ and $P_{2}$ are actually the constraints on the respective inputs $\rho_{1},\rho_{2}$ under which $(P_{1},\rho_{1})$ and $(P_{2},\rho_{2})$ are comparable.

Although the probabilistic branching trees of $P_{1}$ and $P_{2}$ are generally infinite, we have a back tracking procedure to find sufficient constrains for comparability of them in the case of finite-dimensional state Hilbert spaces.

Lemma A13.1.

For any two programs $P_{1}$ and $P_{2}$ in finite-dimensional Hilbert spaces, we can compute the constrains on inputs under which they become comparable within a finite number of steps.

Proof.

We show find linear constrains by back tracking through the structure of programs $P_{,}P_{2}$:

• •

At the output points, the constrains are $\{(I,I)\}$, which means that the output probability should be the same.

• •

Now suppose that at some point, the constrains are $\{(A_{1},B_{1}),\cdots,(A_{k},B_{k})\}$, which means that the respective inputs $\rho_{1},\rho_{2}$ at this point should satisfy ${\mathrm{tr}}(A_{i}\rho_{1})={\mathrm{tr}}(B_{i}\rho_{2})$ to make the following subprogram generate same probabilistic branching trees. Such constrains are also considered as the requirements of the outputs of the front subprograms.

Our aim is to generate the constrains for the point before the current one. We only illustrate the following two cases:

• –

The subprograms of $P_{1}$ and $P_{2}$ associated with this point are:

[TABLE]

Then the following equations should be added into the constraints:

${\mathrm{tr}}(M_{i}^{{\dagger}}M_{i}\rho_{1})={\mathrm{tr}}(N_{i}^{{\dagger}}N_{i}\rho_{2})$ for $1\leq i\leq m$.

• *

${\mathrm{tr}}(\sum_{i=1}^{m}P_{i}(M_{i}\rho_{1}M_{i}^{{\dagger}})A_{j})=(\sum_{i=1}^{m}P_{i}(M_{i}\rho_{1}M_{i}^{{\dagger}})B_{j})$ for all $1\leq j\leq k$.

It is easy to derive new constrains for the input at the points of ${\rm IF_{1}}$ and ${\rm IF_{2}}$.

• –

The subprograms of $P_{1}$ and $P_{2}$ associated with this point are:

[TABLE]

Assume that the semantic functions of $P$ and $Q$ are super-operators ${\mathcal{E}}$ and ${\mathcal{F}}$, respectively. We set ${\mathcal{E}}_{a}={\mathcal{E}}\circ M_{1}\cdot M_{1}^{{\dagger}}$ and ${\mathcal{F}}_{a}={\mathcal{F}}\circ N_{1}\cdot N_{1}^{{\dagger}}$ Then the following equations should be added into the constrains: for each $1\leq j$,

${\mathrm{tr}}(M_{0}{\mathcal{E}}_{a}^{j}(\rho_{1})M_{0}^{{\dagger}})={\mathrm{tr}}(N_{0}{\mathcal{F}}_{a}^{j}\rho_{2}N_{0}^{{\dagger}})$ for $1\leq i\leq m$.

• *

${\mathrm{tr}}(M_{0}{\mathcal{E}}_{a}^{j}(\rho_{1})M_{0}^{{\dagger}}A_{i})=(N_{0}{\mathcal{F}}_{a}^{j}\rho_{2}N_{0}^{{\dagger}}B_{j})$ for all $1\leq i\leq k$.

Note that the second requirement is very strong in the sense that rather than only requiring the outputs of the loops satisfies the latter constrains, we want each branch of them satisfies the latter constrains. This is reasonable because different branches of the loops can actually happen in different points of time.

The key idea here is that although the above procedure may produce infinitely many constrains, a finite number of them will be enough to ensure that all of them are satisfied. Indeed, we can see that $d_{a}^{2}+d_{b}^{2}+1$ of these constraints are enough by observing that the equations given above can be regarded as linear constrains of linear recurrent series of degree $d_{a}^{2}+d_{b}^{2}$. It is well known that a $d$-degree linear recurrent series is [math] if and only if the front $d+1$ items are all [math]. ∎

For a better understanding of the procedure given in the proof of the above lemma, it is visualised as Algorithm 1.

A14. Comparison between Unruh’s Logic and Ours

Expressiveness

One main consideration in (Unruh, 2019b) is to retain the intuitive flavour of proofs in probabilistic relational Hoare logic and to give an implementation in a general-purpose proof assistant. Thus, (Unruh, 2019b) only considers projective predicates as pre-conditions and post-conditions. As already noted in Section 7, this restriction can simplify the verification of quantum programs, but also limits the expressiveness of the logic. In particular, we believe that our main examples cannot be dealt with by Unruh’s logic (Unruh, 2019b): The symmetry in Example 1.1, the uniformity in Proposition 6.1, Quantum Bernoulli Factory (Example 6.1) and the reliability of quantum teleportation (Section 6.3.2) cannot be specified in that logic because the preconditions in judgments (12), (14) and (18-20) are not projective (i.e. the projection onto a (closed) subspace of the state Hilbert space). In addition, (Unruh, 2019b) introduces classic variables and Boolean predicates into programming language and logic, which significantly enhances the expressiveness and practicability. However, introducing classic elements does not bring about a deeper understanding of the relationship between quantum programs while makes the logic itself much more complicated.

Later on, (Li and Unruh, 2019) also considers general observables as predicates and remove all classical variables. Its expressiveness is the same as ours, but the proof rules are different (see discussion below).

Inference Rules

(Unruh, 2019b)** vs. rqPD (Section 7)**: Since (Unruh, 2019b) introduces classical variables, the proof rules are quite different from ours. Here we mainly focus on the difference between if and while rules. We believe that Unruh’s proof rules JointMeasure together with JointIf and JointWhile for reasoning about if and while statements with quantum measurements as guards is weaker than our rules (IF-P) and (LP-P). The reasons are given as follows.

The guards in if and while statements considered in (Unruh, 2019b) are boolean expressions while measure statement is introduced to extract information from quantum registers. Our if and while statements (with quantum measurements as guards) can be regarded as a combination of measure and if, while statements in (Unruh, 2019b). Note that the rule JointMeasure (see the arXiv version (Unruh, 2018); which is the general form of rule JointMeasureSimple discussed in the conference version (Unruh, 2019b)) is quite restrictive; more precisely, the preconditions must satisfy: 1. Two measurements can be converted through isometries $u_{1}$, $u_{2}$ (expressed as condition $C_{e}$); 2. The states over the measured quantum registers need to be equal up to the basis transforms $u_{1}$ and $u_{2}$ (expressed as condition $u_{1}Q_{1}^{\prime}\equiv_{\textsf{quant}}u_{2}Q_{2}^{\prime}$). Such preconditions are significantly stronger than the preconditions given in our (IF-P) and (LP-P) rules. In fact, we only need to ensure that two measurements produces the same output distribution if two measured states can be lifted to the precondition (see Definition 7.2).

It is worth mentioning that, Unruh’s definition of the valid judgments requires that the coupling of inputs and outputs must be separable, so Frame rule holds directly. In contrast, our definition of validity allows the entangled couplings, so a separability condition is added to our (Frame) rule. In addition, there is no (Frame) rule in (Li and Unruh, 2019).

(Li and Unruh, 2019)** vs. rqPD (Section 5)**: The inference rules in (Li and Unruh, 2019) are just those basic construct-specific rules presented in Section 5.2. However, the proof of soundness is somewhat different because of the difference between the definitions of valid judgments. Moreover, we present more rules using measurement condition (see Fig. 6), which enable us to capture more relational properties between quantum programs. For instance, although the symmetry in Example 1.1 and the uniformity of Quantum Bernoulli Factory (Example 6.1) can be expressed in (Li and Unruh, 2019), their rules are not strong enough for reasoning about these judgments. In opposite, the example of Quantum Zeno Effect used in (Li and Unruh, 2019) can also be verified using our logic.

Complexity

One of the major differences between our logic and Unruh’s one [Unruh, 2019b; Li and Unruh, 2019] comes from the treatment of entanglement in relational judgments:

1. (1)

Our definition of valid judgment $P_{1}\sim P_{2}:A\Rightarrow B$ quantifies over all inputs in $\mathcal{H}_{P_{1}\langle 1\rangle}\otimes\mathcal{H}_{P_{2}\langle 2\rangle}$ including entanglements between $P_{1}$ and $P_{2}$. In contrast, Unruh [Unruh, 2019b; Li and Unruh, 2019] only allows separable inputs between $P_{1}$ and $P_{2}$. 2. (2)

Unruh [Unruh, 2019b; Li and Unruh, 2019] also requires that couplings for the outputs of programs $P_{1}$ and $P_{2}$ must be separable. This is not required in our logic.

The above differences render essentially different complexities of checking the validity of a given judgment in applications. It is known that deciding the separability of a given quantum state is NP-hard with respect to the dimension (Gurvits, 2003; Gharibian, 2010); thus, we believe that deciding the existence of separable couplings in some subspaces is also NP-hard. If so, this will prevent the possibility of efficiently automatically checking validity defined in [Unruh, 2019b; Li and Unruh, 2019] even if the semantic function is known. However, quantum Strassen theorem proved in the previous work (Zhou et al., 2019a) implies that it has only a polynomial time complexity with respect to the dimension to deciding the existence of couplings used in our projective judgments. With the same techniques of SDP (semi-definite programming), the validity of general judgment can also check within polynomial time with respect to the dimension.

A15. Validity of Judgments: Separability versus Entanglements

In this subsection, we will explore more details between separability and entanglements. Let us first consider item (1). Intuitively, in our logic, to test the relationship between $P_{1}$ and $P_{2}$, we run them in parallel within an environment where entanglement between the two parties are allowed. However, in Unruh’s logic, such an entanglement is not provided in the experiment. As one can imagine, our logic can be used to reveal some subtler relational properties of quantum programs. To see this formally, let us introduce the notion of validity with separable inputs (but not necessarily with separable coupling for outputs) for general Hermitian operators (rather than projective ones) as the preconditions and postconditions.

Definition A15.1.

Judgment (4) is valid with separable inputs, written:

[TABLE]

if it is valid under separability condition $\Gamma=[\mathit{var}(P_{1}\langle 1\rangle),\mathit{var}(P_{2}\langle 2\rangle)]$; that is,

[TABLE]

The relationship between the general validity $\models$, projective validity $\models_{P}$ and validity $\models_{S}$ with separable inputs is clarified in the following:

Proposition A15.1.

For projective predicates $A$ and $B$:

[TABLE]

and for general quantum predicates $A$ and $B$,

[TABLE]

Clauses (ii) and (iv) clearly indicate that our intuition is correct; that is, a judgment with entangled inputs is strictly stronger than the same judgment with separable inputs.

Now let us turn to items (2). It was clearly pointed out in (Unruh, 2019b) that the first try there is to define validity of judgments without the requirement of separable couplings for the outputs of $P_{1}$ and $P_{2}$. But separability for the couplings for outputs was finally imposed to the definition of validity of judgments in (Unruh, 2019b). A nice benefit is that the rule (SC) for sequential composition can be easily achieved for such a notion of validity. Our design decision for preserving rule (SC) is to allow entanglement occurring in both inputs and the couplings for outputs. A benefit of our definition is that the entanglement in these couplings enables us to reveal subtler relational properties between quantum programs. To be more precise, let us consider two lossless programs $P_{1},P_{2}$ and judgment $P_{1}\sim P_{2}:A\Rightarrow B$. For an (even separable) $\rho$, let $\lambda={\mathrm{tr}}(A\rho)$, then Proposition 3.3 shows that there can be an entangled witness for $\lambda$-lifting $\llbracket P_{1}\rrbracket({\mathrm{tr}}_{\langle 2\rangle}(\rho))B^{\#}\llbracket P_{2}\rrbracket({\mathrm{tr}}_{\langle 1\rangle}(\rho))$. Indeed, it is the case even for separable postcondition $B$.

Inference Rules

Of course, different definitions of valid judgments imply different inference rules in our logic and Unruh’s one. We already said that without the separability requirement on the couplings for outputs, rule (SC) is not true for validity $\models_{S}$ with separable inputs. A series of inference rules are derived in (Unruh, 2019b) by imposing the separability requirement on the couplings for outputs. Here, we would like to point out how this difficulty can be partially solved without this separability. Indeed, a weaker version of (SC), namely (SC-Sep) shown in Figure 21, can be obtained by combining $\models_{S}$ with our general validity $\models$. Furthermore, other inference rules in our rqPD are sound for $\models_{S}$ except that the rule (Frame) should be slightly modified to (Frame-Sep) in Figure 21.