© 2026 Aqora Quantum S.A.S.

Terms Privacy Legal Notice

arXiv:2602.09874

Simpler Presentations for Many Fragments of Quantum Circuits

Colin Blake

quant-phcs.LOSubmitted Feb 10, 2026• Announced Feb 11, 2026• 0 citations• Revised May 2, 2026 (v2)

v1 · Feb 10, 2026 v2 · May 2, 2026 v3 · Jul 25, 2026

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.

Journal reference: Leibniz Int. Proc. Inform. (LIPIcs) 378 (2026), 6:1-6:20
DOI: 10.4230/LIPIcs.FSCD.2026.6
Comments: accepted at FSCD 2026, to appear in LIPIcs

Related papers

A Complete and Natural Rule Set for Multi-Qutrit Clifford Circuits

Sarah Meng Li, Michele Mosca, Neil J. Ross +2 more

We present a complete set of rewrite rules for n-qutrit Clifford circuits where n is any non-negative integer.This is the first completeness result for any fragment of quantum circuits in odd prime dimensions.We first generalize Selinger's normal form for n-qubit Clifford circuits to the qutrit setting.Then, we present a rewrite system by which any Clifford circuit can be reduced to this normal form.We then simplify the rewrite rules in this procedure to a small natural set of rules, giving a clean presentation of the group of qutrit Clifford unitaries in terms of generators and relations.

arXiv:2508.14670•Electronic Proceedings in Theoretical Computer Science•Aug 19, 2025•2 citations

Quantum Circuit Completeness: Extensions and Simplifications

Alexandre Clément, Noé Delorme, Simon Perdrix +1 more

Although quantum circuits have been ubiquitous for decades in quantum computing, the first complete equational theory for quantum circuits has only recently been introduced. Completeness guarantees that any true equation on quantum circuits can be derived from the equational theory. We improve this completeness result in two ways: (i) We simplify the equational theory by proving that several rules can be derived from the remaining ones. In particular, two out of the three most intricate rules are removed, the third one being slightly simplified. (ii) The complete equational theory can be extended to quantum circuits with ancillae or qubit discarding, to represent respectively quantum computations using an additional workspace, and hybrid quantum computations. We show that the remaining intricate rule can be greatly simplified in these more expressive settings, leading to equational theories where all equations act on a bounded number of qubits. The development of simple and complete equational theories for expressive quantum circuit models opens new avenues for reasoning about quantum circuits. It provides strong formal foundations for various compiling tasks such as circuit optimisation, hardware constraint satisfaction and verification.

arXiv:2303.03117•Leibniz international proceedings in informatics•Mar 6, 2023•0 citations

Quantum Circuit Completeness: Extensions and Simplifications

Alexandre Clément, Noé Delorme, Simon Perdrix +1 more

Although quantum circuits have been ubiquitous for decades in quantum computing, the first complete equational theory for quantum circuits has only recently been introduced. Completeness guarantees that any true equation on quantum circuits can be derived from the equational theory.We improve this completeness result in two ways: (i) We simplify the equational theory by proving that several rules can be derived from the remaining ones. In particular, two out of the three most intricate rules are removed, the third one being slightly simplified. (ii) The complete equational theory can be extended to quantum circuits with ancillae or qubit discarding, to represent respectively quantum computations using an additional workspace, and hybrid quantum computations. We show that the remaining intricate rule can be greatly simplified in these more expressive settings, leading to equational theories where all equations act on a bounded number of qubits.The development of simple and complete equational theories for expressive quantum circuit models opens new avenues for reasoning about quantum circuits. It provides strong formal foundations for various compiling tasks such as circuit optimisation, hardware constraint satisfaction and verification.

•Jan 1, 2024•2 citations

How Many Quantum Circuit Identities Are Needed to Generate All Others?

Yuantian Ding, Nengkun Yu, Xiaokang Qiu

Abstract Quantum circuit optimizers use rewrite rules from circuit equivalences, yet prior work has identified thousands of such identities, creating substantial challenges for their storage, management, and effective application. For many widely used unitary gate sets, including Clifford+T, this apparent complexity is largely redundant, raising a fundamental question: How many quantum circuit identities are actually needed to generate all others? In this work, we provide strong evidence that a small pruned set of identities suffices to generate all circuit equivalences of bounded depth. Surprisingly, for circuits on up to nine qubits in which each side of an equality has depth at most ten, fewer than twenty identities are sufficient to derive all others, and for circuits on up to five qubits with depth at most ten, only 17 rules–each involving at most three qubits–are enough. These results enable significantly more compact and efficient rewriting systems for quantum compiler optimization and reveal underlying algebraic structure in common gate sets, showing that the vast majority of known circuit identities are consequences of a small foundational basis.

Lecture notes in computer science•Jan 1, 2026•0 citations

A Complete Equational Theory for Real-Clifford+CH Quantum Circuits

Alexandre Clément

We introduce a complete equational theory for the fragment of quantum circuits generated by the real Clifford gates plus the two-qubit controlled-Hadamard gate. That is, we give a simple set of equalities between circuits of this fragment, and prove that any other true equation can be derived from these. This is the first such completeness result for a finitely-generated, universal fragment of quantum circuits, with no parameterized gates and no need for ancillas.

quant-pharXiv:2602.06644•Feb 9, 2026•0 citations

Optimising Clifford Circuits with Quantomatic

Andrew Fagan, Ross Duncan

We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.

arXiv:1901.10114•Electronic Proceedings in Theoretical Computer Science•Jan 31, 2019•32 citations

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.

We present a complete set of rewrite rules for n-qutrit Clifford circuits where n is any non-negative integer.This is the first completeness result for any fragment of quantum circuits in odd prime dimensions.We first generalize Selinger's normal form for n-qubit Clifford circuits to the qutrit setting.Then, we present a rewrite system by which any Clifford circuit can be reduced to this normal form.We then simplify the rewrite rules in this procedure to a small natural set of rules, giving a clean presentation of the group of qutrit Clifford unitaries in terms of generators and relations.

Although quantum circuits have been ubiquitous for decades in quantum computing, the first complete equational theory for quantum circuits has only recently been introduced. Completeness guarantees that any true equation on quantum circuits can be derived from the equational theory. We improve this completeness result in two ways: (i) We simplify the equational theory by proving that several rules can be derived from the remaining ones. In particular, two out of the three most intricate rules are removed, the third one being slightly simplified. (ii) The complete equational theory can be extended to quantum circuits with ancillae or qubit discarding, to represent respectively quantum computations using an additional workspace, and hybrid quantum computations. We show that the remaining intricate rule can be greatly simplified in these more expressive settings, leading to equational theories where all equations act on a bounded number of qubits. The development of simple and complete equational theories for expressive quantum circuit models opens new avenues for reasoning about quantum circuits. It provides strong formal foundations for various compiling tasks such as circuit optimisation, hardware constraint satisfaction and verification.

Although quantum circuits have been ubiquitous for decades in quantum computing, the first complete equational theory for quantum circuits has only recently been introduced. Completeness guarantees that any true equation on quantum circuits can be derived from the equational theory.We improve this completeness result in two ways: (i) We simplify the equational theory by proving that several rules can be derived from the remaining ones. In particular, two out of the three most intricate rules are removed, the third one being slightly simplified. (ii) The complete equational theory can be extended to quantum circuits with ancillae or qubit discarding, to represent respectively quantum computations using an additional workspace, and hybrid quantum computations. We show that the remaining intricate rule can be greatly simplified in these more expressive settings, leading to equational theories where all equations act on a bounded number of qubits.The development of simple and complete equational theories for expressive quantum circuit models opens new avenues for reasoning about quantum circuits. It provides strong formal foundations for various compiling tasks such as circuit optimisation, hardware constraint satisfaction and verification.

Abstract Quantum circuit optimizers use rewrite rules from circuit equivalences, yet prior work has identified thousands of such identities, creating substantial challenges for their storage, management, and effective application. For many widely used unitary gate sets, including Clifford+T, this apparent complexity is largely redundant, raising a fundamental question: How many quantum circuit identities are actually needed to generate all others? In this work, we provide strong evidence that a small pruned set of identities suffices to generate all circuit equivalences of bounded depth. Surprisingly, for circuits on up to nine qubits in which each side of an equality has depth at most ten, fewer than twenty identities are sufficient to derive all others, and for circuits on up to five qubits with depth at most ten, only 17 rules–each involving at most three qubits–are enough. These results enable significantly more compact and efficient rewriting systems for quantum compiler optimization and reveal underlying algebraic structure in common gate sets, showing that the vast majority of known circuit identities are consequences of a small foundational basis.

We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.