Paper: One Rig to Control Them All (at LICS 2026)
Open access: https://doi.org/10.4230/LIPIcs.LICS.2026.56
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.
BibTeX
@InProceedings{HeunenKaarsgaardLem-OneRigtoControlThem,
author = {Chris Heunen and Robin Kaarsgaard and Louis Lemonnier},
title = {One Rig to Control Them All},
booktitle = {Proceedings of the Forty-First Annual Symposium on Logic in Computer Science (LICS 2026)},
year = {2026},
month = {July},
pages = {56:1--56:24},
location = {Lisbon, Portugal},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
doi = {10.4230/LIPIcs.LICS.2026.56}
}