TY - GEN
T1 - One Rig to Control Them All
AU - Heunen, Chris
AU - Kaarsgaard, Robin
AU - Lemonnier, Louis
PY - 2026/7/29
Y1 - 2026/7/29
N2 - 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.
AB - 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.
KW - complete equational theories
KW - Quantum control
KW - rig categories
U2 - 10.4230/LIPIcs.LICS.2026.56
DO - 10.4230/LIPIcs.LICS.2026.56
M3 - Article in proceedings
AN - SCOPUS:105045281848
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 41st Annual Symposium on Logic in Computer Science, LICS 2026
A2 - Claudia, Faggian
A2 - Joost-Pieter, Katoen
A2 - Joost-Pieter, Katoen
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 41st Annual Symposium on Logic in Computer Science, LICS 2026
Y2 - 20 July 2026 through 23 July 2026
ER -