One Rig to Control Them All
Chris Heunen, Robin Kaarsgaard, Louis Lemonnier
Abstract
Controlled commands -- computations whose execution depends on a separate input -- play a central role in reversible Boolean circuits and quantum circuits. However, existing formalisms typically treat control only implicitly, entangled with other aspects of computation. From a semantic perspective, control is most naturally expressed in semisimple rig categories, which -- unlike standard circuit models such as props -- support both parallel and conditional composition. We present a construction that freely adjoins an explicit syntactic notion of control to a circuit theory specified as a suitable prop, subject to eight universally quantified equations. Our main result is that these equations are sound and complete for the intended semantics of control: the resulting theory satisfies a universal property, identifying it exactly as the circuit subtheory of the free semisimple rig completion. The proof combines coherence for rig categories with a new method based on induction over Gray codes. We illustrate the usefulness of the framework by showing that it simplifies several existing sound and complete axiomatisations of quantum circuits, isolating a small and conceptually clean set of generators and equations. In addition, the same equations yield a sound and complete axiomatisation of the multiply controlled Toffoli gate set, that is universal for reversible Boolean circuits.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 43480881-b055-4468-94d3-761d6085f26aCited by top-tier papers1
Ask how each one uses itBuilds on6
- A Complete Equational Theory for Quantum CircuitsAlexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix et al.LICS 2023 · 14 citations
- With a Few Square Roots, Quantum Computing Is as Easy as PiJacques Carette, Chris Heunen, Robin Kaarsgaard, Amr SabryPOPL 2024 · 7 citations
- Minimal Equational Theories for Quantum CircuitsAlexandre Clément, Noé Delorme, Simon PerdrixLICS 2024 · 3 citations
- Quantum information effectsChris Heunen, Robin KaarsgaardPOPL 2022 · 1 citation
- Hadamard-Pi: Equational Quantum ProgrammingWang Fang, Chris Heunen, Robin KaarsgaardPOPL 2026
Related papers
- Complete ω-Regular Supermartingale CertificatesAlessandro Abate, Mirco Giacobbe, Sergey Ichtchenko, Diptarko RoyLICS 2026
- Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languagesVikraman Choudhury, Jacek Karwowski, Amr SabryPOPL 2022 · 10 citations
- Optimal Synthesis of Multi-Controlled Qudit GatesWei Zi, Qian Li, Xiaoming SunDAC 2023 · 7 citations
- Linear Dependent Type Theory for Quantum Programming Languages: Extended AbstractPeng Fu, Kohei Kishida, Peter SelingerLICS 2020 · 23 citations
- Verification of Recursively Defined Quantum CircuitsMingsheng Ying, Zhicheng ZhangPLDI 2026
