© 2026 Aqora Quantum S.A.S.

Terms Privacy Legal Notice

arXiv:2311.07476 · ACM/IEEE Symposium on Logic in Computer Science (LICS)

Minimal Equational Theories for Quantum Circuits

Alexandre Clément, Noé Delorme, Simon Perdrix

Published Jun 21, 2024• 3 citations

Abstract

We introduce the first minimal and complete equational theory for quantum circuits. Hence, we show that any true equation on quantum circuits can be derived from simple rules, all of them being standard except a novel but intuitive one which states that a multi-control 2π rotation is nothing but the identity. Our work improves on the recent complete equational theories for quantum circuits, by getting rid of several rules including a fairly impractical one. One of our main contributions is to prove the minimality of the equational theory, i.e. none of the rules can be derived from the other ones. More generally, we demonstrate that any complete equational theory on quantum circuits (when all gates are unitary) requires rules acting on an unbounded number of qubits. Finally, we also simplify the complete equational theories for quantum circuits with ancillary qubits and/or qubit discarding.

DOI: 10.1145/3661814.3662088

Related papers

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

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

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

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 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

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.

•Jul 20, 2026•0 citations

We introduce the first minimal and complete equational theory for quantum circuits. Hence, we show that any true equation on quantum circuits can be derived from simple rules, all of them being standard except a novel but intuitive one which states that a multi-control 2π rotation is nothing but the identity. Our work improves on the recent complete equational theories for quantum circuits, by getting rid of several rules including a fairly impractical one. One of our main contributions is to prove the minimality of the equational theory, i.e. none of the rules can be derived from the other ones. More generally, we demonstrate that any complete equational theory on quantum circuits (when all gates are unitary) requires rules acting on an unbounded number of qubits. Finally, we also simplify the complete equational theories for quantum circuits with ancillary qubits and/or qubit discarding.

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.

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.