Completeness of the ZX-calculus

TL;DR

This paper establishes the first complete axiomatisation of the ZX-calculus for pure qubit quantum mechanics, enabling diagrammatic reasoning and automation in quantum computing, with extensions to Clifford+T and qutrit systems.

Contribution

It provides the first complete ZX-calculus for pure qubit quantum mechanics by translating from the ZW-calculus, and extends completeness to Clifford+T and qutrit stabilizer systems.

Findings

First complete axiomatisation of ZX-calculus for pure qubit quantum mechanics.

Complete ZX-calculus for Clifford+T quantum mechanics derived from ZW-calculus.

Proved completeness of ZX-calculus with 9 rules for 2-qubit Clifford+T circuits.

Abstract

The ZX-calculus is an intuitive but also mathematically strict graphical language for quantum computing, which is especially powerful for the framework of quantum circuits. Completeness of the ZX-calculus means any equality of matrices with size powers of $n$ can be derived purely diagrammatically. In this thesis, we give the first complete axiomatisation the ZX-calculus for the overall pure qubit quantum mechanics, via a translation from the completeness result of another graphical language for quantum computing -- the ZW-calculus. This paves the way for automated pictorial quantum computing, with the aid of some software like Quantomatic. Based on this universal completeness, we directly obtain a complete axiomatisation of the ZX-calculus for the Clifford+T quantum mechanics, which is approximatively universal for quantum computing, by restricting the ring of complex numbers to its subring corresponding to the Clifford+T fragment resting on the completeness theorem of the ZW-calculus for arbitrary commutative ring. Furthermore, we prove the completeness of the ZX-calculus (with just 9 rules) for 2-qubit Clifford+T circuits by verifying the complete set of 17 circuit relations in diagrammatic rewriting. In addition to completeness results within the qubit related formalism, we extend the completeness of the ZX-calculus for qubit stabilizer quantum mechanics to the qutrit stabilizer system. Finally, we show with some examples the application of the ZX-calculus to the proof of generalised supplementarity, the representation of entanglement classification and Toffoli gate, as well as equivalence-checking for the UMA gate.