Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 14, 2019

The ZX-Calculus for Stabilizer Quantum Mechanics

Posted by John Baez

guest post by Fatimah Ahmadi and John van de Wetering

This is the second post of Applied Category Theory School 2019. We present Backens’ completeness proof for the ZX-calculus for stabilizer quantum mechanics.

## Introduction

Physicists from all fields are used to graphical calculi, the most common being Feynman diagrams. Feynman diagrams were introduced by Richard Feynman in the 1940s as a bookkeeping method for the messy calculations of quantum electrodynamics. In David Kaiser’s words,

In the hands of a postwar generation, a tool intended to lead quantum electrodynamics out of a decades-long morass helped transform physics.

The applications of Feynman diagrams are not limited to QED and prevailed in other areas of physics, such as cosmology, or statistical and condensed matter physics. Another well-known example of a graphical calculus was invented by Roger Penrose for the calculation of tensors; a convenient method to match and contract the middle indices of tensors.

However, neither of these methods were initially based on a rigorous mathematical setting. As mentioned earlier, they were just introduced as more of a bookkeeping method based on what we expect to obtain if a calculation is done in a standard formalism.

In 2004, Samson Abramsky and Bob Coecke pioneered a new formalism for quantum mechanics using monoidal category theory which comes with a rigorous graphical calculus. They found that compact closed categories were well suited to describing quantum mechanics.

In this formalism, physical systems are objects of a compact closed category and a process between two systems is a morphism. A state of a system is also interpreted as a process, meaning a morphism from the monoidal unit to an object. The sequential application of processes is the composition of morphisms, and the joint system/process is given by the monoidal product of two objects/morphisms. This framework has classical physics in one extreme as the category of sets and quantum-like physics in another extreme.

Although one can recover Hilbert space quantum mechanics from Categorical Quantum Mechanics (CQM), it intends to suggest a fresh insight into quantum mechanics in the foundational level. In this post, however, we will restrict ourselves to the categorical formulation of standard quantum physics: the category of finite-dimensional Hilbert spaces. We restrict the model even further and only introduce a graphical calculus, namely the ZX-calculus, as a useful tool for the qubit-based quantum computation with post-selected measurements.

We assume a working knowledge of quantum computation, you may also find the introduction of the previous post useful.

The building blocks of quantum computers in the matrix formalism are:

  1. qubits, which are encoded in the states of a two-dimensional Hilbert space, like the spin of an electron,
  2. quantum gates, particularly the Clifford+T gates.
  3. projective measurements, represented by self-adjoint operators.

Despite the indisputable usefulness of the matrix formalism in quantum computation, it is still a low-level language. Calculating the tensor products of matrices is impractical because the sizes of the matrices increase exponentially with the number of qubits. An alternative that scales better with an increasing amount of qubits are graphical languages. A graphical language consists of a set of generators, some ways to compose them into a diagram, and a set of rules that tell you when two diagrams are equal. The dominant graphical language in quantum computation is the circuit model. In the circuit model, time goes left to right, each wire represents a qubit, boxes are gates and the tensor product of two qubits is depicted by parallel wires.

The circuit model makes tracking and simplifying a computation easier. For instance take the circuit to the right: knowing that V 2=Y 2=IV^2=Y^2=I, YY and UU commute and Y=ERY=E \otimes R, one can transform this circuit into a simpler one.

However, the circuit model is inflexible, and does not allow any topological deformation. In contrast, The ZX-calculus and other calculi inspired by CQM (like the ZW-calculus or ZH-calculus) have a set of built-in rewrite rules which have fewer restrictions on the topology, and as a result allows rewrites that have no counterpart in the circuit model. These rules propose a systematic way for simplification of diagrams. For instance, using naturality of braiding in a symmetric category, we can simplify this diagram.

Any graphical calculus should satisfy at least three main conditions to be able to replace the matrix formalism:

  • Universality, meaning any gate/unitary matrix has a corresponding diagram. It implies a language is general enough to describe all possible calculations.
  • Soundness, meaning if two diagrams are equivalent in a graphical calculus D 1=D 2D_1=D_2, their matrix representation should also be the same [[D 1]]=?[[D 2]][\![ D_1 ]\!]\overset{?}{=}[\![ D_2 ]\!].
  • Completeness, meaning if the matrix representations of two diagrams are equal, [[D 1]]=[[D 2]][\![ D_1 ]\!]=[\![ D_2 ]\!], then two diagrams are equivalent, D 1=?D 2D_1\overset{?}{=} D_2. Completeness entails that a rule set is powerful enough to prove all equalities.

Remark: Equivalent diagrams might not be identical, but using rewrite rules, there is a series of moves which transform one to another.

The ZX-calculus is a PROP: a category of natural numbers with addition as a monoidal structure. There are only two types of morphism, red spiders and green spiders, which are decorated with an angle in [0,2π)[0, 2 \pi) and can have an arbitrary amount of inputs and outputs (in this picture, red node is a node with white α\alpha and green node is the node with black α\alpha).

These morphisms can be combined by juxtaposition, which corresponds to the tensor product, or by connecting the wires, which corresponds to the regular composition of linear maps. Rewrite rules quotient out the morphisms in the category. A functor from this category to the category of finite-dimensional Hilbert spaces is a matrix formalism interpretation. In this picture, soundness equates to the functoriality of the functor, universality means this functor is surjective on morphisms and completeness is captured by injectivity of this functor. In other words, if the ZX-calculus intends to fully describe Hilbert space quantum mechanics, this functor should be an equivalence.

The proof of universality and soundness of the ZX-calculus is straightforward. For universality, we only need to show each gate has a corresponding diagram. Soundness also follows from checking the matrix representation of each rewrite rule. The difficulty is in the completeness proof. In this post, we give the completeness proof for the ZX-calculus for stabilizer quantum mechanics. Note that this result ignores global scalars. That is we consider equality modulo normalisation: UU U \cong U^\prime if U =αUU^\prime = \alpha U such that α\alpha \in \mathbb{C} and α0\alpha \neq 0.

The outline of the rest of this post will be as follows: we introduce the ZX-calculus for the stabilizer quantum mechanics, then briefly review stabilizer quantum mechanics and its relation to graph states. We show that there is a correspondence between stabilizer states and graph states with local Cliffords and that this correspondence can be proven inside the ZX-calculus. Finally, as a pair of such diagrams are identical if and only if they correspond to the same quantum states, we can use this to show completeness of the calculus.

The ZX-calculus for the stabilizer states

The basic elements of the ZX-calculus for stabilizer quantum mechanics are:

  • wires, representing qubits (Wires are bendable, i.e. we have “cups” and “caps”, as well as straight wires.),
  • spiders, they are morphisms of the category. There are two types of spiders: Green spiders are represented in the computational basis {12[1 0],12[0 1]}\{ \frac{1}{\sqrt2}\begin{bmatrix} 1\\ 0 \end{bmatrix} , \frac{1}{\sqrt2}\begin{bmatrix} 0\\ 1 \end{bmatrix} \}. Red spiders are represented in the Hadamard basis {12[1 1],12[1 1]}\{ \frac{1}{\sqrt2}\begin{bmatrix} 1\\ 1 \end{bmatrix} , \frac{1}{\sqrt2}\begin{bmatrix} 1\\ -1 \end{bmatrix} \}. α\alpha is in the set of {0,π/2,π,π/2}\{ 0, \pi/2, \pi, -\pi/2 \} . An unlabled node is a zero phase.
  • Hadamard gates:

  • the tensor product, the tensor product of two diagrams is given by gluing them side by side.

  • for the composition of two spiders, we glue diagrams vertically and,

  • rewrite rules which are shown in the following pictures:

Spider rules and identity

Bialgebra, Hopf algebra, and copying

π\pi-copying π\pi-commutation and color change

Euler decomposition of Hadamard. This rule cannot be derived from the categorical axioms; nonetheless, it is necessary for the completeness result.

Stabilizer Quantum Mechanics

The stabilizer quantum computation is a non-universal fragment of quantum computation. Its basic elements are 1. qubits prepared in |0 n|0\rangle ^{\otimes n} ; 2. Clifford gates and 3. Projective measurements in the computational basis. Based on the Gottesman-Knill theorem, this fragment can be efficiently simulated by a classical computer and it is not even a universal classical model. However, it is still an important fragment for fault-tolerant and measurement-based quantum computation.

The completeness result

The proof of the main theorem is through an algorithmic procedure. It takes two diagrams with the same matrix representation. Then, separately, using the Choi-Jamiolkowski isomorphism, it transforms each of them into a state. Finally, by applying rewrite rules, it turns both of the diagrams into particular graph states with local Clifford operations which will represent the same state if and only if the diagrams are identical. We ignore the details of computation and only present the big picture of the proof. The interested reader can consult the paper for more detail on steps of the proof.

Definition 1: A group GG generated by some Pauli matrices P nP_n stabilizes a state ψ\psi if for every element UGU \in G in this group, Uψ=ψU \psi = \psi . We call this state a stabilizer state.

Remark: Any stabilizer state can be given uniquely by the generators of this group. Thus, for specifying the state, it is enough to give the generators of this group.

Definition 2: A finite graph state (V,E)(V, E) with a finite set of vertices VV and a finite set of edges EE, is an undirected simple graph.

Definition 3: Given a graph (V,E)(V, E) with nn vertices, |V|=n|V|=n, the corresponding graph state is an n-qubit state with a stabilizer group generated by nn operators. These generators are given by assigning an XX operator to each node and a ZZ operator to nodes connected to it. For instance, the generators of this graph are: {XZZZ,ZXZZ,ZZXI,ZZIX}\{ X \otimes Z \otimes Z \otimes Z, Z \otimes X \otimes Z \otimes Z , Z \otimes Z \otimes X \otimes I , Z \otimes Z \otimes I \otimes X \}

Definition 4: A n-qubit GS-LC diagram is a graph state modulo single qubit Clifford operators. I.e. G shown in the picture is a graph and UUs are single qubit Clifford operators applied to nodes of the main graph.

Every graph state gives a stabilizer state, but not every stabilizer state is equal to a graph state. We define equivalence classes of stabilizer states which can be transformed into each other by applying local Clifford operators. In this way, we can get a reduced form of GS-LC state for every stabilizer state.

Definition 5: A stabilizer state diagram in reduced GS-LC (written rGS-LC) form is a diagram in GS-LC form satisfying the following additional constraints:

  • All vertex operators belong to the set:

  • Two adjacent vertices must not both have vertex operators that include red nodes.

Theorem 6: Any stabilizer state is equivalent to a rGS-LC state.

Proposition 7: A ZX-calculus representation of a graph state is given by substituting

  • each node of the graph state with a green node with one output, and
  • each edge with a Hadamard gate connected to both green nodes of the edge.

For instance,

Definition 8: A pair of rGS-LC diagrams on the same number of qubits is called simplified if there are no pairs of qubits pp,qq such that pp has a red node in its vertex operator in the first diagram but not in the second, qq has a red node in the second diagram but not in the first, and pp and qq are adjacent in at least one of the diagrams.

Proposition 9: Any pair of rGS-LC diagrams on nn qubits can be simplified.

Theorem 10: The two diagrams making up a simplified pair of rGS-LC diagrams are equal, i.e. they correspond to the same quantum state, if and only if they are identical.

Theorem 11: The ZX-calculus is complete for stabilizer quantum mechanics.

Proof: Given two different diagrams corresponding to the same matrix:

  1. We first transform them into two states, using the fact that the category has duals.

  1. Then we simplify diagrams to get two simplified rGS-LC diagrams in ZX-representation.
  2. Again, it uses the trick of the first step to transform them back into two operators.
  3. Using Theorem 10, if they represent the same matrix, they should be two identical graphs. For example, the CZ operator,CZ=[1 0 0 0 0 1 0 0 0 0 1 0 0 0 0 1]CZ=\begin{bmatrix} 1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 1 & 0 \\ 0 & 0 & 0 & -1 \end{bmatrix} , is given by two distinct diagrams as below:

For the first step, we bend the lower part of two diagrams and replace the cup with an equivalent ZX graph state.

Then by applying π\pi rules and changing colors we get:

The final simplified diagram, by application of rewrite rules and other lemmas presented in this paper, will be:

For the right-hand side diagram, again we bend the diagrams, substitute the cup with ZX-calculus representation and finally apply the color change rule to get:

After applying rewrite rules, the above digram turns into the same final simplified diagram of the left-hand side and this completes the proof.


During the 5 years since Backens’ paper was released, a lot has happened in the world of graphical calculi for quantum computation. The above rule-set was only complete for Clifford computation. We now have extensions of the rule-set that are complete for Clifford+T quantum computing , and universal quantum computing, this latter one only requiring a single additional rule. There are also other graphical calculi being used. The ZW-calculus allows a natural description of Fermionic quantum computing, while the ZH-calculus can describe Toffoli–Hadamard circuits easily.

The ZX-calculus with the rule-set presented above has been used for a variety of applications. The representation of the graph-states is helpful in describing measurement-based quantum computation, while the rules allow one to easily reason about this model of computation. ZX-diagrams also seem to be a very natural language for describing lattice surgery on surface code quantum computers. Finally, recently the ZX-calculus has seen some use in circuit optimisation. In particular, using the rules described above, new ways to minimize the amount of T gates, an important cost metric for fault-tolerant quantum computation, have been found in this paper. Some extensions of the rule-set seem promising for circuit optimisation as well. In particular, an extended Euler Decomposition rule has been used to prove non-trivial circuit identities.

Posted at April 14, 2019 1:20 AM UTC

TrackBack URL for this Entry:

3 Comments & 0 Trackbacks


On Wednesday, April 10, I went to a lecture on math and biology, where it was about how the measure the distance between two clusters of data sets. Then, in the evening I went to a public lecture by a famous physicist named Roger Penrose who studied black holes before most scientists thought they existed. Coincidentally, the talk was on the same day that the Event Horizon Telescope announced that they imaged a black hole. Roger Penrose also invented Penrose diagrams and Penrose Tilings. In his talk, he used hand drawn drawings on transparencies on an overhead projector, which is very old fashioned, but he is 87 years old. He was promoting his own personal theory of cyclical cosmology, outside the mainstream, that every universe is proceeded by a previous universe, and followed by another universe, infinitely in both directions. He does not assume a Big Crunch followed by a Big Bang, and instead assumes that the universe expands until it’s thin, cold, and empty, and then that transitions into the next Big Bang.

His talk was titled “Are we seeing Hawking Points in the Microwave Sky?”

They held the talk in a large auditorium, which was absolutely packed. Roger Penrose enjoys some level of celebrity because he was written popular books. His fans in the audience were just gushing, and assumed his theory must be true. However, several physics professors from UBC were also in audience, and they were all very skeptical of his theory. Penrose claimed that “Hawking points” which are imprints left by black holes from the previous universe have already been observed in the CMB. In fact, no such thing has been observed. It reminded me of this article about Einstein

where an elderly physicist’s unsuccessful recent theories receive more attention because of their previous successful achievements from decades earlier. I do not want to sound like I’m criticizing Roger Penrose but he is 87 years old, and if you have ever had a family member that age, then you know what I’m talking about. I am not criticizing him. His fans in the audience used his theory as an excuse to promote their own crackpot nonsense. One woman in the audience asked whether “consciousness” could pass from the last universe into this universe. I do not blame Penrose for that. Whenever you give a popular lecture, there are going to be people like that in the audience. You just have to be polite when people in the audience ask questions like that.

In his talk, he used only hand drawn diagrams on transparencies. He drew a diagram representing this universe, and then extended the diagram to include an infinite number of universes before an after, despite there being no evidence for any others. This reminded me if Penrose diagrams, where he would draw a diagram representing a black hole, and then extend the diagram to include an infinite number of black holes connected to it, despite there being no evidence for any of the others.

The other comment I want to make is that these diagrams of quantum mechanics have inspired a form of poetry about quantum mechanics.

Posted by: Jeffery Winkler on April 17, 2019 11:47 PM | Permalink | Reply to this

Re: The ZX-Calculus for Stabilizer Quantum Mechanics

What about this paper? I believe this is what Roger Penrose means as proof.

Posted by: Karen Hart on July 15, 2019 2:49 AM | Permalink | Reply to this

Re: The ZX-Calculus for Stabilizer Quantum Mechanics

What about this paper? I believe this is what Roger Penrose means as proof.

Posted by: Karen Hart on July 15, 2019 5:37 AM | Permalink | Reply to this

Post a New Comment