Completeness of the ZX-Calculus. (arXiv:1903.06035v1 [quant-ph])

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 or
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.

Article web page: