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

arXiv:2506.06835 · Proceedings of the ACM on Programming Languages

Hadamard-Pi: Equational Quantum Programming

Wang Sheng Fang, Chris Heunen, Robin Kaarsgaard

Published Jan 8, 2026• 0 citations
arXivHTMLPDF

Abstract

Quantum computing offers advantages over classical computation, yet the precise features that set the two apart remain unclear. In the standard quantum circuit model, adding a 1-qubit basis-changing gate—commonly chosen to be the Hadamard gate—to a universal set of classical reversible gates yields computationally universal quantum computation. However, the computational behaviours enabled by this addition are not fully characterised. We give such a characterisation by introducing a small quantum programming language extending the universal classical reversible programming language Π with a single primitive corresponding to the Hadamard gate. The language comes equipped with a sound and complete categorical semantics that is specified by a purely equational theory. Completeness is shown by means of a novel finite presentation, and a corresponding synthesis algorithm, for the groups of orthogonal matrices with entries in the ring z [ 1 2 ] .

DOI
10.1145/3776647

Related papers

With a Few Square Roots, Quantum Computing Is as Easy as Pi

Jacques Carette, Chris Heunen, Robin Kaarsgaard +1 more

Rig groupoids provide a semantic model of Π , a universal classical reversible programming language over finite types. We prove that extending rig groupoids with just two maps and three equations about them results in a model of quantum computing that is computationally universal and equationally sound and complete for a variety of gate sets. 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 nondegeneracy axiom, which we relate to the Euler decomposition of the Hadamard gate. The semantic construction is turned into an extension of Π , called Π , that is a computationally universal quantum programming language equipped with an equational theory that is sound and complete with respect to the Clifford gate set, the standard gate set of Clifford+T restricted to ≤ 2 qubits, and the computationally universal Gaussian Clifford+T gate set.

arXiv:2310.14056•Proceedings of the ACM on Programming Languages•Jan 2, 2024•7 citations

The Quantum Effect: A Recipe for QuantumPi

Jacques Carette, Chris Heunen, Robin Kaarsgaard +1 more

Free categorical constructions characterise quantum computing as the combination of two copies of a reversible classical model, glued by the complementarity equations of classical structures. This recipe effectively constructs a computationally universal quantum programming language from two copies of Pi, the internal language of rig groupoids. The construction consists of Hughes' arrows. Thus answer positively the question whether a computational effect exists that turns reversible classical computation into quantum computation: the quantum effect. Measurements can be added by layering a further effect on top. Our construction also enables some reasoning about quantum programs (with or without measurement) through a combination of classical reasoning and reasoning about complementarity.

arXiv:2302.01885•Feb 3, 2023•1 citation

How to Bake a Quantum Π

Jacques Carette, Chris Heunen, Robin Kaarsgaard +1 more

We construct a computationally universal quantum programming language Quantum Π from two copies of Π , the internal language of rig groupoids. The first step constructs a pure (measurement-free) term language by interpreting each copy of Π in a generalisation of the category Unitary in which every morphism is “rotated” by a particular angle, and the two copies are amalgamated using a free categorical construction expressed as a computational effect. The amalgamated language only exhibits quantum behaviour for specific values of the rotation angles, a property which is enforced by imposing a small number of equations on the resulting category. The second step in the construction introduces measurements by layering an additional computational effect.

Proceedings of the ACM on Programming Languages•Aug 15, 2024•2 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

Free Quantum Computing

Jacques Carette, Chris Heunen, Robin Kaarsgaard +2 more

Quantum computing improves substantially on known classical algorithms for various important problems, but the nature of the relationship between quantum and classical computing is not yet fully understood. This relationship can be clarified by free models, that add to classical computing just enough physical principles to represent quantum computing and no more. Here we develop an axiomatisation of quantum computing that replaces the standard continuous postulates with a small number of discrete equations, as well as a free model that replaces the standard linear-algebraic model with a category-theoretical one. The axioms and model are based on reversible classical computing, isolate quantum advantage in the ability to take certain well-behaved square roots, and link to various quantum computing hardware platforms. This approach allows combinatorial optimisation, including brute force computer search, to optimise quantum computations. The free model may be interpreted as a programming language for quantum computers, that has the same expressivity and computational universality as the standard model, but additionally allows automated verification and reasoning.

quant-pharXiv:2602.16927•Proceedings of the National Academy of Sciences•Feb 20, 2026•0 citations

The Qudit ZH-Calculus: Generalised Toffoli+Hadamard and Universality

Patrick Roy, John van de Wetering, Lia Yeh

We introduce the qudit ZH-calculus and show how to generalise the phase-free qubit rules to qudits.We prove that for prime dimensions d, the phase-free qudit ZH-calculus is universal for matrices over the ring Z[e 2πi/d ].For qubits, there is a strong connection between phase-free ZH-diagrams and Toffoli+Hadamard circuits, a computationally universal fragment of quantum circuits.We generalise this connection to qudits, by finding that the two-qudit |0 -controlled X gate can be used to construct all classical reversible qudit logic circuits in any odd qudit dimension, which for qubits requires the three-qubit Toffoli gate.We prove that our construction is asymptotically optimal up to a logarithmic term.Twenty years after the celebrated result by Shi proving universality of Toffoli+Hadamard for qubits, we prove that circuits of |0 -controlled X and Hadamard gates are approximately universal for qudit quantum computing for any odd prime d, and moreover that phase-free ZH-diagrams correspond precisely to such circuits allowing postselections.

arXiv:2307.10095•Electronic Proceedings in Theoretical Computer Science•Aug 23, 2023•8 citations
Quantum computing offers advantages over classical computation, yet the precise features that set the two apart remain unclear. In the standard quantum circuit model, adding a 1-qubit basis-changing gate—commonly chosen to be the Hadamard gate—to a universal set of classical reversible gates yields computationally universal quantum computation. However, the computational behaviours enabled by this addition are not fully characterised. We give such a characterisation by introducing a small quantum programming language extending the universal classical reversible programming language Π with a single primitive corresponding to the Hadamard gate. The language comes equipped with a sound and complete categorical semantics that is specified by a purely equational theory. Completeness is shown by means of a novel finite presentation, and a corresponding synthesis algorithm, for the groups of orthogonal matrices with entries in the ring z [ 1 2 ] .
Rig groupoids provide a semantic model of Π , a universal classical reversible programming language over finite types. We prove that extending rig groupoids with just two maps and three equations about them results in a model of quantum computing that is computationally universal and equationally sound and complete for a variety of gate sets. 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 nondegeneracy axiom, which we relate to the Euler decomposition of the Hadamard gate. The semantic construction is turned into an extension of Π , called Π , that is a computationally universal quantum programming language equipped with an equational theory that is sound and complete with respect to the Clifford gate set, the standard gate set of Clifford+T restricted to ≤ 2 qubits, and the computationally universal Gaussian Clifford+T gate set.
Free categorical constructions characterise quantum computing as the combination of two copies of a reversible classical model, glued by the complementarity equations of classical structures. This recipe effectively constructs a computationally universal quantum programming language from two copies of Pi, the internal language of rig groupoids. The construction consists of Hughes' arrows. Thus answer positively the question whether a computational effect exists that turns reversible classical computation into quantum computation: the quantum effect. Measurements can be added by layering a further effect on top. Our construction also enables some reasoning about quantum programs (with or without measurement) through a combination of classical reasoning and reasoning about complementarity.
We construct a computationally universal quantum programming language Quantum Π from two copies of Π , the internal language of rig groupoids. The first step constructs a pure (measurement-free) term language by interpreting each copy of Π in a generalisation of the category Unitary in which every morphism is “rotated” by a particular angle, and the two copies are amalgamated using a free categorical construction expressed as a computational effect. The amalgamated language only exhibits quantum behaviour for specific values of the rotation angles, a property which is enforced by imposing a small number of equations on the resulting category. The second step in the construction introduces measurements by layering an additional computational effect.
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.
Quantum computing improves substantially on known classical algorithms for various important problems, but the nature of the relationship between quantum and classical computing is not yet fully understood. This relationship can be clarified by free models, that add to classical computing just enough physical principles to represent quantum computing and no more. Here we develop an axiomatisation of quantum computing that replaces the standard continuous postulates with a small number of discrete equations, as well as a free model that replaces the standard linear-algebraic model with a category-theoretical one. The axioms and model are based on reversible classical computing, isolate quantum advantage in the ability to take certain well-behaved square roots, and link to various quantum computing hardware platforms. This approach allows combinatorial optimisation, including brute force computer search, to optimise quantum computations. The free model may be interpreted as a programming language for quantum computers, that has the same expressivity and computational universality as the standard model, but additionally allows automated verification and reasoning.
We introduce the qudit ZH-calculus and show how to generalise the phase-free qubit rules to qudits.We prove that for prime dimensions d, the phase-free qudit ZH-calculus is universal for matrices over the ring Z[e 2πi/d ].For qubits, there is a strong connection between phase-free ZH-diagrams and Toffoli+Hadamard circuits, a computationally universal fragment of quantum circuits.We generalise this connection to qudits, by finding that the two-qudit |0 -controlled X gate can be used to construct all classical reversible qudit logic circuits in any odd qudit dimension, which for qubits requires the three-qubit Toffoli gate.We prove that our construction is asymptotically optimal up to a logarithmic term.Twenty years after the celebrated result by Shi proving universality of Toffoli+Hadamard for qubits, we prove that circuits of |0 -controlled X and Hadamard gates are approximately universal for qudit quantum computing for any odd prime d, and moreover that phase-free ZH-diagrams correspond precisely to such circuits allowing postselections.