Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem
Adriano Barile, Stefano Berardi, Luca Roversi
TL;DR
This work models a class of Reversible Boolean Circuits (RBC) as a bi-dimensional diagrammatic language within a free $3$-category ${\bf Toff}$, enabling simultaneous representation of circuits and their rewriting rules. Termination of the rewriting system is proved by constructing a strict $3$-functor ${\bf Toff}\to{\bf Move}$ to a well-founded $3$-category that records wire moves and imposes a decreasing measure. The approach builds on higher-category formalisms to capture multi-level compositions and reductions, leveraging a Move-based cost to guarantee that no infinite rewrite sequences exist. The results lay groundwork for normal-form analysis of RBC and invite extensions to other reversible gate bases and confluence studies, highlighting both practical implications for circuit optimization and theoretical insights into higher-dimensional rewriting systems.
Abstract
Reversible Boolean Circuits are an interesting computational model under many aspects and in different fields, ranging from Reversible Computing to Quantum Computing. Our contribution is to describe a specific class of Reversible Boolean Circuits - which is as expressive as classical circuits - as a bi-dimensional diagrammatic programming language. We uniformly represent the Reversible Boolean Circuits we focus on as a free 3-category Toff. This formalism allows us to incorporate the representation of circuits and of rewriting rules on them, and to prove termination of rewriting. Termination follows from defining a non-identities-preserving functor from our free 3-category Toff into a suitable 3-category Move that traces the "moves" applied to wires inside circuits.