Simpler Presentations for Many Fragments of Quantum Circuits

TL;DR

This paper develops simplified, minimal equational presentations for various quantum circuit fragments, enhancing reasoning and verification by focusing on structural rules and removing redundancies.

Contribution

It provides minimal, near-Clifford algebraic frameworks for multiple quantum circuit fragments, improving the efficiency of circuit optimization and verification.

Findings

Achieved minimal presentations for qubit Clifford, real Clifford, and CNOT-dihedral fragments.

Transferred completeness theorems into PROP frameworks for these fragments.

Removed redundant non-structural rules, simplifying the equational reasoning process.

Abstract

Equational reasoning is central to quantum circuit optimisation and verification: one replaces subcircuits by provably equivalent ones using a fixed set of rewrite rules viewed as equations. A finite rule set is most informative when it separates the genuine algebra of a circuit fragment from the structural treatment of wires. This paper gives six near-Clifford fragments a common PROP treatment, where wire permutations are structural: qubit Clifford, real Clifford, Clifford+T (up to two qubits), Clifford+CS (up to three qubits), CNOT-dihedral, and qutrit Clifford. Starting from prior completeness theorems, we transfer completeness into this setting and remove redundant non-structural rules, then check minimality by separating interpretations tailored to individual axioms; the resulting presentations are minimal in all arities for qubit Clifford, real Clifford, and CNOT-dihedral, minimal in bounded ranges for the remaining fragments, and comparable by one transfer-and-separation pattern.