The ZX-calculus is complete for stabilizer quantum mechanics

TL;DR

This paper proves that the ZX-calculus provides a complete graphical language for reasoning about stabilizer quantum mechanics, allowing all matrix-derived equalities to be derived pictorially.

Contribution

It establishes the completeness of the ZX-calculus specifically for stabilizer quantum mechanics, extending its utility beyond universality.

Findings

ZX-calculus is complete for stabilizer quantum mechanics

Diagrams can be brought into a normal form based on graph states

All matrix-based equalities can be derived graphically

Abstract

The ZX-calculus is a graphical calculus for reasoning about quantum systems and processes. It is known to be universal for pure state qubit quantum mechanics, meaning any pure state, unitary operation and post-selected pure projective measurement can be expressed in the ZX-calculus. The calculus is also sound, i.e. any equality that can be derived graphically can also be derived using matrix mechanics. Here, we show that the ZX-calculus is complete for pure qubit stabilizer quantum mechanics, meaning any equality that can be derived using matrices can also be derived pictorially. The proof relies on bringing diagrams into a normal form based on graph states and local Clifford operations.