Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

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

Alexandre Clément

Published Jul 20, 2026• 0 citations
Publisher

Abstract

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.

DOI
10.4230/lipics.lics.2026.28

Related papers

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.

Leibniz international proceedings in informatics•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

Simpler Presentations for Many Fragments of Quantum Circuits

Colin Blake

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.

quant-pharXiv:2602.09874•Feb 11, 2026•0 citations

A Sound and Complete Equational Theory for 3-Qubit Toffoli-Hadamard Circuits

Matthew Amy, Neil J. Ross, Scott Wesley

We give a sound and complete equational theory for 3-qubit quantum circuits over the Toffoli-Hadamard gate set { X, CX, CCX, H }. That is, we introduce a collection of true equations among Toffoli-Hadamard circuits on three qubits that is sufficient to derive any other true equation between such circuits. To obtain this equational theory, we first consider circuits over the Toffoli-K gate set { X, CX, CCX, K }, where K = HxH. The Toffoli-Hadamard and Toffoli-K gate sets appear similar, but they are crucially different on exactly three qubits. Indeed, in this case, the former generates an infinite group of operators, while the latter generates the finite group of automorphisms of the well-known E8 lattice. We take advantage of this fact, and of the theory of automorphism groups of lattices, to obtain a sound and complete collection of equations for Toffoli-K circuits. We then extend this equational theory to one for Toffoli-Hadamard circuits by leveraging prior work of Li et al. on Toffoli-Hadamard operators.

arXiv:2407.11152•Electronic Proceedings in Theoretical Computer Science•Aug 9, 2024•0 citations

A Complete Equational Presentation of Qudit Circuits via Polycontrolled PROPs

Colin Blake

High-dimensional quantum computation needs a native circuit-level equational theory for qudits. We give the first finite schematic equational theory that is sound and complete for exact unitary qudit circuits in every finite dimension at least two. Circuits are built from local gates, sequential and parallel composition, and value-controls; equality is derivable exactly when the standard unitary denotations agree. For each dimension, a finite list of local bounded-arity axiom schemata presents the theory, and the diagrammatic shapes do not depend on d. Primitive value-control makes control on a chosen basis value part of the language, so local rules generate the internal algebra of controlled operations within the circuit PROP. This gives a finite, dimension-uniform basis for exact equational reasoning about qudit circuits.

quant-pharXiv:2602.09873•Leibniz international proceedings in informatics•Feb 11, 2026•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.

arXiv:2303.03117•Leibniz international proceedings in informatics•Mar 6, 2023•0 citations
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.
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 give a sound and complete equational theory for 3-qubit quantum circuits over the Toffoli-Hadamard gate set { X, CX, CCX, H }. That is, we introduce a collection of true equations among Toffoli-Hadamard circuits on three qubits that is sufficient to derive any other true equation between such circuits. To obtain this equational theory, we first consider circuits over the Toffoli-K gate set { X, CX, CCX, K }, where K = HxH. The Toffoli-Hadamard and Toffoli-K gate sets appear similar, but they are crucially different on exactly three qubits. Indeed, in this case, the former generates an infinite group of operators, while the latter generates the finite group of automorphisms of the well-known E8 lattice. We take advantage of this fact, and of the theory of automorphism groups of lattices, to obtain a sound and complete collection of equations for Toffoli-K circuits. We then extend this equational theory to one for Toffoli-Hadamard circuits by leveraging prior work of Li et al. on Toffoli-Hadamard operators.
High-dimensional quantum computation needs a native circuit-level equational theory for qudits. We give the first finite schematic equational theory that is sound and complete for exact unitary qudit circuits in every finite dimension at least two. Circuits are built from local gates, sequential and parallel composition, and value-controls; equality is derivable exactly when the standard unitary denotations agree. For each dimension, a finite list of local bounded-arity axiom schemata presents the theory, and the diagrammatic shapes do not depend on d. Primitive value-control makes control on a chosen basis value part of the language, so local rules generate the internal algebra of controlled operations within the circuit PROP. This gives a finite, dimension-uniform basis for exact equational reasoning about qudit circuits.
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.