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.

翻译：可逆布尔电路是一种在可逆计算与量子计算等不同领域中具有多方面研究价值的计算模型。本文的贡献在于将一类表达能力与经典电路相当的可逆布尔电路描述为二维图解式编程语言。我们统一将所研究的可逆布尔电路表示为自由3-范畴Toff。该形式化框架使我们能够将电路表示及其重写规则纳入其中，并证明重写操作具有终止性。这一终止性结论是通过构建一个从自由3-范畴Toff到适当3-范畴Move的非恒等保序函子实现的，该函子可追踪电路中作用于导线的"移动"操作。