Diagrammatic Reasoning beyond Clifford+T Quantum Mechanics

TL;DR

This paper explores the expressive power of the ZX-Calculus beyond the Clifford+T fragment, demonstrating its completeness for linear diagrams in full quantum mechanics and proposing a simplified axiomatisation with one additional axiom.

Contribution

It extends the completeness of the ZX-Calculus to all linear diagrams in pure quantum mechanics and introduces a simpler axiomatisation with a single extra axiom.

Findings

ZX-Calculus is complete for all linear diagrams in full quantum mechanics.

A single non-linear axiom suffices to complete the axiomatisation.

Simpler axiomatisation than previous approaches.

Abstract

The ZX-Calculus is a graphical language for quantum mechanics. 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.