Researchers have developed a simplified axiomatic approach to quantum computation. By extending rig groupoids with two maps and three equations, they have created a model of quantum computing that is computationally universal and equationally sound, and complete for a variety of gate sets. The model reduces reasoning about quantum programs to manipulate the coherence conditions of rig categories. The team’s approach is a significant step towards making quantum computing more accessible and easier to understand.
A team of researchers from McMaster University, Canada, University of Edinburgh, UK, University of Southern Denmark, Denmark, and Indiana University, USA, have developed a semantic model of a universal classical reversible programming language over finite types. The team includes Jacques Carette, Chris Heunen, Robin Kaarsgaard, and Amr Sabry. They have proven that extending rig groupoids with just two maps and three equations about them results in a model of quantum computing that is computationally universal equationally sound and complete for a variety of gate sets.
The model consists of a rig groupoid equipped with two maps and three equations. The first map corresponds to an 8th root of the identity morphism on the unit 1. The second map corresponds to a square root of the symmetry on 1,1. As square roots are generally not unique and can sometimes even be trivial, the maps are constrained to satisfy a non-degeneracy axiom which is related to the Euler decomposition of the Hadamard gate.
The semantic construction is turned into an extension of a computationally universal quantum programming language equipped with an equational theory that is sound and complete concerning the Clifford gate set, the standard gate set of Clifford+T restricted to 2 qubits, and the computationally universal Gaussian Clifford+T gate set.
Just like in the classical case, quantum computing can be built up from booleans and associated operations. The quantum version of boolean negation is the X gate. The quantum circuit model also includes a gate, X, also known as the V gate, that is the square root of X.
The Euler decomposition expresses any 1-qubit unitary gate as a product of a global phase and three rotations along two fixed orthogonal axes. The quantum model has two additional morphisms. The map is a primitive 8th root of the identity, its semantics is partially specified by E1. The map V is the square root of boolean negation, its semantics is partially specified by E2.
This approach reduces reasoning about quantum programs to manipulating the coherence conditions of rig categories, extended with the axioms E1, E2, and E3. Many quantum equivalences follow similarly. For example, the proof that SS is equivalent to the Z gate follows by just the coherence conditions of rig categories.
The equational theory extracted from the semantic model is sound and complete with respect to arbitrary Clifford circuits, Clifford+T circuits of at most 2 qubits, and arbitrary Gaussian Clifford+T circuits. These completeness theorems form the main technical results of the research.
In the article “With a Few Square Roots, Quantum Computing Is as Easy as Pi,” published on January 5, 2024, authors Jacques Carette, Chris Heunen, Robin Kaarsgaard, and Amr Sabry explore the complexities of quantum computing. The article was published in the Proceedings of the ACM on programming languages. The full article can be accessed through its DOI reference https://doi.org/10.1145/3632861.