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:2405.10896 · Electronic Proceedings in Theoretical Computer Science

ZX-calculus is Complete for Finite-Dimensional Hilbert Spaces

Boldizsár Poór, Razin Abdulrauf Shaikh, Quanlong Wang

Published Aug 19, 2025• 2 citations
arXivHTMLPDF

Abstract

The ZX-calculus is a graphical language for reasoning about quantum computing and quantum information theory.As a complete graphical language, it incorporates a set of axioms rich enough to derive any equation of the underlying formalism.While completeness of the ZX-calculus has been established for qubits and the Clifford fragment of prime-dimensional qudits, universal completeness beyond two-level systems has remained unproven until now.In this paper, we present a proof establishing the completeness of finite-dimensional ZX-calculus, incorporating only the mixeddimensional Z-spider and the qudit X-spider as generators.Our approach builds on the completeness of another graphical language, the finite-dimensional ZW-calculus, with direct translations between these two calculi.By proving its completeness, we lay a solid foundation for the ZX-calculus as a versatile tool not only for quantum computation but also for various fields within finite-dimensional quantum theory.

DOI
10.4204/eptcs.426.5

Related papers

Completeness for arbitrary finite dimensions of ZXW-calculus, a unifying calculus

Boldizsár Poór, Quanlong Wang, Razin Abdulrauf Shaikh +3 more

The ZX-calculus is a universal graphical language for qubit quantum computation, meaning that every linear map between qubits can be expressed in the ZX-calculus. Furthermore, it is a complete graphical rewrite system: any equation involving linear maps that is derivable in the Hilbert space formalism for quantum theory can also be derived in the calculus by rewriting. It has widespread usage within quantum industry and academia for a variety of tasks such as quantum circuit optimisation, error-correction, and education.The ZW-calculus is an alternative universal graphical language that is also complete for qubit quantum computing. In fact, its completeness was used to prove that the ZX-calculus is universally complete. This calculus has advanced how quantum circuits are compiled into photonic hardware architectures in the industry.Recently, by combining these two calculi, a new calculus has emerged for qubit quantum computation, the ZXW-calculus. Using this calculus, graphical-differentiation, -integration, and -exponentiation were made possible, thus enabling the development of novel techniques in the domains of quantum machine learning and quantum chemistry.Here, we generalise the ZXW-calculus to arbitrary finite dimensions, that is, to qudits. Moreover, we prove that this graphical rewrite system is complete for any finite dimension. This is the first completeness result for any universal graphical language beyond qubits.

arXiv:2302.12135•ACM/IEEE Symposium on Logic in Computer Science (LICS)•Jun 26, 2023•13 citations

Completeness of the ZX-Calculus

Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart

The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. It comes equipped with an equational presentation. We focus here on a very important property of the language: completeness, which roughly ensures the equational theory captures all of quantum mechanics. We first improve on the known-to-be-complete presentation for the so-called Clifford fragment of the language - a restriction that is not universal - by adding some axioms. Thanks to a system of back-and-forth translation between the ZX-Calculus and a third-party complete graphical language, we prove that the provided axiomatisation is complete for the first approximately universal fragment of the language, namely Clifford+T. We then prove that the expressive power of this presentation, though aimed at achieving completeness for the aforementioned restriction, extends beyond Clifford+T, to a class of diagrams that we call linear with Clifford+T constants. We use another version of the third-party language - and an adapted system of back-and-forth translation - to complete the language for the ZX-Calculus as a whole, that is, with no restriction. We briefly discuss the added axioms, and finally, we provide a complete axiomatisation for an altered version of the language which involves an additional generator, making the presentation simpler.

arXiv:1903.06035•Logical Methods in Computer Science•Jun 4, 2020•18 citations

Completeness of qufinite ZXW calculus, a graphical language for finite-dimensional quantum theory

Quanlong Wang, Boldizsár Poór, Shaikh, Razin A.

Finite-dimensional quantum theory serves as the theoretical foundation for quantum information and computation. Mathematically, it is formalized in the category FHilb, comprising all finite-dimensional Hilbert spaces and linear maps between them. However, there has not been a graphical language for FHilb which is both universal and complete and thus incorporates a set of rules rich enough to derive any equality of the underlying formalism solely by rewriting. In this paper, we introduce the qufinite ZXW calculus - a graphical language for reasoning about finite-dimensional quantum theory. We set up a unique normal form to represent an arbitrary tensor and prove the completeness of this calculus by demonstrating that any qufinite ZXW diagram can be rewritten into its normal form. This result implies the equivalence of the qufinite ZXW calculus and the category FHilb, leading to a purely diagrammatic framework for finite-dimensional quantum theory with the same reasoning power. In addition, we identify several domains where the application of the qufinite ZXW calculus holds promise. These domains include spin networks, interacting mixed-dimensional systems in quantum chemistry, quantum programming, high-level description of quantum algorithms, and mixed-dimensional quantum computing. Our work paves the way for a comprehensive diagrammatic description of quantum physics, opening the doors of this area to the wider public.

arXiv:2309.13014•Sep 22, 2023•1 citation

A non-anyonic qudit ZW-calculus

Quanlong Wang

ZW-calculus is a useful graphical language for pure qubit quantum computing. It is via the translation of the completeness of ZW-calculus that the first proof of completeness of ZX-calculus was obtained. A d-level generalisation of qubit ZW-calculus (anyonic qudit ZW-calculus) has been given in [Hadzihasanovic 2017] which is universal for pure qudit quantum computing. However, the interpretation of the W spider in this type of ZW-calculus has so-called q-binomial coefficients involved, thus makes computation quite complicated. In this paper, we give a new type of qudit ZW-calculus which has generators and rewriting rules similar to that of the qubit ZW-calculus. Especially, the Z spider is exactly the same as that of the qudit ZX-calculus as given in [Wang 2021], and the new W spider has much simpler interpretation as a linear map. Furthermore, we establish a translation between this qudit ZW-calculus and the qudit ZX-calculus which is universal as shown in [Wang 2021], therefore this qudit ZW-calculus is also universal for pure qudit quantum computing.

arXiv:2109.11285•Sep 23, 2021•4 citations

Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics

Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart

The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. An axiomatisation has recently been proven to be complete for an approximatively universal fragment of quantum mechanics, the so-called Clifford+T fragment. We focus here on the expressive power of this axiomatisation beyond Clifford+T Quantum mechanics. We consider the full pure qubit quantum mechanics, and mainly prove two results: (i) First, the axiomatisation for Clifford+T quantum mechanics is also complete for all equations involving some kind of linear diagrams. The linearity of the diagrams reflects the phase group structure, an essential feature of the ZX-calculus. In particular all the axioms of the ZX-calculus are involving linear diagrams. (ii) We also show that the axiomatisation for Clifford+T is not complete in general but can be completed by adding a single (non linear) axiom, providing a simpler axiomatisation of the ZX-calculus for pure quantum mechanics than the one recently introduced by Ng&Wang.

arXiv:1801.10142•ACM/IEEE Symposium on Logic in Computer Science (LICS)•Jun 27, 2018•55 citations

Minimality in Finite-Dimensional ZW-Calculi

Marc de Visme, Renaud Vilmart

The ZW-calculus is a graphical language capable of representing 2-dimensional quantum systems (qubit) through its diagrams, and manipulating them through its equational theory. We extend the formalism to accommodate finite dimensional Hilbert spaces beyond qubit systems. First we define a qu$d$it version of the language, where all systems have the same arbitrary finite dimension $d$, and show that the provided equational theory is both complete -- i.e. semantical equivalence is entirely captured by the equations -- and minimal -- i.e. none of the equations are consequences of the others. We then extend the graphical language further to allow for mixed-dimensional systems. We again show the completeness and minimality of the provided equational theory.

arXiv:2401.16225•Leibniz international proceedings in informatics•Jan 29, 2024•1 citation
The ZX-calculus is a graphical language for reasoning about quantum computing and quantum information theory.As a complete graphical language, it incorporates a set of axioms rich enough to derive any equation of the underlying formalism.While completeness of the ZX-calculus has been established for qubits and the Clifford fragment of prime-dimensional qudits, universal completeness beyond two-level systems has remained unproven until now.In this paper, we present a proof establishing the completeness of finite-dimensional ZX-calculus, incorporating only the mixeddimensional Z-spider and the qudit X-spider as generators.Our approach builds on the completeness of another graphical language, the finite-dimensional ZW-calculus, with direct translations between these two calculi.By proving its completeness, we lay a solid foundation for the ZX-calculus as a versatile tool not only for quantum computation but also for various fields within finite-dimensional quantum theory.
The ZX-calculus is a universal graphical language for qubit quantum computation, meaning that every linear map between qubits can be expressed in the ZX-calculus. Furthermore, it is a complete graphical rewrite system: any equation involving linear maps that is derivable in the Hilbert space formalism for quantum theory can also be derived in the calculus by rewriting. It has widespread usage within quantum industry and academia for a variety of tasks such as quantum circuit optimisation, error-correction, and education.The ZW-calculus is an alternative universal graphical language that is also complete for qubit quantum computing. In fact, its completeness was used to prove that the ZX-calculus is universally complete. This calculus has advanced how quantum circuits are compiled into photonic hardware architectures in the industry.Recently, by combining these two calculi, a new calculus has emerged for qubit quantum computation, the ZXW-calculus. Using this calculus, graphical-differentiation, -integration, and -exponentiation were made possible, thus enabling the development of novel techniques in the domains of quantum machine learning and quantum chemistry.Here, we generalise the ZXW-calculus to arbitrary finite dimensions, that is, to qudits. Moreover, we prove that this graphical rewrite system is complete for any finite dimension. This is the first completeness result for any universal graphical language beyond qubits.
The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. It comes equipped with an equational presentation. We focus here on a very important property of the language: completeness, which roughly ensures the equational theory captures all of quantum mechanics. We first improve on the known-to-be-complete presentation for the so-called Clifford fragment of the language - a restriction that is not universal - by adding some axioms. Thanks to a system of back-and-forth translation between the ZX-Calculus and a third-party complete graphical language, we prove that the provided axiomatisation is complete for the first approximately universal fragment of the language, namely Clifford+T. We then prove that the expressive power of this presentation, though aimed at achieving completeness for the aforementioned restriction, extends beyond Clifford+T, to a class of diagrams that we call linear with Clifford+T constants. We use another version of the third-party language - and an adapted system of back-and-forth translation - to complete the language for the ZX-Calculus as a whole, that is, with no restriction. We briefly discuss the added axioms, and finally, we provide a complete axiomatisation for an altered version of the language which involves an additional generator, making the presentation simpler.
Finite-dimensional quantum theory serves as the theoretical foundation for quantum information and computation. Mathematically, it is formalized in the category FHilb, comprising all finite-dimensional Hilbert spaces and linear maps between them. However, there has not been a graphical language for FHilb which is both universal and complete and thus incorporates a set of rules rich enough to derive any equality of the underlying formalism solely by rewriting. In this paper, we introduce the qufinite ZXW calculus - a graphical language for reasoning about finite-dimensional quantum theory. We set up a unique normal form to represent an arbitrary tensor and prove the completeness of this calculus by demonstrating that any qufinite ZXW diagram can be rewritten into its normal form. This result implies the equivalence of the qufinite ZXW calculus and the category FHilb, leading to a purely diagrammatic framework for finite-dimensional quantum theory with the same reasoning power. In addition, we identify several domains where the application of the qufinite ZXW calculus holds promise. These domains include spin networks, interacting mixed-dimensional systems in quantum chemistry, quantum programming, high-level description of quantum algorithms, and mixed-dimensional quantum computing. Our work paves the way for a comprehensive diagrammatic description of quantum physics, opening the doors of this area to the wider public.
ZW-calculus is a useful graphical language for pure qubit quantum computing. It is via the translation of the completeness of ZW-calculus that the first proof of completeness of ZX-calculus was obtained. A d-level generalisation of qubit ZW-calculus (anyonic qudit ZW-calculus) has been given in [Hadzihasanovic 2017] which is universal for pure qudit quantum computing. However, the interpretation of the W spider in this type of ZW-calculus has so-called q-binomial coefficients involved, thus makes computation quite complicated. In this paper, we give a new type of qudit ZW-calculus which has generators and rewriting rules similar to that of the qubit ZW-calculus. Especially, the Z spider is exactly the same as that of the qudit ZX-calculus as given in [Wang 2021], and the new W spider has much simpler interpretation as a linear map. Furthermore, we establish a translation between this qudit ZW-calculus and the qudit ZX-calculus which is universal as shown in [Wang 2021], therefore this qudit ZW-calculus is also universal for pure qudit quantum computing.
The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. An axiomatisation has recently been proven to be complete for an approximatively universal fragment of quantum mechanics, the so-called Clifford+T fragment. We focus here on the expressive power of this axiomatisation beyond Clifford+T Quantum mechanics. We consider the full pure qubit quantum mechanics, and mainly prove two results: (i) First, the axiomatisation for Clifford+T quantum mechanics is also complete for all equations involving some kind of linear diagrams. The linearity of the diagrams reflects the phase group structure, an essential feature of the ZX-calculus. In particular all the axioms of the ZX-calculus are involving linear diagrams. (ii) We also show that the axiomatisation for Clifford+T is not complete in general but can be completed by adding a single (non linear) axiom, providing a simpler axiomatisation of the ZX-calculus for pure quantum mechanics than the one recently introduced by Ng&Wang.
The ZW-calculus is a graphical language capable of representing 2-dimensional quantum systems (qubit) through its diagrams, and manipulating them through its equational theory. We extend the formalism to accommodate finite dimensional Hilbert spaces beyond qubit systems. First we define a qudddit version of the language, where all systems have the same arbitrary finite dimension ddd, and show that the provided equational theory is both complete -- i.e. semantical equivalence is entirely captured by the equations -- and minimal -- i.e. none of the equations are consequences of the others. We then extend the graphical language further to allow for mixed-dimensional systems. We again show the completeness and minimality of the provided equational theory.