Completeness of the ZX-calculus - Wang, Q (2018)
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 Cliord+T quantum mechanics, which is approximatively universal for quantum computing, by restricting the ring of complex numbers to its subring corresponding to the Cliord+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 Cliord+T circuits by verifying the complete set of 17 circuit relations in diagrammatic rewriting. This is an important step towards efficient simplification of general n-qubit Cliord+T circuits, considering that we now have all the necessary rules for diagrammatical quantum reasoning and a very simple construction of Tooli gate within our axiomatisation framework, which is approximately universal for quantum computation together with the Hadamard gate. 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 Tooli gate, as well as equivalence-checking for the UMA gate.