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

ACM Transactions on Quantum Computing

Completeness of Graphical Languages for Mixed State Quantum Mechanics

Titouan Carette, Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart

Published Dec 21, 2021• 9 citations
Publisher

Abstract

There exist several graphical languages for quantum information processing, like quantum circuits, ZX-calculus, ZW-calculus, and so on. Each of these languages forms a †-symmetric monoidal category (†-SMC) and comes with an interpretation functor to the †-SMC of finite-dimensional Hilbert spaces. In recent years, one of the main achievements of the categorical approach to quantum mechanics has been to provide several equational theories for most of these graphical languages, making them complete for various fragments of pure quantum mechanics. We address the question of how to extend these languages beyond pure quantum mechanics to reason about mixed states and general quantum operations, i.e., completely positive maps. Intuitively, such an extension relies on the axiomatisation of a discard map that allows one to get rid of a quantum system, an operation that is not allowed in pure quantum mechanics. We introduce a new construction, the discard construction , which transforms any †-symmetric monoidal category into a symmetric monoidal category equipped with a discard map. Roughly speaking this construction consists in making any isometry causal. Using this construction, we provide an extension for several graphical languages that we prove to be complete for general quantum operations. However, this construction fails for some fringe cases like Clifford+T quantum mechanics, as the category does not have enough isometries.

DOI
10.1145/3464693

Related papers

Completeness of Graphical Languages for Mixed States Quantum Mechanics (Track B: Automata, Logic, Semantics, and Theory of Programming)

Titouan Carette, Emmanuel Jeandel, Simon Perdrix +1 more

There exist several graphical languages for quantum information processing, like quantum circuits, ZX-Calculus, ZW-Calculus, etc. Each of these languages forms a dagger-symmetric monoidal category (dagger-SMC) and comes with an interpretation functor to the dagger-SMC of (finite dimension) Hilbert spaces. In the recent years, one of the main achievements of the categorical approach to quantum mechanics has been to provide several equational theories for most of these graphical languages, making them complete for various fragments of pure quantum mechanics. We address the question of the extension of these languages beyond pure quantum mechanics, in order to reason on mixed states and general quantum operations, i.e. completely positive maps. Intuitively, such an extension relies on the axiomatisation of a discard map which allows one to get rid of a quantum system, operation which is not allowed in pure quantum mechanics. We introduce a new construction, the discard construction, which transforms any dagger-symmetric monoidal category into a symmetric monoidal category equipped with a discard map. Roughly speaking this construction consists in making any isometry causal. Using this construction we provide an extension for several graphical languages that we prove to be complete for general quantum operations. However this construction fails for some fringe cases like the Clifford+T quantum mechanics, as the category does not have enough isometries.

arXiv:1902.07143•Leibniz international proceedings in informatics•Jan 1, 2019•19 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

A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics

Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart

We introduce the first complete and approximately universal diagrammatic language for quantum mechanics. We make the ZX-Calculus, a diagrammatic language introduced by Coecke and Duncan, complete for the so-called Clifford+T quantum mechanics by adding two new axioms to the language. The completeness of the ZX-Calculus for Clifford+T quantum mechanics -- also called the π/4-fragment of the ZX-Calculus -- was one of the main open questions in categorical quantum mechanics. We prove the completeness of this fragment using the recently studied ZW-Calculus, a calculus dealing with integer matrices. We also prove that the π/4-fragment of the ZX-Calculus represents exactly all the matrices over some finite dimensional extension of the ring of dyadic rationals.

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

A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics

Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart

We introduce the first complete and approximately universal diagrammatic language for quantum mechanics. We make the ZX-Calculus, a diagrammatic language introduced by Coecke and Duncan, complete for the so-called Clifford+T quantum mechanics by adding two new axioms to the language. The completeness of the ZX-Calculus for Clifford+T quantum mechanics -- also called the π/4-fragment of the ZX-Calculus -- was one of the main open questions in categorical quantum mechanics. We prove the completeness of this fragment using the recently studied ZW-Calculus, a calculus dealing with integer matrices. We also prove that the π/4-fragment of the ZX-Calculus represents exactly all the matrices over some finite dimensional extension of the ring of dyadic rationals.

•May 31, 2017•110 citations

Complete Graphical Language for Hermiticity-Preserving Superoperators

Titouan Carette, Timothée Hoffreumon, Émile Larroque +1 more

Universal and complete graphical languages have been successfully designed for pure state quantum mechanics, corresponding to linear maps between Hilbert spaces, and mixed states quantum mechanics, corresponding to completely positive superoperators. In this paper, we go one step further and present a universal and complete graphical language for Hermiticity-preserving superoperators. Such a language opens the possibility of diagrammatic compositional investigations of antilinear transformations featured in various physical situations, such as the Choi-Jamiołkowski isomorphism, spin-flip, or entanglement witnesses. Our construction relies on an extension of the ZW-calculus exhibiting a normal form for Hermitian matrices.

arXiv:2302.04212•ACM/IEEE Symposium on Logic in Computer Science (LICS)•Jun 26, 2023•1 citation

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
There exist several graphical languages for quantum information processing, like quantum circuits, ZX-calculus, ZW-calculus, and so on. Each of these languages forms a †-symmetric monoidal category (†-SMC) and comes with an interpretation functor to the †-SMC of finite-dimensional Hilbert spaces. In recent years, one of the main achievements of the categorical approach to quantum mechanics has been to provide several equational theories for most of these graphical languages, making them complete for various fragments of pure quantum mechanics. We address the question of how to extend these languages beyond pure quantum mechanics to reason about mixed states and general quantum operations, i.e., completely positive maps. Intuitively, such an extension relies on the axiomatisation of a discard map that allows one to get rid of a quantum system, an operation that is not allowed in pure quantum mechanics. We introduce a new construction, the discard construction , which transforms any †-symmetric monoidal category into a symmetric monoidal category equipped with a discard map. Roughly speaking this construction consists in making any isometry causal. Using this construction, we provide an extension for several graphical languages that we prove to be complete for general quantum operations. However, this construction fails for some fringe cases like Clifford+T quantum mechanics, as the category does not have enough isometries.
There exist several graphical languages for quantum information processing, like quantum circuits, ZX-Calculus, ZW-Calculus, etc. Each of these languages forms a dagger-symmetric monoidal category (dagger-SMC) and comes with an interpretation functor to the dagger-SMC of (finite dimension) Hilbert spaces. In the recent years, one of the main achievements of the categorical approach to quantum mechanics has been to provide several equational theories for most of these graphical languages, making them complete for various fragments of pure quantum mechanics. We address the question of the extension of these languages beyond pure quantum mechanics, in order to reason on mixed states and general quantum operations, i.e. completely positive maps. Intuitively, such an extension relies on the axiomatisation of a discard map which allows one to get rid of a quantum system, operation which is not allowed in pure quantum mechanics. We introduce a new construction, the discard construction, which transforms any dagger-symmetric monoidal category into a symmetric monoidal category equipped with a discard map. Roughly speaking this construction consists in making any isometry causal. Using this construction we provide an extension for several graphical languages that we prove to be complete for general quantum operations. However this construction fails for some fringe cases like the Clifford+T quantum mechanics, as the category does not have enough isometries.
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.
We introduce the first complete and approximately universal diagrammatic language for quantum mechanics. We make the ZX-Calculus, a diagrammatic language introduced by Coecke and Duncan, complete for the so-called Clifford+T quantum mechanics by adding two new axioms to the language. The completeness of the ZX-Calculus for Clifford+T quantum mechanics -- also called the π/4-fragment of the ZX-Calculus -- was one of the main open questions in categorical quantum mechanics. We prove the completeness of this fragment using the recently studied ZW-Calculus, a calculus dealing with integer matrices. We also prove that the π/4-fragment of the ZX-Calculus represents exactly all the matrices over some finite dimensional extension of the ring of dyadic rationals.
We introduce the first complete and approximately universal diagrammatic language for quantum mechanics. We make the ZX-Calculus, a diagrammatic language introduced by Coecke and Duncan, complete for the so-called Clifford+T quantum mechanics by adding two new axioms to the language. The completeness of the ZX-Calculus for Clifford+T quantum mechanics -- also called the π/4-fragment of the ZX-Calculus -- was one of the main open questions in categorical quantum mechanics. We prove the completeness of this fragment using the recently studied ZW-Calculus, a calculus dealing with integer matrices. We also prove that the π/4-fragment of the ZX-Calculus represents exactly all the matrices over some finite dimensional extension of the ring of dyadic rationals.
Universal and complete graphical languages have been successfully designed for pure state quantum mechanics, corresponding to linear maps between Hilbert spaces, and mixed states quantum mechanics, corresponding to completely positive superoperators. In this paper, we go one step further and present a universal and complete graphical language for Hermiticity-preserving superoperators. Such a language opens the possibility of diagrammatic compositional investigations of antilinear transformations featured in various physical situations, such as the Choi-Jamiołkowski isomorphism, spin-flip, or entanglement witnesses. Our construction relies on an extension of the ZW-calculus exhibiting a normal form for Hermitian matrices.
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.