Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:1507.03854 · Electronic Proceedings in Theoretical Computer Science

Making the stabilizer ZX-calculus complete for scalars

Miriam Backens

Published Nov 4, 2015• 35 citations
arXivHTMLPDF

Abstract

The ZX-calculus is a graphical language for quantum processes with built-in rewrite rules. The rewrite rules allow equalities to be derived entirely graphically, leading to the question of completeness: can any equality that is derivable using matrices also be derived graphically? The ZX-calculus is known to be complete for scalar-free pure qubit stabilizer quantum mechanics, meaning any equality between two pure stabilizer operators that is true up to a non-zero scalar factor can be derived using the graphical rewrite rules. Here, we replace those scalar-free rewrite rules with correctly scaled ones and show that, by adding one new diagram element and a new rewrite rule, the calculus can be made complete for pure qubit stabilizer quantum mechanics with scalars. This completeness property allows amplitudes and probabilities to be calculated entirely graphically. We also explicitly consider stabilizer zero diagrams, i.e. diagrams that represent a zero matrix, and show that two new rewrite rules suffice to make the calculus complete for those.

DOI
10.4204/eptcs.195.2

Related papers

The ZX-calculus is complete for stabilizer quantum mechanics

Miriam Backens

The ZX-calculus is a graphical calculus for reasoning about quantum systems and processes. It is known to be universal for pure state qubit quantum mechanics (QM), meaning any pure state, unitary operation and post-selected pure projective measurement can be expressed in the ZX-calculus. The calculus is also sound , i.e. any equality that can be derived graphically can also be derived using matrix mechanics. Here, we show that the ZX-calculus is complete for pure qubit stabilizer QM, meaning any equality that can be derived using matrices can also be derived pictorially. The proof relies on bringing diagrams into a normal form based on graph states and local Clifford operations.

arXiv:1307.7025•New Journal of Physics•Sep 17, 2014•122 citations

Towards a Minimal Stabilizer ZX-calculus

Miriam Backens, Simon Perdrix, Quanlong Wang

The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics. The language is sound and complete: one can transform a stabilizer ZX-diagram into another one using the graphical rewrite rules if and only if these two diagrams represent the same quantum evolution or quantum state. We previously showed that the stabilizer ZX-calculus can be simplified by reducing the number of rewrite rules, without losing the property of completeness [Backens, Perdrix & Wang, EPTCS 236:1--20, 2017]. Here, we show that most of the remaining rules of the language are indeed necessary. We do however leave as an open question the necessity of two rules. These include, surprisingly, the bialgebra rule, which is an axiomatisation of complementarity, the cornerstone of the ZX-calculus. Furthermore, we show that a weaker ambient category -- a braided autonomous category instead of the usual compact closed category -- is sufficient to recover the meta rule 'only connectivity matters', even without assuming any symmetries of the generators.

arXiv:1709.08903•Logical Methods in Computer Science•Dec 22, 2020•6 citations

Towards a Minimal Stabilizer ZX-calculus

Miriam Backens, Simon Perdrix, Quanlong Wang

The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics. The language is sound and complete: one can transform a stabilizer ZX-diagram into another one using the graphical rewrite rules if and only if these two diagrams represent the same quantum evolution or quantum state. We previously showed that the stabilizer ZX-calculus can be simplified by reducing the number of rewrite rules, without losing the property of completeness [Backens, Perdrix & Wang, EPTCS 236:1--20, 2017]. Here, we show that most of the remaining rules of the language are indeed necessary. We do however leave as an open question the necessity of two rules. These include, surprisingly, the bialgebra rule, which is an axiomatisation of complementarity, the cornerstone of the ZX-calculus. Furthermore, we show that a weaker ambient category -- a braided autonomous category instead of the usual compact closed category -- is sufficient to recover the meta rule 'only connectivity matters', even without assuming any symmetries of the generators.

Logical Methods in Computer Science•Sep 27, 2017•5 citations

A Simplified Stabilizer ZX-calculus

Miriam Backens, Simon Perdrix, Quanlong Wang

The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics.The language is sound and complete: a stabilizer ZX-diagram can be transformed into another one if and only if these two diagrams represent the same quantum evolution or quantum state. We show that the stabilizer ZX-calculus can be simplified, removing unnecessary equations while keeping only the essential axioms which potentially capture fundamental structures of quantum mechanics. We thus give a significantly smaller set of axioms and prove that meta-rules like 'colour symmetry' and 'upside-down symmetry', which were considered as axioms in previous versions of the language, can in fact be derived. In particular, we show that the additional symbol and one of the rules which had been recently introduced to keep track of scalars (diagrams with no inputs or outputs) are not necessary.

arXiv:1602.04744•Electronic Proceedings in Theoretical Computer Science•Jan 1, 2017•28 citations

The ZX-Calculus is Canonical in the Heisenberg Picture for Stabilizer Quantum Mechanics

Jacob Biamonte, Aly Nasrallah

In 2008 Coecke and Duncan proposed the graphical ZX-calculus rewrite system which came to formalize reasoning with quantum circuits, measurements and quantum states. The ZX-calculus is sound for qubit quantum mechanics. Hence, equality of diagrams under ZX-equivalent transformations lifts to an equality of corresponding equations over matrices. Conversely, in 2014 Backens proved completeness, establishing that any derivation done in stabilizer quantum mechanics with matrices can be derived graphically using the ZX-calculus. A graphical rewrite system that is both confluent and also terminates uniquely is called canonical: Applying alternate sequences of rewrites to the same initial diagram, a rewrite system is confluent whenever all resulting diagrams can be manipulated to establish graphical equivalence. Here we show that a reduced ZX-rewrite system is already confluent in the Heisenberg picture for stabilizer quantum mechanics. Moreover, any application of a subset of ZX-rewrites terminates uniquely and irrespective of the order of term rewrites in the Heisenberg picture for stabilizer quantum mechanics. The ZX-system is hence Heisenberg-canonical for stabiliser quantum mechanics. For a stabilizer circuit on $n$-qubits with $l$ single-qubit gates and $g$ two-qubit gates, the circuit output can be derived graphically in the Heisenberg picture using no more than $(\frac{1}{2}\cdot g+l)\cdot n$ graphical rewrites, thereby providing a graphical proof of the Gottesman-Knill theorem. Finally, we establish that each stabilizer state described by a Clifford circuit gives rise to a non-negative parent Hamiltonian with $n+1$ terms and a one-dimensional kernel spanned by the corresponding stabilizer state. Such parent Hamiltonians can be derived with $\mathcal{O}(t\cdot n)$ graphical rewrites for a low energy state prepared by a $t$-gate Clifford circuit.

arXiv:2301.05717•Jan 13, 2023•0 citations

Completeness for flow-preserving rewrite rules

Miriam Backens, Simon Perdrix

Complete sets of graphical rewrite rules enable fully graphical reasoning about quantum computations and have been an area of active research for more than a decade. Many recent applications of the ZX-calculus have made use of the close correspondence between ZX-diagrams and computations in the one-way model of measurement-based quantum computation. In this model, various kinds of flow properties ensure deterministic implementability; for ZX-diagrams, these same properties allow efficient translation into quantum circuits (a problem that is known to be #P-hard in general). Therefore, flow-preserving ZX-calculus rewrite rules are of strong interest. Here, we extend the set of flow-preserving rules appearing in the literature with a few new rules and extensions of existing rules. We then show that the resulting rule set is complete for all flow-preserving translations between ZX-diagrams of appropriate form. The proof employs a manifestly flow-preserving equivalent of circuit extraction, where a diagram with gflow is transformed, using only flow-preserving rewrite rules, into a diagram with causal flow.

quant-pharXiv:2608.13035•Aug 14, 2026•0 citations
The ZX-calculus is a graphical language for quantum processes with built-in rewrite rules. The rewrite rules allow equalities to be derived entirely graphically, leading to the question of completeness: can any equality that is derivable using matrices also be derived graphically? The ZX-calculus is known to be complete for scalar-free pure qubit stabilizer quantum mechanics, meaning any equality between two pure stabilizer operators that is true up to a non-zero scalar factor can be derived using the graphical rewrite rules. Here, we replace those scalar-free rewrite rules with correctly scaled ones and show that, by adding one new diagram element and a new rewrite rule, the calculus can be made complete for pure qubit stabilizer quantum mechanics with scalars. This completeness property allows amplitudes and probabilities to be calculated entirely graphically. We also explicitly consider stabilizer zero diagrams, i.e. diagrams that represent a zero matrix, and show that two new rewrite rules suffice to make the calculus complete for those.
The ZX-calculus is a graphical calculus for reasoning about quantum systems and processes. It is known to be universal for pure state qubit quantum mechanics (QM), meaning any pure state, unitary operation and post-selected pure projective measurement can be expressed in the ZX-calculus. The calculus is also sound , i.e. any equality that can be derived graphically can also be derived using matrix mechanics. Here, we show that the ZX-calculus is complete for pure qubit stabilizer QM, meaning any equality that can be derived using matrices can also be derived pictorially. The proof relies on bringing diagrams into a normal form based on graph states and local Clifford operations.
The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics. The language is sound and complete: one can transform a stabilizer ZX-diagram into another one using the graphical rewrite rules if and only if these two diagrams represent the same quantum evolution or quantum state. We previously showed that the stabilizer ZX-calculus can be simplified by reducing the number of rewrite rules, without losing the property of completeness [Backens, Perdrix & Wang, EPTCS 236:1--20, 2017]. Here, we show that most of the remaining rules of the language are indeed necessary. We do however leave as an open question the necessity of two rules. These include, surprisingly, the bialgebra rule, which is an axiomatisation of complementarity, the cornerstone of the ZX-calculus. Furthermore, we show that a weaker ambient category -- a braided autonomous category instead of the usual compact closed category -- is sufficient to recover the meta rule 'only connectivity matters', even without assuming any symmetries of the generators.
The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics. The language is sound and complete: one can transform a stabilizer ZX-diagram into another one using the graphical rewrite rules if and only if these two diagrams represent the same quantum evolution or quantum state. We previously showed that the stabilizer ZX-calculus can be simplified by reducing the number of rewrite rules, without losing the property of completeness [Backens, Perdrix & Wang, EPTCS 236:1--20, 2017]. Here, we show that most of the remaining rules of the language are indeed necessary. We do however leave as an open question the necessity of two rules. These include, surprisingly, the bialgebra rule, which is an axiomatisation of complementarity, the cornerstone of the ZX-calculus. Furthermore, we show that a weaker ambient category -- a braided autonomous category instead of the usual compact closed category -- is sufficient to recover the meta rule 'only connectivity matters', even without assuming any symmetries of the generators.
The stabilizer ZX-calculus is a rigorous graphical language for reasoning about quantum mechanics.The language is sound and complete: a stabilizer ZX-diagram can be transformed into another one if and only if these two diagrams represent the same quantum evolution or quantum state. We show that the stabilizer ZX-calculus can be simplified, removing unnecessary equations while keeping only the essential axioms which potentially capture fundamental structures of quantum mechanics. We thus give a significantly smaller set of axioms and prove that meta-rules like 'colour symmetry' and 'upside-down symmetry', which were considered as axioms in previous versions of the language, can in fact be derived. In particular, we show that the additional symbol and one of the rules which had been recently introduced to keep track of scalars (diagrams with no inputs or outputs) are not necessary.
In 2008 Coecke and Duncan proposed the graphical ZX-calculus rewrite system which came to formalize reasoning with quantum circuits, measurements and quantum states. The ZX-calculus is sound for qubit quantum mechanics. Hence, equality of diagrams under ZX-equivalent transformations lifts to an equality of corresponding equations over matrices. Conversely, in 2014 Backens proved completeness, establishing that any derivation done in stabilizer quantum mechanics with matrices can be derived graphically using the ZX-calculus. A graphical rewrite system that is both confluent and also terminates uniquely is called canonical: Applying alternate sequences of rewrites to the same initial diagram, a rewrite system is confluent whenever all resulting diagrams can be manipulated to establish graphical equivalence. Here we show that a reduced ZX-rewrite system is already confluent in the Heisenberg picture for stabilizer quantum mechanics. Moreover, any application of a subset of ZX-rewrites terminates uniquely and irrespective of the order of term rewrites in the Heisenberg picture for stabilizer quantum mechanics. The ZX-system is hence Heisenberg-canonical for stabiliser quantum mechanics. For a stabilizer circuit on nnn-qubits with lll single-qubit gates and ggg two-qubit gates, the circuit output can be derived graphically in the Heisenberg picture using no more than (12⋅g+l)⋅n(\frac{1}{2}\cdot g+l)\cdot n(21​⋅g+l)⋅n graphical rewrites, thereby providing a graphical proof of the Gottesman-Knill theorem. Finally, we establish that each stabilizer state described by a Clifford circuit gives rise to a non-negative parent Hamiltonian with n+1n+1n+1 terms and a one-dimensional kernel spanned by the corresponding stabilizer state. Such parent Hamiltonians can be derived with O(t⋅n)\mathcal{O}(t\cdot n)O(t⋅n) graphical rewrites for a low energy state prepared by a ttt-gate Clifford circuit.
Complete sets of graphical rewrite rules enable fully graphical reasoning about quantum computations and have been an area of active research for more than a decade. Many recent applications of the ZX-calculus have made use of the close correspondence between ZX-diagrams and computations in the one-way model of measurement-based quantum computation. In this model, various kinds of flow properties ensure deterministic implementability; for ZX-diagrams, these same properties allow efficient translation into quantum circuits (a problem that is known to be #P-hard in general). Therefore, flow-preserving ZX-calculus rewrite rules are of strong interest. Here, we extend the set of flow-preserving rules appearing in the literature with a few new rules and extensions of existing rules. We then show that the resulting rule set is complete for all flow-preserving translations between ZX-diagrams of appropriate form. The proof employs a manifestly flow-preserving equivalent of circuit extraction, where a diagram with gflow is transformed, using only flow-preserving rewrite rules, into a diagram with causal flow.