→$\to$ ⊗$\otimes$ ×$\times$ ∩$\cap$ ⊤$\top$ ⊥$\bot$

# Gottesman Types for Quantum Programs

Robert Rand University of Chicago<EMAIL_ADDRESS>Microsoft
QuantumUniversity of ChicagoMicrosoft QuantumUniversity of Maryland Aarthi
Sundaram Microsoft Quantum<EMAIL_ADDRESS>University of ChicagoMicrosoft
QuantumUniversity of Maryland Kartik Singhal University of Chicago
<EMAIL_ADDRESS>Microsoft QuantumUniversity of Maryland Brad Lackey
Microsoft QuantumUniversity of Maryland<EMAIL_ADDRESS>
###### Abstract

The Heisenberg representation of quantum operators provides a powerful
technique for reasoning about quantum circuits, albeit those restricted to the
common (non-universal) Clifford set $H$, $S$ and $CNOT$. The Gottesman-Knill
theorem showed that we can use this representation to efficiently simulate
Clifford circuits. We show that Gottesman’s semantics for quantum programs can
be treated as a type system, allowing us to efficiently characterize a common
subset of quantum programs. We also show that it can be extended beyond the
Clifford set to partially characterize a broad range of programs. We apply
these types to reason about separable states and the superdense coding
algorithm.

##  1 Introduction

The _Heisenberg representation_ of quantum mechanics treats quantum operators
as functions on unitary matrices, rather than on the quantum state. For
instance, for any quantum state $\ket{\phi}$,

$HZ\ket{\phi}=XH\ket{\phi}$ (1)

so an $H$ gate can be viewed as a higher-order function that takes $Z$ to $X$
(and similarly takes $X$ to $Z$). Gottesman [8] uses this representation to
present the rules for how the Clifford quantum gates $H$, $S$ and $CNOT$
operate on Pauli $X$ and $Z$ gates, which is sufficient to fully describe the
behavior of the Clifford operators. There, H is given the following
description based on its action above:

$H:\mathbf{Z}\to\mathbf{X}\qquad H:\mathbf{X}\to\mathbf{Z}$

In Gottesman’s paper, the end goal is to fully describe quantum programs and
prove the _Gottesman-Knill theorem_ , which shows that any Clifford circuit
can be simulated efficiently. Here we observe that the judgements above look
like typing judgments, and show that they can indeed be treated as such
(section 3). As such, they can be used to make coarse guarantees about
programs, without fully describing the programs’ behaviors. We show a simple
example of applying this system to the superdense coding algorithm (section
5). In section 6, we demonstrate, using the GHZ state $\ket{000}+\ket{111}$,
how the type system is capable of tracking both the creation and destruction
of entanglement. In section 7, we extend the type system to deal with programs
outside the Clifford group and use it to characterize the Toffoli gate. We
discuss the possible future applications of this system in section 8.

The system and examples in this paper are formalized in Coq at
https://github.com/inQWIRE/GottesmanTypes.

##  2 Gottesman Semantics

Gottesman’s semantics for $H$, $S$, and $CNOT$ are given by the following
table.

$\begin{array}[]{rlcrl}H:&\mathbf{X}\rightarrow\mathbf{Z}&&CNOT:&\mathbf{X}\otimes\mathbf{I}\rightarrow\mathbf{X}\otimes\mathbf{X}\\\
H:&\mathbf{Z}\rightarrow\mathbf{X}&&CNOT:&\mathbf{I}\otimes\mathbf{X}\rightarrow\mathbf{I}\otimes\mathbf{X}\\\
S:&\mathbf{X}\rightarrow\mathbf{Y}&&CNOT:&\mathbf{Z}\otimes\mathbf{I}\rightarrow\mathbf{Z}\otimes\mathbf{I}\\\
S:&\mathbf{Z}\rightarrow\mathbf{Z}&&CNOT:&\mathbf{I}\otimes\mathbf{Z}\rightarrow\mathbf{Z}\otimes\mathbf{Z}\end{array}$

Note that these rules are intended to simply describe the action of each gate
on the corresponding unitary matrices, as in equation 1. However, given the
action of a circuit on every permutation of $X$ and $Z$ (or any spanning set)
we can deduce the semantics of the program itself [8].111The intuition behind
this comes from the fact that this set of $X$ and $Z$ operators form the
generators of the Pauli basis for quantum states. Hence, deducing the action
of a unitary matrix on them provides an information theoretically complete
picture of the action of the matrix on any input and suffices to deduce the
semantics of the program. For our purposes, though, we will treat these as a
type system, justifying that choice in section 3.

We can combine our typing rules by simple multiplication, for instance
combining the second and third rules for $CNOT$, we get

$CNOT:(\mathbf{I}\mathbf{Z}\otimes\mathbf{X}\mathbf{I}\rightarrow\mathbf{I}\mathbf{Z}\otimes\mathbf{X}\mathbf{I})=\mathbf{Z}\otimes\mathbf{X}\rightarrow\mathbf{Z}\otimes\mathbf{X}$

In the rule for $S$, $\mathbf{Y}$ is equivalent to $i\mathbf{X}\mathbf{Z}$ so
we can reason about an $S$ applied twice compositionally. We use
$f\mathrel{\$}g$ for forward function composition (equivalent to $g\circ f$):

$S;S:(\mathbf{X}\to i\mathbf{X}\mathbf{Z}\mathrel{\$}i\mathbf{X}\mathbf{Z}\to
i\mathbf{Y}\mathbf{Z})=\mathbf{X}\to-\mathbf{X}$

Once we have a type system for $H$, $S$ and $CNOT$ we can define additional
gates in terms of these, and derive their types. For instance, the Pauli $Z$
gate is simply $S;S$, for which we derived the following type for $\mathbf{X}$
and trivially can derive the type for $\mathbf{Z}$:

$\displaystyle Z:~{}$ $\displaystyle\mathbf{X}\rightarrow-\mathbf{X}$
$\displaystyle Z:~{}$ $\displaystyle\mathbf{Z}\rightarrow\mathbf{Z}$

Defining $X$ as $H;Z;H$, we can derive the type for the Pauli $X$ gate as:

$\displaystyle X=H;Z;H:~{}$
$\displaystyle(\mathbf{X}\to\mathbf{Z}\mathrel{\$}\mathbf{Z}\to\mathbf{Z}\mathrel{\$}\mathbf{Z}\to\mathbf{X})=\mathbf{X}\rightarrow\mathbf{X}$
$\displaystyle X=H;Z;H:~{}$
$\displaystyle(\mathbf{Z}\rightarrow\mathbf{X}\mathrel{\$}\mathbf{X}\rightarrow-\mathbf{X}\mathrel{\$}-\mathbf{X}\rightarrow-\mathbf{Z})=\mathbf{Z}\rightarrow-\mathbf{Z}$

Likewise, $Y=S;X;Z;S$ and so, the type for the Pauli $Y$ gate would be:

$\displaystyle Y=S;Z;X;S:~{}$
$\displaystyle(\mathbf{Z}\rightarrow\mathbf{Z}\mathrel{\$}\mathbf{Z}\rightarrow\mathbf{Z}\mathrel{\$}\mathbf{Z}\rightarrow-\mathbf{Z}\mathrel{\$}-\mathbf{Z}\rightarrow-\mathbf{Z})=\mathbf{Z}\rightarrow-\mathbf{Z}$
$\displaystyle Y=S;Z;X;S:~{}$
$\displaystyle(\mathbf{X}\rightarrow\mathbf{Y}\mathrel{\$}\mathbf{Y}\rightarrow-\mathbf{Y}\mathrel{\$}-\mathbf{Y}\rightarrow\mathbf{Y}\mathrel{\$}\mathbf{Y}\rightarrow-\mathbf{X})=\mathbf{X}\rightarrow-\mathbf{X}$

We can also define more complicated gates like $CZ$ and $SWAP$ as
$H_{\\_}2;CNOT;H_{\\_}2$ (where $H_{\\_}2$ is $H$ applid to $CNOT$’s target
qubit) and $CNOT;NOTC;CNOT$, (where $NOTC$ is a flipped $CNOT$) for which we
can easily derive the following types:

$\begin{array}[]{rlrl}CZ:&\mathbf{X}\otimes\mathbf{I}\rightarrow\mathbf{X}\otimes\mathbf{Z}&\quad
SWAP:&\mathbf{X}\otimes\mathbf{I}\rightarrow\mathbf{I}\otimes\mathbf{X}\\\
CZ:&\mathbf{I}\otimes\mathbf{X}\rightarrow\mathbf{Z}\otimes\mathbf{X}&\quad
SWAP:&\mathbf{I}\otimes\mathbf{X}\rightarrow\mathbf{X}\otimes\mathbf{I}\\\
CZ:&\mathbf{Z}\otimes\mathbf{I}\rightarrow\mathbf{Z}\otimes\mathbf{I}&\quad
SWAP:&\mathbf{Z}\otimes\mathbf{I}\rightarrow\mathbf{I}\otimes\mathbf{Z}\\\
CZ:&\mathbf{I}\otimes\mathbf{Z}\rightarrow\mathbf{I}\otimes\mathbf{Z}&\quad
SWAP:&\mathbf{I}\otimes\mathbf{Z}\rightarrow\mathbf{Z}\otimes\mathbf{I}\\\
\end{array}$

By combining the rules stated above, we can also derive the action of $SWAP$
on $\mathbf{X}\otimes\mathbf{Y}$ as:

$SWAP:(\mathbf{X}\otimes\mathbf{Y}=\mathbf{X}\mathbf{I}\mathbf{I}\otimes\mathbf{I}(i\mathbf{X})\mathbf{Z})\rightarrow(\mathbf{I}(i\mathbf{X})\mathbf{Z}\otimes\mathbf{X}\mathbf{I}\mathbf{I}=\mathbf{Y}\otimes\mathbf{X})$

This gives us less information than the types for $SWAP$ above, but might be
the type we intend for a given use of swapping: In particular, we might want
to use a $SWAP$ to exchange qubits in the $X$ and $Y$ bases, as we will show.

We show the full rules for typing circuits in fig. 1, which we will reference
throughout this paper.

  1. 1.

Grammar:

$\displaystyle G:=\mathbf{I}\mid\mathbf{X}\mid\mathbf{Z}\mid-G\mid iG\mid
G*G\mid G\otimes G\mid G\to G\mid G\cap G\mid G\times G\mid\top$

  2. 2.

Multiplication and Tensor Laws:

$\mathbf{X}*\mathbf{X}=\mathbf{I}$ |  $\mathbf{Z}*\mathbf{Z}=\mathbf{I}$ |  $\mathbf{Z}*\mathbf{X}=-\mathbf{X}*\mathbf{Z}$ | $A*\mathbf{I}=A=\mathbf{I}*A$
---|---|---|---
$--A=A$ |  $i(iA)=-A$ |  $i(-A)=-(iA)$ | $A*(B*C)=A*B*C$
$-A*B=-(A*B)=A*-B$ | $iA*B=i(A*B)=A*iB$
$A\otimes(B\otimes C)=(A\otimes B)\otimes C$ | $A\otimes B=(A\otimes\mathbf{I})*(\mathbf{I}\otimes B)$
$iA\otimes B=i(A\otimes B)=A\otimes iB$ | $-A\otimes B=-(A\otimes B)=A\otimes-B$
$\ (A\otimes B)*(C\otimes D)=(A*C)\otimes(B*D)\text{ where
}\absolutevalue{A}=\absolutevalue{C}$

  3. 3.

Tensors Rules:

$\inferrule*[Right=$⊗1$]{g\ 1:A\rightarrow A^{\prime}\absolutevalue{E}=m-1}{g\ m:E\otimes A\otimes E^{\prime}\rightarrow E\otimes A^{\prime}\otimes E^{\prime}}$ |  $\inferrule*[Right=$⊗$-rev]{g\ 2\ 1:A\otimes B\rightarrow A^{\prime}\otimes B^{\prime}}{g\ 1\ 2:B\otimes A\rightarrow B^{\prime}\otimes A^{\prime}}$
---|---
$\inferrule*[Right=$⊗2$]{g\ 1\ 2:A\otimes B\rightarrow A^{\prime}\otimes
B^{\prime}\absolutevalue{E}=m-1\absolutevalue{E^{\prime}}=n-m-1}{g\ m\
n:E\otimes A\otimes E^{\prime}\otimes B\otimes E^{\prime\prime}\rightarrow
E\otimes A^{\prime}\otimes E^{\prime}\otimes B^{\prime}\otimes
E^{\prime\prime}}$

  4. 4.

Arrow and Sequence Rules:

$\inferrule*[Right=mul]{p:A\rightarrow A^{\prime}p:B\rightarrow B^{\prime}}{p:(A*B)\rightarrow(A^{\prime}*B^{\prime})}$ | $\inferrule*[Right=im]{p:A\rightarrow A^{\prime}}{p:iA\rightarrow iA^{\prime}}$
---|---
$\inferrule*[Right=cut]{p_{\\_}1:A\rightarrow Bp_{\\_}2:B\rightarrow C}{p_{\\_}1;p_{\\_}2:A\rightarrow C}$ | $\inferrule*[Right=neg]{p:A\rightarrow A^{\prime}}{p:-A\rightarrow-A^{\prime}}$
$p_{\\_}1;(p_{\\_}2;p_{\\_}3):A\equiv(p_{\\_}1;p_{\\_}2);p_{\\_}3:A$

  5. 5.

Intersection Rules:

$I^{\otimes n}\cap A=A\qquad A\cap A=A\qquad A\cap B=B\cap A\qquad A\cap B\cap C=A\cap(B\cap C)$ $\inferrule*[Right=$∩$-I]{g:Ag:B}{g:A\cap B}$ |  $\inferrule*[Right=$∩$-E]{g:A\cap B}{g:A}$
---|---
$\inferrule*[Right=$∩$-Arr]{g:(A\rightarrow B)\cap(A\rightarrow C)}{g:A\rightarrow(B\cap C)}$ |  $\inferrule*[Right=$∩$-Arr-Dist]{g:(A\rightarrow A^{\prime})\cap(B\rightarrow B^{\prime})}{g:(A\cap B)\rightarrow(A^{\prime}\cap B^{\prime})}$

  6. 6.

Separability Rules

$(A\otimes\mathbf{I}^{n})=A\times\mathbf{I}^{n}\text{ where
}A\in\\{1,-1,i,-i\\}*\\{X,Y,Z\\}$ $(A\times B)\cap(A\otimes C)=A\times(B\cap
C)\qquad(A\times B)\cap(I^{\otimes n}\otimes C)=A\times(B\cap C)$

Figure 1: The grammar and typing rules for Gottesman types. The grammar allows
us to describe ill-formed types, such as
$\mathbf{X}\cap(\mathbf{I}\otimes\mathbf{Z})$, but these don’t type any
circuits. The intersection and arrow typing rules are derived from standard
subtyping rules [17, Chapter 15]. The arity of a type not containing
$\\{\times,\to\\}$ is the longest sequence of atoms connected by tensors. For
instance, $\absolutevalue{\mathbf{I}*\mathbf{Z}\otimes
i\mathbf{X}}=\absolutevalue{(\mathbf{X}\otimes\mathbf{X})\cap(\mathbf{Z}\otimes\mathbf{Z})}=2$.

##  3 Interpretation on Basis States

We can interpret the type $H:\mathbf{Z}\to\mathbf{X}$ as saying that $H$ takes
a qubit in the $\mathbf{Z}$ basis (that is, $\ket{0}$ or $\ket{1}$) to a qubit
in the $\mathbf{X}$ basis ($\ket{+}$ and $\ket{-}$). This form of reasoning is
present in Perdrix’s [16] work on abstract interpretation for quantum systems,
which classifies qubits in an $\mathbf{X}$ or $\mathbf{Z}$ basis, for the
purpose of tracking entanglement. Unfortunately, that system cannot leave the
$\mathbf{X}$ and $\mathbf{Z}$ bases, and hence cannot derive that
$Z:\mathbf{X}\rightarrow-\mathbf{X}$ due to the intermediate $\mathbf{Y}$.
More fundamentally, while we can show that $SWAP$ has type
$\mathbf{X}\otimes\mathbf{Z}\rightarrow\mathbf{Z}\otimes\mathbf{X}$, the first
$CNOT$ application entangles the two qubits (represented in our system by
$\mathbf{X}\mathbf{Z}\otimes\mathbf{X}\mathbf{Z}$) which Perdrix classifies as
simply $\top$ and marks as potentially entangled. (We also use $\top$ but only
for gates that lie outside the set of Clifford operators, see section 7.) As a
result, Perdrix’s system typically classifies most circuits as $\top$ after
just a few gate applications, while ours never leaves the Pauli bases as long
as we apply Clifford gates.

######  Proposition 1.

Given a unitary $U:A\rightarrow B$ in the Heisenberg interpretation, $U$ takes
every eigenstate of $A$ to an eigenstate of $B$.

###### Proof.

From eq. [1] in Gottesman [8], given a state $\ket{\psi}$ and an operator $U$,

$UN\ket{\psi}=UNU^{\dagger}U\ket{\psi}.$

Additionally, in the Heisenberg interpretation this can be denoted as:
$U:N\rightarrow UNU^{\dagger}$. Suppose that $\ket{\psi}$ is an eigenstate of
$N$ with eigenvalue $\lambda$ and let $\ket{\phi}$ denote the state after $U$
acts on $\ket{\psi}$. Then,

$\lambda\ket{\phi}=U(\lambda\ket{\psi})=UN\ket{\psi}=UNU^{\dagger}U\ket{\psi}=(UNU^{\dagger})\ket{\phi}.$

Hence, $\ket{\phi}$ is an eigenstate of the modified operator $UNU^{\dagger}$
with eigenvalue $\lambda$. ∎

#### Intersection Types

It may seem odd that we have given multiple types to $H$, $S$, $CNOT$ and the
various derived operators. This isn’t particularly rare in type systems with
subtyping, which is an appropriate lens for viewing the types we have given
above. However, it is useful to have the most descriptive type for any term in
our language. We can give these using intersection types. For instance, we
have the following types for $H$ and $CNOT$:

$\displaystyle H:$
$\displaystyle(\mathbf{X}\to\mathbf{Z})\cap(\mathbf{Z}\to\mathbf{X})$
$\displaystyle CNOT:$
$\displaystyle(\mathbf{X}\otimes\mathbf{I}\to\mathbf{X}\otimes\mathbf{X})\cap(\mathbf{I}\otimes\mathbf{X}\to\mathbf{I}\otimes\mathbf{X})\cap(\mathbf{Z}\otimes\mathbf{I}\to\mathbf{Z}\otimes\mathbf{I})\cap(\mathbf{I}\otimes\mathbf{Z}\to\mathbf{Z}\otimes\mathbf{Z})$

From these we can derive any of the types given earlier, using the standard
rules for intersections (fig. 1). Another advantage of using intersection
types is that it is closely related to the stabilizer formalism that is used
extensively in error-correction. This connection is further discussed in
section 8.

#### The role of $\mathbf{I}$

$\mathbf{I}$ plays an interesting role in this type system. For $\mathbf{I}$
alone, we have the following two facts, the first drawn from the Heisenberg
representation of quantum mechanics and the second from our interpretation of
types as eigenstates:

$\displaystyle\forall~{}U,\quad U:\mathbf{I}\to\mathbf{I}$ (2)
$\displaystyle\forall~{}\ket{\psi},~{}\ket{\psi}:\mathbf{I}$ (3)

This would lead us to treat $\mathbf{I}$ as a kind of top type, where
$A<:\mathbf{I}$ for any type $A$. However, this would be incompatible with
$\otimes$. For example, the two qubit Bell pair $\ket{\Phi^{+}}$ has type
$\mathbf{X}\otimes\mathbf{X}$ but not type $\mathbf{X}\otimes\mathbf{I}$. By
contrast, $\mathbf{X}\otimes\mathbf{I}$ contains precisely the separable two
qubit states where the first qubit is an eigenstate of $\mathbf{X}$. This
second type, which is neither a subtype nor supertype of the first allows us
to consider the important property of _separability_ or non-entanglement of
qubits.

##  4 Separability

######  Proposition 2.

For any Pauli matrix $U\in\\{-1,1,-i,i\\}*\\{X,Y,Z\\}$, the eigenstates of
$U\otimes I^{\otimes n-1}$ are all the vectors $\ket{u}\otimes\ket{\psi}$
where $\ket{u}$ is an eigenstate of $U$ and $\ket{\psi}$ is any state.

###### Proof.

Let $\ket{\phi}$ be the $\lambda$ eigenstate and $\ket{\phi^{\bot}}$ be the
$-\lambda$ eigenstate for $U\in\\{1,-1,i,-i\\}*\\{X,Y,Z\\}$ where
$\lambda\in\\{1,i\\}$. Note that $\\{\ket{\phi},\ket{\phi^{\bot}}\\}$ forms a
single-qubit basis.

First, consider states of the form $\ket{\gamma}=\ket{u}\otimes\ket{\psi}$
where $\ket{u}\in\\{\ket{\phi},\ket{\phi^{\bot}}\\}$ and
$\ket{\psi}\in\mathbb{C}^{2^{n-1}}$. Clearly,

$(U\otimes I^{\otimes n-1})\ket{\gamma}=(U\otimes I^{\otimes
n-1})\ket{u}\otimes\ket{\psi}=(U\ket{u})\otimes\ket{\psi}=\lambda_{\\_}u\ket{u}\otimes\ket{\psi}.$

Hence, every state of the form of $\ket{\gamma}$ is an eigenstate of $U\otimes
I^{\otimes n-1}$. Additionally, note that by similar reasoning, for every
separable state $\ket{\gamma}=\ket{v}\otimes\ket{\psi}$ where
$\ket{v}\notin\\{\ket{\phi},\ket{\phi^{\bot}}\\}$, $\ket{\gamma}$ is not an
eigenstate of $U\otimes I^{\otimes n-1}$.

Now we show, that any state not in this separable form cannot be an eigenstate
of $U\otimes I^{\otimes n-1}$. By way of contradiction assume that
$\ket{\delta}$ is an eigenstate of $U\otimes I^{\otimes n-1}$ with $(U\otimes
I^{\otimes n-1})\ket{\delta}=\mu\ket{\delta}$. Expand

$\ket{\delta}=\alpha\ket{\phi}\ket{\psi_{\\_}1}+\beta\ket{\phi^{\bot}}\ket{\psi_{\\_}2}$

where $\ket{\psi_{\\_}1},\ket{\psi_{\\_}2}\in\mathbb{C}^{2^{n-1}}$. Then we
compute

$\displaystyle(U\otimes I^{\otimes n-1})\ket{\delta}$ $\displaystyle=$
$\displaystyle\alpha(U\ket{\phi})\ket{\psi_{\\_}1}+\beta(U\ket{\phi^{\bot}})\ket{\psi_{\\_}2}$
$\displaystyle=$
$\displaystyle\lambda\alpha\ket{\phi}\ket{\psi_{\\_}1}-\lambda\beta\ket{\phi^{\bot}}\ket{\psi_{\\_}2}$
$\displaystyle=$
$\displaystyle\mu\alpha\ket{\phi}\ket{\psi_{\\_}1}+\mu\beta\ket{\phi^{\bot}}\ket{\psi_{\\_}2}$

where we have used that $\ket{\phi}$ and $\ket{\phi^{\bot}}$ are the
$+\lambda$ and $-\lambda$ eigenvalues of $U$ respectively. As the components
of the expansion are orthogonal to each other, $\mu$ must satisfy:

$\mu\alpha=\lambda\alpha\text{ and }\mu\beta=-\lambda\beta.$

As $\lambda\not=0$, since $U\otimes I^{\otimes n-1}$ is unitary, we either
have (i) $\alpha=0$, $\mu=-\lambda$, and
$\ket{\delta}=\ket{\phi^{\bot}}\ket{\psi_{\\_}2}$ or (ii) $\beta=0$,
$\mu=+\lambda$, and $\ket{\delta}=\ket{\phi}\ket{\psi_{\\_}1}$. In either case
$\ket{\delta}$ has a separable form as claimed. ∎

Following Gottesman’s notation, let $U_{\\_}k:=I^{\otimes(n-k)}\otimes
U\otimes I^{\otimes(n-k)}$ for $1\leq k\leq n$ and a single qubit Pauli $U$.
(Gottesman writes $\overline{\mathbf{X}}_{\\_}k$ and
$\overline{\mathbf{Z}}_{\\_}k$; we’ll elide the bar but make frequent use of
the notation.) Combining Propositions 1 and 2, we obtain the following
corollary:

######  Corollary 1.

Every term of type $U_{\\_}k$ is separable, for $U\in\\{\pm X,\pm Y,\pm Z\\}$
and $1\leq k\leq n$. That is, the factor associated with $U$ is unentangled
with the rest of the system.

In this light, we can reconsider the types we’ve given to $CNOT$. In section
2, we showed that $CNOT$ has the type
$\mathbf{Z}\otimes\mathbf{X}\to\mathbf{Z}\otimes\mathbf{X}$. This is true but
not particularly useful to a programmer who doesn’t view the eigenvectors of
$\mathbf{Z}\otimes\mathbf{X}$ as a helpful category. If however, we look at
the intersection type given for $CNOT$ in section 3, we see that $CNOT$ has
the type
$(\mathbf{Z}\otimes\mathbf{I}\to\mathbf{Z}\otimes\mathbf{I})\cap(\mathbf{I}\otimes\mathbf{X}\to\mathbf{I}\otimes\mathbf{X})$.
This says that $CNOT$ takes $\ket{i}\otimes\ket{\psi}$ where $i\in\\{0,1\\}$
to a similar separable state, and likewise for when the second qubit is in
$\mathbf{X}$. Hence, we can conclude that it takes a separable pair of
$\mathbf{Z}$ and $\mathbf{X}$ qubits to a similar separable pair.

Our $\cap$-Arr-Dist rule (fig. 1), which follows directly from the subtyping
rules for arrow and intersection222Thanks to Andreas Rossberg for pointing
this out on Stack Overflow., allows us to make this explicit. We can weaken
$CNOT$’s type to
$(\mathbf{Z}\otimes\mathbf{I}\cap\mathbf{I}\otimes\mathbf{X})\to(\mathbf{Z}\otimes\mathbf{I}\cap\mathbf{I}\otimes\mathbf{X})$.
This type, which encodes the separability of the $\mathbf{Z}$ and $\mathbf{X}$
qubits, is useful enough that we will introduce a new type constructor
$\times$, where $A\times\mathbf{I}^{\otimes n}=A\otimes\mathbf{I}^{\otimes n}$
for $A\in\\{\pm X,\pm Y,\pm Z\\}$. This distributes in the expected way over
intersections: $(A\times B)\cap(A\otimes C)=A\times(B\cap C)$ and $(A\times
B)\cap(I\otimes C)=A\times(B\cap C)$, allowing us to derive
$CNOT:\mathbf{Z}\times\mathbf{X}$.

##  5 Example: Superdense Coding

To illustrate the power of this simple system, consider the example of
superdense coding as in fig. 2. Superdense coding allows Alice to convey two
bits of information $x$ and $y$, which we treat as qubits in the $\mathbf{Z}$
state, to Bob by sending a single qubit and consuming one EPR pair.

$x$$y$$\ket{0}$$x$$\ket{0}$$y$HXZXXH Figure 2: Superdense Coding sending
classical bits $x$ and $y$ from Alice to Bob.

The desired type for this circuit is
$\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}$, showing that
four classical bits are transmitted. Hence, we need to derive the output types
for $\mathbf{Z}_{\\_}1,\mathbf{Z}_{\\_}2,\mathbf{Z}_{\\_}3$ and
$\mathbf{Z}_{\\_}4$. We can trivially derive that superdense has types
$\mathbf{Z}_{\\_}1\to\mathbf{Z}_{\\_}1$ and
$\mathbf{Z}_{\\_}2\to\mathbf{Z}_{\\_}2$ (since $CZ$ and $CNOT$ have types
$\mathbf{Z}\otimes\mathbf{I}\to\mathbf{Z}\otimes\mathbf{I}$), so we’ll look at
the derivation for $\mathbf{Z}_{\\_}3$:

⬇

Definition superdense :$=$

INIT ; I $\otimes$ I $\otimes$ Z $\otimes$ I (* initial type *)

H 3 ; I $\otimes$ I $\otimes$ X $\otimes$ I (* create Bell pair *)

CNOT 3 4 ; I $\otimes$ I $\otimes$ X $\otimes$ X

CZ 1 3 ; Z $\otimes$ I $\otimes$ X $\otimes$ X (* map bits onto Bell pair *)

CNOT 2 3 ; Z $\otimes$ I $\otimes$ X $\otimes$ X

CNOT 3 4 ; Z $\otimes$ I $\otimes$ X $\otimes$ I (* decode qubits *)

H 3 Z $\otimes$ I $\otimes$ Z $\otimes$ I

We can similarly derive superdense : I $\otimes$ I $\otimes$ I $\otimes$ Z
$\rightarrow$ I $\otimes$ Z $\otimes$ I $\otimes$ Z. We can now combine all
four derivations using our distributivity rule for $\to$ and $\cap$ as
follows:

$\infer{\mathtt{superdense}:(\mathbf{Z}_{\\_}1\to\mathbf{Z}_{\\_}1)\cap(\mathbf{Z}_{\\_}2\to\mathbf{Z}_{\\_}2)\cap(\mathbf{Z}_{\\_}3\to\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{I})\cap(\mathbf{Z}_{\\_}4\to\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{Z})}{\infer{\mathtt{superdense}:\mathbf{Z}_{\\_}1\cap\mathbf{Z}_{\\_}2\cap\mathbf{Z}_{\\_}3\cap\mathbf{Z}_{\\_}4\to\mathbf{Z}_{\\_}1\cap\mathbf{Z}_{\\_}2\cap\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{I}\cap\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{Z}}{\infer{\mathtt{superdense}:\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}\to\mathbf{Z}\times(\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{I}\cap\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{I}\cap\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{Z})}{\infer{\mathtt{superdense}:\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}\to\mathbf{Z}\times(\mathbf{Z}\times(\mathbf{Z}\otimes\mathbf{I}\cap\mathbf{I}\otimes\mathbf{Z})}{\mathtt{superdense}:\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}\to\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}}}}}$

##  6 Example: GHZ state, Creation and Unentangling

To demonstrate how we can track the possibly entangling and disentangling
property of the CNOT gate, we can look at the example of creating the GHZ
state $\ket{000}+\ket{111}$ starting from $\ket{000}$ and then disentangling
it. A similar example was considered by Honda [10] to demonstrate how his
system can track when $CNOT$ displays either its entangling or un-entangling
behaviour. One crucial difference is that Honda uses the denotational
semantics of density matrices which, in practice, would scale badly with the
size of the program being type checked. Our approach is closer to that of
Perdrix [15, 16] in terms of design and scalability but capable of showing
separability where the prior systems could not.

We will consider the following GHZ program acting on the initial state
$\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}=\mathbf{Z}_{\\_}1\cap\mathbf{Z}_{\\_}2\cap\mathbf{Z}_{\\_}3$.
We first follow the derivation for $\mathbf{Z}_{\\_}1$:

⬇

Definition GHZ :$=$

INIT ; Z $\otimes$ I $\otimes$ I (* initial state *)

H 1; X $\otimes$ I $\otimes$ I

CNOT 1 2; X $\otimes$ X $\otimes$ I (* Bell Pair *)

CNOT 2 3: X $\otimes$ X $\otimes$ X (* GHZ State created *)

Repeating the derivation for $Z_{\\_}2$ and $Z_{\\_}3$, We obtain the
following type:

$\mathtt{GHZ}:(\mathbf{Z}_{\\_}1\textrightarrow\mathbf{X}⊗\mathbf{X}⊗\mathbf{X})∩(\mathbf{Z}_{\\_}2\textrightarrow\mathbf{Z}⊗\mathbf{Z}⊗\mathbf{I})∩(\mathbf{Z}_{\\_}3\textrightarrow\mathbf{I}⊗\mathbf{Z}⊗\mathbf{Z})$

This type is non-trivial to read, but we can clearly see that entanglement is
produced between the three qubits.

If we now apply CNOT 2 1, we get the following type:

$\mathtt{GHZ;~{}CNOT~{}2~{}1}:(\mathbf{Z}_{\\_}1\textrightarrow\mathbf{I}⊗\mathbf{X}⊗\mathbf{X})∩(\mathbf{Z}_{\\_}2\textrightarrow\mathbf{Z}⊗\mathbf{I}⊗\mathbf{I})∩(\mathbf{Z}_{\\_}3\textrightarrow\mathbf{I}⊗\mathbf{Z}⊗\mathbf{Z})$

We can reduce the output type to
$\mathbf{Z}\times(\mathbf{X}\otimes\mathbf{X}\cap\mathbf{Z}\otimes\mathbf{Z})$,
showing that we’ve neatly separated the first qubit from the Bell pair on
qubits 2 and 3 in what used to be a GHZ state.

If we then apply CNOT 3 2 we get

$\mathtt{GHZ;~{}CNOT~{}2~{}1;~{}CNOT~{}3~{}2}:(\mathbf{Z}_{\\_}1\textrightarrow\mathbf{I}⊗\mathbf{I}⊗\mathbf{X})∩(\mathbf{Z}_{\\_}2\textrightarrow\mathbf{Z}⊗\mathbf{I}⊗\mathbf{I})∩(\mathbf{Z}_{\\_}3\textrightarrow\mathbf{I}⊗\mathbf{Z}⊗\mathbf{I})$

resulting in the fully separable state
$\mathbf{Z}\times\mathbf{Z}\times\mathbf{X}$.

##  7 Beyond the Clifford Group

Universal quantum computation requires that we use gates outside the Clifford
set, the two most studied candidates being the $T$ ($\pi/8$) and Toffoli
gates. In order to type $T$ and Toffoli, we will need to add a new $\top$
type, which describes any basis state in the state interpretation of our
types, and any unitary in the Heisenberg interpretation. We can then give the
following type to the $T$ gate:

$\displaystyle T:~{}$ $\displaystyle\mathbf{Z}\rightarrow\mathbf{Z}$
$\displaystyle T:~{}$ $\displaystyle\mathbf{X}\rightarrow\top$

Here $\top$ really is a top type. Unlike $\mathbf{I}$, which behaves like an
identity, $\top$ behaves like an annihilator:

$\displaystyle\forall A,\mathbf{I}A=A=A\mathbf{I}$ $\displaystyle\forall
A,\top A=\top=A\top$

Instead of explicitly giving a type to the Toffoli gate, we can derive it from
Toffoli’s standard decomposition into $T$, $H$ and $CNOT$ gates:

⬇

Definition TOFFOLI a b c :$=$

H c;

CNOT b c; T† c;

CNOT a c; T c;

CNOT b c; T† c;

CNOT a c; T b; T c;

H c;

CNOT a b; T a; T† b;

CNOT a b.

We first note that $T^{\dagger}$ is simply seven consecutive $T$s, so like
$T$, it preserves $\mathbf{Z}$ and takes $\mathbf{X}$ to $\top$. Now consider
TOFFOLI’s action on $\mathbf{I}\otimes\mathbf{I}\otimes\mathbf{X}$. We can
annotate the program with the types after every line:

⬇

Definition TOFFOLI a b c :$=$

INIT ; I $\otimes$ I $\otimes$ X

H c ; I $\otimes$ I $\otimes$ Z

CNOT b c; T† c; I $\otimes$ Z $\otimes$ Z

CNOT a c; T c; Z $\otimes$ Z $\otimes$ Z

CNOT b c; T† c; Z $\otimes$ I $\otimes$ Z

CNOT a c; T b; T c; I $\otimes$ I $\otimes$ Z

H c; I $\otimes$ I $\otimes$ X

CNOT a b; T a; T† b; I $\otimes$ I $\otimes$ X

CNOT a b. I $\otimes$ I $\otimes$ X

The $T$’s here are all identities, so only the behaviors of $H$ (which takes
$\mathbf{X}$ to $\mathbf{Z}$ and back) and $CNOT$ (which takes
$\mathbf{I}\otimes\mathbf{Z}$ to $\mathbf{Z}\otimes\mathbf{Z}$ and back) are
relevant.

The derivations for $\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{I}$ and
$\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{I}$ are similar, and the other
three states map to the top element:

$\begin{array}[]{rlrl}\mathtt{TOFFOLI}:&\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{I}\rightarrow\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{I}&\quad\mathtt{TOFFOLI}:&\mathbf{X}\otimes\mathbf{I}\otimes\mathbf{I}\rightarrow\top\otimes\top\otimes\top\\\
\mathtt{TOFFOLI}:&\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{I}\rightarrow\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{I}&\quad\mathtt{TOFFOLI}:&\mathbf{I}\otimes\mathbf{X}\otimes\mathbf{I}\rightarrow\top\otimes\top\otimes\top\\\
\mathtt{TOFFOLI}:&\mathbf{I}\otimes\mathbf{I}\otimes\mathbf{Z}\rightarrow\top\otimes\top\otimes\top&\quad\mathtt{TOFFOLI}:&\mathbf{I}\otimes\mathbf{I}\otimes\mathbf{X}\rightarrow\mathbf{I}\otimes\mathbf{I}\otimes\mathbf{X}\\\
\end{array}$

Using our technique for deriving judgements about separability, we can further
derive the following type for the Toffoli gate

$\mathtt{TOFFOLI}:\mathbf{Z}\times\mathbf{Z}\times\mathbf{X}\rightarrow\mathbf{Z}\times\mathbf{Z}\times\mathbf{X}$

which says that if you feed a Toffoli three separable qubits in the
$\mathbf{Z}$, $\mathbf{Z}$ and $\mathbf{X}$ basis, you receive three qubits in
the same basis back.

##  8 Applications and Future Work

We think that this type system, along with possible extensions, is broadly
applicable. Here we outline some of the possible uses of the type system along
with (where necessary) extensions that will enable these uses.

#### Stabilizer Types and Quantum Error Correction

This aim of this paper is to define types for unitary operations, however in
section 3 we interpreted types such as $\mathbf{X}\otimes\mathbf{X}$ and
$\mathbf{X}\otimes\mathbf{I}$ as being inhabited by certain states. Gates and
circuits, by acting on such states, obtain an arrow type. But as we vary the
input states on which unitaries act, they in fact obtain many different arrow
types. We used the concept of intersection types to characterize this
phenomenon.

However the nature of Pauli operators allows for a different treatment using
the stabilizer formalism [8]. Namely two tensor products of Pauli operators
(of the same arity) must either commute or anticommute. Consequently, any
collection of such types with a joint eigenspace (and hence having a nonempty
intersection type) necessarily pairwise commutes. Then, in fact, any product
of these operators will also share this eigenspace and would serve equally
well in describing the intersection type.

For example, $X\otimes X$ and $X\otimes I$ commute and the intersection type
$(\mathbf{X}\otimes\mathbf{X})\cap(\mathbf{X}\otimes\mathbf{I})$ is nonempty,
being $\\{\ket{++},\ket{+-},\ket{-+},\ket{--}\\}$. These states are also
eigenstates of $I\otimes X=(X\otimes X)(X\otimes I)$ and hence also of type
$\mathbf{I}\otimes\mathbf{X}=(\mathbf{X}\otimes\mathbf{X})*(\mathbf{X}\otimes\mathbf{I})$.
Consequently our intersection type could be equally well presented as
$(\mathbf{X}\otimes\mathbf{X})\cap(\mathbf{I}\otimes\mathbf{X})$ or
$(\mathbf{I}\otimes\mathbf{X})\cap(\mathbf{X}\otimes\mathbf{I})$. And so we
should not think of the intersection type
$(\mathbf{X}\otimes\mathbf{X})\cap(\mathbf{X}\otimes\mathbf{I})$ being
determined by $\mathbf{X}\otimes\mathbf{X}$ and $\mathbf{X}\otimes\mathbf{I}$
alone, but rather by all the elements in the (commutative) group they
generate.

Such a commutative group is typically called a stabilizer group. Formally, a
stabilizer group is any commutative group of tensor products of Pauli
operators some common arity $n$ that does not contain $-I^{\otimes n}$. This
latter condition ensures the joint $+1$-eigenspace of all the operators in a
stabilizer group exists, which then is called the stabilizer code associated
to the group [7]. The eigenspaces associated with other eigenvalue
combinations are called syndrome spaces. Therefore our intersection type
(presuming it does not include $-\mathbf{I}^{n}$) is realized as a stabilizer
code and its associated syndrome spaces, hence capturing the notion of a Pauli
frame [11].

The Gottesman semantics of section 2 then can be interpreted as type theory
for stabilizer groups and stabilizer codes, which is the direction taken by
[10]. This provides a type theory for stabilizer codes that includes encoding
and decoding [4], and syndrome extraction [20] circuits. Potential other
applications could include analyzing circuits that implement non-Clifford
gates on stabilizer codes [14, 22] and circuits that fault-tolerantly switch
between codes [5].

Beyond application to quantum error correction, treating intersection types
through stabilizer groups offers new deduction rules. In the analysis of the
GHZ state of section 6, the type of GHZ; CNOT 1 3 has as codomain the
intersection type

$(\mathbf{X}\otimes\mathbf{X}\otimes\mathbf{I})\cap(\mathbf{Z}\otimes\mathbf{Z}\otimes\mathbf{I})\cap(\mathbf{Z}\otimes\mathbf{Z}\otimes\mathbf{Z}).$

Given the deduction rules of fig. 1 alone, proving separability of this type
is impossible. Yet through the stabilizer formalism, one recognizes it also
has the type
$(\mathbf{I}\otimes\mathbf{I}\otimes\mathbf{Z})=(\mathbf{Z}\otimes\mathbf{Z}\otimes\mathbf{I})*(\mathbf{Z}\otimes\mathbf{Z}\otimes\mathbf{Z})$,
and so we may represent our intersection type equivalently as

$(\mathbf{X}\otimes\mathbf{X}\otimes\mathbf{I})\cap(\mathbf{Z}\otimes\mathbf{Z}\otimes\mathbf{I})\cap(\mathbf{I}\otimes\mathbf{I}\otimes\mathbf{Z})=((\mathbf{X}\otimes\mathbf{X})\cap(\mathbf{Z}\otimes\mathbf{Z}))\times\mathbf{Z}.$

#### Adding measurement

It’s challenging to turn Gottesman’s semantics for measurement into a type
system in light of the fact that it looks at the operation on all the basis
states, rather than simply the evolution of a single Pauli operator. Namely it
adds significant computational complexity, where typechecking should be
linear. Nonetheless, the action of measurement on stabilizer groups is
understood [8]. With the link between intersection types and stabilizers
established above, we can see the potential for realizing such a type system.
The challenge lies in the fact that to execute the action of measurement on a
stabilizer group, one needs to find a set of generators of the group in a
particular form. In our grammar, we need to express an intersection type using
a special presentation, which requires the introduction of rewrite rules like
those we just used in the analysis of the GHZ state.

Formally measurement acts as follows; for ease of exposition, suppose we are
measuring the first qubit in the computational basis (a $Z$-basis
measurement). From our initial intersection, do the following:

  1. 1.

Use the rewrite rules to ensure there are only $0$ or $1$ terms in the
intersection that have $\mathbf{X}$ in the first position. If there is $1$
such term, then remove it from the intersection.

  2. 2.

If there are $0$ terms that have $\mathbf{X}$ in the first position, use the
rewrite rules to ensure there are only $0$ or $1$ terms that have $\mathbf{Z}$
in the first position. If there is $1$ such term, remove it from the
intersection.

  3. 3.

Add $\mathbf{Z}\otimes\mathbf{I}^{n-1}$ to the intersection.

The resulting intersection type is the type after measurement.

For example in our analysis of the GHZ state in section 6, the circuit GHZ had
a codomain of type

$(\mathbf{X}\otimes\mathbf{X}\otimes\mathbf{X})\cap(\mathbf{Z}\otimes\mathbf{Z}\otimes\mathbf{I})\cap(\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{Z}).$

To compute the type of GHZ; MEAS 1 we enact the above program. Fortunately our
intersection already has the requisite form, with the first term being the
only one with an $\mathbf{X}$ in the initial position. We remove the term and
add $\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{I}$ to get

$(\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{I})\cap(\mathbf{Z}\otimes\mathbf{Z}\otimes\mathbf{I})\cap(\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{Z}).$

Using these same rewrite rules, we can replace the second term with
$\mathbf{I}\otimes\mathbf{Z}\otimes\mathbf{I}$ and with that term replace the
last with $\mathbf{I}\otimes\mathbf{I}\otimes\mathbf{Z}$, producing the output
type as

$(\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{I})\cap(\mathbf{Z}\otimes\mathbf{I}\otimes\mathbf{I})\cap(\mathbf{I}\otimes\mathbf{I}\otimes\mathbf{Z})=\mathbf{Z}\times\mathbf{Z}\times\mathbf{Z}.$

At first glance, it is not clear that the program for measurement above is
well-defined. Why should such a presentation for a general intersection type
exist? Even if one does, how do we find one among all possible rewrites?
Fortunately neither of the concerns is an issue. It is well known that
stabilizer groups have a denotational semantics as binary matrices of
dimension linear in the number of qubits, see for example [13, §10.5]. The
existence of such a presentation, and a procedure to find one, reduces to
straightforward linear algebra. Hence the program above for measurement can be
accomplished in at worst quadratic time in the number of qubits.

#### Resource Tracking

Resource monotones track the amount of resources contained in a type. For
instance, at a very coarse level, one might quantify the entanglement in a
state by counting the number of “ebits” needed to create the state. In our
formalism, a Bell state is of type
$\mathbf{E}=(\mathbf{X}\otimes\mathbf{X})\cap(\mathbf{Z}\otimes\mathbf{Z})$,
which is counted as having one ebit. A seperable type such as
$\mathbf{X}\times\mathbf{Z}$ has a resource value 0 and hence no ebits. While
the current system cannot handle such resource monotones, it seems plausible
that using a suitable extension could similarly calculate the resource cost of
various operations. Say, by counting the number of $\mathbf{E}$ types used in
a protocol. Then, superdense coding has an $\mathbf{E}$-count of 1 while
entanglement swapping will have an $\mathbf{E}$-count of 2.

Our types are too fine to capture the notion of local equivalence [12].
Instead, one can coarsen to types generated from graph states [6]. For
example, all six entangled two qubit types are equivalent under the local
operations of $H\otimes I$, $S\otimes I$, $I\otimes H$, and $I\otimes S$, and
therefore, from an entanglement monotone perspective, they all contain the
same amount of entanglement.

One can show that for three qubits, there are only two classes of entangled
types, up to relabeling of the qubit indices [3]. Such computations are quite
challenging at scale, and so methods to quantify the amount of entanglement
using such states is a long-term goal of this project.

#### Ancilla correctness.

Many quantum circuits introduce ancillary qubits that are used to perform some
classical computation and are then discarded in a basis state. Several efforts
have been made to verify this behaviour: The Quipper [9] and Q# [21] languages
allow us to _assert_ that ancilla are separable and can be safely discarded,
while $\mathcal{Q}\textsc{wire}$ allows us to manually verify this [18]. More
recently, Silq [2] allows us to define “qfree” functions that never put qubits
into a superposition. We hope to avoid this restriction and use our type
system to automatically guarantee ancilla correctness by showing that the
ancillae are in $\mathbf{Z}$ and separable.

#### Provenance tracking

Another useful addition to the type system is _ownership_. Superdense coding
is a central example of a class of quantum communication protocols. By
annotating the typing judgements with ownership information and restricting
multiqubit operations to qubits under the same ownership, we can guarantee
that superdense coding only transmits a single qubit, via a provided channel
$\mathcal{C}$. (Note that measurement and ownership types are both forms of
static information-flow control [19].) With this additional typing
information, we can give superdense coding the type

$\mathbf{Z}_{\\_}A\times\mathbf{Z}_{\\_}A\times\mathbf{Z}_{\\_}A\times\mathbf{Z}_{\\_}B\to\mathbf{Z}_{\\_}A\times\mathbf{Z}_{\\_}A\times\mathbf{Z}_{\\_}B\times\mathbf{Z}_{\\_}B$

indicating that a single qubit has passed from Alice’s control to Bob’s.

### Acknowledgements

The first author would like to acknowledge the support of the U.S. Department
of Energy, Office of Science, Office of Advanced Scientific Computing
Research, Quantum Testbed Pathfinder Program under Award Number DE-SC0019040.
The third author was funded by EPiQC, an NSF Expedition in Computing, under
grant CCF-1730449.

## References

  * [1]
  * [2] Benjamin Bichsel, Maximilian Baader, Timon Gehr & Martin Vechev (2020): _Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics_.  In: Proc. PLDI ’20, p. 286–300, 10.1145/3385412.3386007.  Available at https://files.sri.inf.ethz.ch/website/papers/pldi20-silq.pdf.
  * [3] Sergey Bravyi, David Fattal & Daniel Gottesman (2006): _GHZ extraction yield for multipartite stabilizer states_.  J. Math. Phys. 47(6), p. 062106, 10.1063/1.2203431.  Available at https://arxiv.org/abs/quant-ph/0504208.
  * [4] Richard Cleve & Daniel Gottesman (1997): _Efficient Computations of Encodings for Quantum Error Correction_.  Phys. Rev. A 56, pp. 76–82, 10.1103/PhysRevA.56.76.  Available at https://arxiv.org/abs/quant-ph/9607030.
  * [5] Kristina R Colladay & Erich J Mueller (2018): _Rewiring Stabilizer Codes_.  New Journal of Physics 20(8), p. 083030, 10.1088/1367-2630/aad8dd.  Available at https://arxiv.org/abs/1707.09403.
  * [6] David Fattal, Toby S Cubitt, Yoshihisa Yamamoto, Sergey Bravyi & Isaac L Chuang (2004): _Entanglement in the stabilizer formalism_.  arXiv preprint.  Available at https://arxiv.org/abs/quant-ph/0406168.
  * [7] Daniel Gottesman (1996): _Class of quantum error-correcting codes saturating the quantum Hamming bound_.  Phys. Rev. A 54(3), p. 1862–1868, 10.1103/physreva.54.1862.  Available at https://arxiv.org/abs/quant-ph/9604038.
  * [8] Daniel Gottesman (1998): _The Heisenberg Representation of Quantum Computers_.  In: Group22: Proceedings of the XXII International Colloquium on Group Theoretical Methods in Physics, pp. 32–43.  Available at https://arxiv.org/abs/quant-ph/9807006.
  * [9] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger & Benoît Valiron (2013): _Quipper: A Scalable Quantum Programming Language_.  In: Proc. PLDI ’13, pp. 333–342, 10.1145/2491956.2462177.  Available at https://arxiv.org/abs/1304.3390.
  * [10] Kentaro Honda (2015): _Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism_.  In: Proc. QPL ’15, pp. 262–272, 10.4204/EPTCS.195.19.
  * [11] E. Knill (2005): _Quantum computing with realistically noisy devices_.  Nature 434(7029), pp. 39–44, 10.1038/nature03350.  Available at https://arxiv.org/abs/quant-ph/0410199.
  * [12] Maarten Van den Nest, Jeroen Dehaene & Bart De Moor (2005): _Local unitary versus local Clifford equivalence of stabilizer states_.  Phys. Rev. A 71, p. 062323, 10.1103/PhysRevA.71.062323.  Available at https://arxiv.org/abs/quant-ph/0411115.
  * [13] Michael A. Nielsen & Isaac L. Chuang (2010): _Quantum Computation and Quantum Information: 10th Anniversary Edition_.  Cambridge University Press, 10.1017/CBO9780511976667.
  * [14] Adam Paetznick & Ben W. Reichardt (2013): _Universal Fault-Tolerant Quantum Computation with Only Transversal Gates and Error Correction_.  Phys. Rev. Lett. 111, p. 090505, 10.1103/PhysRevLett.111.090505.  Available at https://arxiv.org/abs/1304.3709.
  * [15] Simon Perdrix (2007): _Quantum Patterns and Types for Entanglement and Separability_.  Electron. Notes Theor. Comput. Sci. 170, pp. 125–138, 10.1016/j.entcs.2006.12.015.  Proc. QPL ’05.
  * [16] Simon Perdrix (2008): _Quantum Entanglement Analysis Based on Abstract Interpretation_.  In: Static Analysis, pp. 270–282, 10.1007/978-3-540-69166-218.  Available at https://arxiv.org/abs/0801.4230.
  * [17] Benjamin C. Pierce (2002): _Types and Programming Languages_.  MIT Press.
  * [18] Robert Rand, Jennifer Paykin, Dong-Ho Lee & Steve Zdancewic (2018): _ReQWIRE: Reasoning about Reversible Quantum Circuits_.  In: Proc. QPL ’18, pp. 299–312, 10.4204/EPTCS.287.17.
  * [19] A. Sabelfeld & A. C. Myers (2006): _Language-based information-flow Security_.  IEEE J. Sel. Areas Commun. 21(1), pp. 5–19, 10.1109/JSAC.2002.806121.  Available at https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf.
  * [20] A. M. Steane (1997): _Active Stabilization, Quantum Computation, and Quantum State Synthesis_.  Phys. Rev. Lett. 78, pp. 2252–2255, 10.1103/PhysRevLett.78.2252.  Available at https://arxiv.org/abs/quant-ph/9611027.
  * [21] Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz & Martin Roetteler (2018): _Q#: Enabling Scalable Quantum Computing and Development with a High-level DSL_.  In: Proc. Real World Domain Specific Languages Workshop (RWDSL) 2018, pp. 7:1–7:10, 10.1145/3183895.3183901.  Available at https://arxiv.org/abs/1803.00652.
  * [22] Theodore J. Yoder (2017): _Universal fault-tolerant quantum computation with Bacon-Shor codes_.  arXiv preprint.  Available at https://arxiv.org/abs/1705.01686.