A Complete Equational Theory for Quantum Circuits

TL;DR

This paper presents the first complete set of algebraic equations for quantum circuits, enabling precise circuit equivalence verification through proven soundness and completeness.

Contribution

It introduces a comprehensive equational theory for quantum circuits, linking them to linear optical circuits for proof of completeness.

Findings

The set of equations is sound and complete for quantum circuit equivalence.

Quantum circuits can be encoded into linear optical circuits for analysis.

The theory applies to multi-controlled gates built from elementary gates.

Abstract

We introduce the first complete equational theory for quantum circuits. More precisely, we introduce a set of circuit equations that we prove to be sound and complete: two circuits represent the same unitary map if and only if they can be transformed one into the other using the equations. The proof is based on the properties of multi-controlled gates -- that are defined using elementary gates -- together with an encoding of quantum circuits into linear optical circuits, which have been proved to have a complete axiomatisation.