A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics
Jeandel, Perdrix, and Vilmart add axioms that make the ZX-calculus complete for Clifford+T quantum mechanics.
Paper information (2018, LICS; preprint: 2017) — Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. arXiv:1705.11151
Work
The paper studies completeness of the ZX-calculus introduced by Coecke and Duncan for the Clifford+T fragment of quantum mechanics. It adds four axioms to the graphical language and uses the ZW-calculus to prove that, in this fragment, graphical equations capture all semantic equality. It also characterizes the matrix-ring structure represented by the fragment.
Contributions
- A complete axiomatisation of the ZX-calculus for Clifford+T quantum mechanics.
- Four additional axioms resolving completeness for this fragment.
- A completeness proof using the ZW-calculus.
- A characterization of the finite-dimensional matrices represented over a finite extension of the dyadic-rational ring.
Limits
Completeness concerns the Clifford+T fragment and the paper's graphical semantics; it does not automatically extend to arbitrary continuous parameters or noisy processes. Provability of graphical equality does not mean that an efficient rewrite will always be found, nor does it establish hardware implementation, compilation cost, or numerical-error guarantees.
Connections
The paper directly extends the ZX-calculus of Interacting Quantum Observables and connects it to the gate-level representation of Quantum Circuits. It can also be compared with Towards Large-Scale Functional Verification of Universal Quantum Circuits: this work proves equational completeness of a diagrammatic calculus, while the latter studies automated functional circuit verification at scale.
Original paper
Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart, A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics, LICS 2018. arXiv:1705.11151