Reversible Boolean Circuits are an interesting computational model under many aspects and in diferent ifelds, ranging from Reversible Computing to Quantum Computing. Our contribute 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 Tof . 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 Tof into a suitable 3-category Move that traces the “moves" applied to wires inside circuits.
The class of Reversible Boolean circuits (from now on, RBC) constitutes an interesting
computational model, for many reasons. We name just some of them: once implemented, they
may help to reduce electronic devices energy consumption [
N 1− T2 +
T3 + (a) Generators of RBC and their semantics T3
T3 ⇛
T3 T3
⇛ (b) An example of reduction on a Reversible
Boolean Circuit
Our focus is to study a class of RBC in the lines of [
All classical boolean functions can be expressed in RBC, provided we add extra inputs/outputs in order to make the boolean functions invertible: in a reversible setting, the number of ouputs must be always equal to that of inputs.
All gates depicted in Fig. 1a represent invertible functions; moreover, they are self-inverse, i.e., if they yield an identity when applied twice.
Our goal in the long term is to answer specific domain questions related to the reversible language purposes. Such questions in the short term require to answer more classical questions about rewriting.
An example of specific reversibility question is: “Can we partition RBC into equivalence
classes to find those containing the most eficient circuits, according to measures which depend
on ancillae or the number of generators involved?”. We recall that “ancillae” is a technical
notion, to identify variables used as temporary storage in a circuit ∈ RBC. Ancillae allow
to compute the desired function while preserving the possibility of reverting the computation.
A good reference to frame the role of ancillae in various contexts can be [
Another specific reversibility question can be: “How can we decide the equivalence of reversible circuits that we obtain by compilers which translate classical boolean circuits into reversible ones, driven by some heuristic aimed at optimizing specific parameters of the output?”. The heuristic in [8] is just an example, of the many proposed in the literature, whose purpose, for instance, is to obtain good translations minimizing the quantity of ancillae.
Answering questions like the two above requires to formally and unambiguously know the representatives of equivalence classes in RBC. This amounts to asking basic questions about rewriting, such as: “What is and how do we get normal forms of RBC?” Contributions. A natural strategy to answer the last question is to look for normal forms w.r.t. an interpretation-preserving rewriting on the circuits of RBC. Fig. 1b suggests what we mean by a simple example, in which we move a Tofoli-three gate next to another Tofoli-three so that they annihilate each other, because Tofoli-three are self-inverse operators. All base reversible gates are self-inverse, while, in general, reversible circuits do not need to be self-inverse.
Rewriting bi-dimensional diagrammatic formal languages has well-know dificulties, mainly concerning their relations with the usual (linear) syntaxes expressing the same problem.
We here explore the use of a free 3-category to represent both the reversible circuits and
the rewriting rules on them. We build over Burroni’s work [9], who introduced the notion
of polygraphs to express algebraic theories and their reductions. Lafont [
We remind the reader that an Abstract Rewriting System (ARS) is said to be terminating when there are no infinite chains of subsequent reductions, i.e. all reductions eventually yield a (not necessarily unique) normal form. We show termination of the rewriting system in Tof : termination follows from defining a functor from Tof into a suitable 3-category Move of moves applied to wires inside circuits.
We remark that the functor we introduce simplifies the functorial and diferential interpretations in [12, 10, 11]: our approach does not require to identify both a non-increasing measure on diagrams, which recalls a current flowing, and a strictly decreasing measure, connected to the “current”, which recalls heat, generated by the “current” itself. We just need to identify a decreasing measure on a monoid of strings. The measure keeps track of the “moves” being applied to each individual wire, and assigns them a cost.
Plan of our work. We sketch the definition of 3-categories (§2), then we provide a
bi-dimensional graphic representation for 3-categories representing circuits (§3). Next, we
formally define the free 3-category Tof (§4), and a functor from Tof to a 3-category Move of
movements through circuits (§5),which we show to be a decreasing measure of reductions.
Eventually we prove termination of reductions on RBC (§6). The reduction rules we utilized are
syntactic in nature; the normal form under algebraic equivalences remains an open problem [
In this section we will briefly go over the definition of -categories. We provide enough details for the purposes of representing circuits and syntactic reductions on them (level 3). For a complete description of higher categories we refer to e.g. [13, 14].
Motivations for using categories. The literature using product categories to describe
circuits is extensive; we follow Burroni and Guiraud and use higher category theory to describe
reduction systems on algebraic structures, with particular attention to circuits [
We give an anticipation on our 3-categorial model.
• The “base” level will contain a single token object * representing the empty space between wires in a circuit. • A first level will contain input and output wires, with a “monoidal” product to generate bundles of multiple wires. In our model, we will consider a single wire as a formal cell * → * between two “empty spaces” * . • A second level will contain circuits as morphisms between input wires and output wires (in our context = because of reversibility), with appropriate series and parallel compositions. • A third level will contain syntactic rewriting rules, considered as morphisms between circuits. Reductions should preserve the number of input/output wires of a circuit.
We have that each level consists of morphisms, named cells, with domain and codomain (here source and target) objects at the adjacent lower level. Source/target of a reduction is a circuit, source/target of a circuit is a set of I/O wires, and source/target of a wire is the empty space * . The -compositions will provide an unified entity that captures both concatenation of wires, series and parallel composition of circuits, as well as three diferent ways to compose reductions. Also, the properties of 0-, 1-, 2-composition will capture equations between circuits and between reductions. The levels up to the second one yield a description of circuits isomorphic to the product categories formalization.
We now provide an equational definition for -categories following [15].
Definition 1 (-categories). A (strict) -category contains the following. • A list of sets , 0 ≤ ≤ , called levels, whose elements are called -cells. • The maps s, called -source, and t, called -target, that associate to each -cell with 0 ≤ < ≤ two -cells s(), t() we respectively call the -source and the -target of ; • The -cells ⋆ , defined for all -cells , and indices 0 ≤ < ≤ such that t() = s(), called the -composition of and , with -source/target given by: 1. s( ⋆ ) = s() and t( ⋆ ) = t() when 0 ≤ ≤ ; 2. s( ⋆ ) = s() ⋆ s() and t( ⋆ ) = t() ⋆ t() when > > .
The -composition is denoted in diagrammatic order (left-to-right).
The data above define an -category if they satisfy the following further conditions. • Globularity.
s− 2(s− 1()) = s− 2(t− 1()),
t− 2(s− 1()) = t− 2(t− 1()) for all -cells with 2 ≤ ≤ . Globularity means that all -cells connect two ( − 1)-cells with the same ( − 2)-source and ( − 2)-target. • Associativity of each ⋆. • Local Units. For all -cells with 0 ≤ < ≤ , there exists an identity -cell id,,, or id for short, such that s(id,,) = t(id,,) = , the lower index source/targets of id,,are those of , and for all -cells we have – if = s( ) then id,, ⋆ = , and – if = t( ) then ⋆ id,, = .
Any -composition of -identity is a -identity, for all 0 ≤ < ≤ . • Exchange Rule.
for , , , ≤ .
( ⋆ ) ⋆ ( ⋆ ) = ( ⋆ ) ⋆ ( ⋆ ) -cells such that the above compositions are defined and all 0 ≤ < <
In order to build the measure that proves termination of circuits reductions, we need the notion of 3-functor which we define for the general case.
Definition 2 (-functor). Let , be -categories. An -functor : → is a map such that for all 0 ≤ ≤ , sends -cells of into -cells of , and such that for all -cells , of , for all 0 ≤ < ≤ , and for all -cells we have: 1. Source/Target preservation. s ( ( )) = (s ( )), t ( ( )) = (t ( )) 2. Identity preservation (for -cells and ⋆ ). (id,,) = id,, () 3. Composition preservation. ( ⋆ ) = ( ) ⋆ () Free -Categories In the next section, we will represent circuits and reductions on them with a free 3-category. A free -category consists of all well-formed expressions for objects in an -category that are generated by a set of names for cells, identities and compositions, modulo all the equations we have for -categories.
Definition 3 (Free -Categories). Let ⃗ be a signature, i.e. a list of sets ⃗ = (0, . . . , ), with sets of names for -cells for 1 ≤ ≤ , equipped with two maps s, t : → − 1, 1 ≤ ≤ such that the globularity requirement is met. We define the free -category generated by the signature ⃗ by induction on .
The 0-category 0 is just the set 0. Assume we have defined the free ( − 1)-category − 1 generated by the signature ⃗− 1 as the ( − 1)-category with levels 0, 1, . . . , − 1. • An -generator of is any name ∈ − 1 such that = 1 or ≥ 2 and satisfies the Globularity condition: s− 2(s− 1( )) = s− 2(t− 1( )) and t− 2(s− 1( )) = t− 2(t− 1( )). • Let be the set of -constants of , containing all -generators and all expressions id,, denoting the -identity on , for 0 ≤ ≤ − 1, ∈ . • Let * be the smallest set containing and all expressions ⋆ such that , ∈ *, 0 ≤ ≤ − 1 and t( ) = s(). Source/target maps are defined on * by the source/target equations for -categories.
is defined as the -category with levels 0, . . . , − 1, and = */ ∼ , where ∼ is the smallest equivalence relation compatible with ⋆0, . . . , ⋆− 1 and including Associativity, Local Units and Exchange.
Alternatively, the readers who are familiar with the definition of polygraphs [ 9, 10, 12] will notice that the free -category generated by the signature is isomorphic to the -category generated by the corresponding -polygraph, which itself lacks categorial structure at the -th level [16].
In this section we restrict to free 3-categories with a single 0-cell * and a unique generator for 1-cell, i.e. the wire , and we describe them as formal circuits and circuit reductions, by specifying what role the -compositions take in the context of circuits. We introduce a diagrammatic syntax that represents such free 3-categories and the associated circuits. A great incentive to use a bi-dimensional syntax is that diagrams actually look like circuits. We stress the fact that the categorial setting together with a diagrammatic formalism give a thorough, compact and sound presentation for circuital theories. We invite the reader to think of -compositions as a gluing operator of two objects along their common -target and source, respectively. Definition 4 (Diagrams for a free 3-category). Let us assume that is a free 3-category with generator sets ⃗ = (0, 1, 2), source and target maps s, t, a single 0-cell and a unique generator for 1-cells. The diagrammatic representation of is as follows.
• Generators. • -cells.
– 0 = {*} consists of a unique 0-cell, representing a separator between input/output wires. We depict * as a white area in the sheet of paper the diagram is drawn on. – 1 = { } consists of a unique 1-cell, which we call a wire. A wire is a formal cell between the two portions of sheet that it divides, both marked with * . – Each gate in 2 is depicted as a circuit-like box with input and output wires representing 1-source and 1-target of the circuit.
2 = ¶ , . . . , , . . . , , . . . , , . . .© .
If is a gate with input and output wires, we write : ⇒ . The diagrams depicting gates preserve the meaning of 2-cells as formal maps between 1-cells (wires). – 3-cells in 3, or reductions, are written as ⇛ . We include no diagram for 3-cells: this would involve 3-dimensional objects [10]. – The set *0 of all 0-cells is again 0 = {*} . – The set *1 of all 1-cells consists of all possible 0-compositions ⋆0 between 1-cell generators. Any element of *1 has the form * * · · · * or simply . . . , freely generated as 0-composition along their common * white area. – The set *2 of all 2-cells represents circuits, and it is obtained from gates in 2 by closure w.r.t. 0-composition ⋆0 (parallel composition, or composition along a common * area), and 1-composition ⋆1 (sequential composition, or composition along a common bundle of wires). – Compositions of 2-cells.
∗ Every two 2-cells are 0-composable, since they have as inputs and outputs 1-cells with the same source and target (the only 0-cell * ). The 0-composition of 2-cells is depicted by putting the circuits next to each other along their common * white area: . This operation corresponds to the usual parallel composition and is read left-to-right. ∗ 1-composition of 2-cells is defined for pairs of 2-cells such that 1-target of the ifrst one (its output wires) is equal to the 1-source of the second one (its input wires). 1-composition vertically stacks circuits by connecting common I/O set of wires:
. This operation corresponds to series composition and is read top-to-bottom. – Circuit equivalences.
∗ The degenerate 1-composition id ⋆1 corresponds to prolonging the wires of = s1( ). The Unit rule = = graphically shows that circuits are defined independently from the length of wires. ∗ The Exchange rule ( ⋆1 ) ⋆0 (ℎ ⋆1 ) = ( ⋆0 ℎ) ⋆1 ( ⋆0 ) says that the diagram defines a single circuit which we can be equivalently read left-to-right, or top-to-bottom. • 3-cells, or circuit reductions, can be composed with ⋆0, ⋆1, ⋆2. If : ⇛ and : ℎ ⇛ , then the compositions behave as follows.
ℎ ⇛ ℎ ⋆ 1 (, ℎ and , 1-composable) ℎ ⇛
⋆ 0 ⇛ ⋆ 2 ( = ℎ) Remark 1. The diagrammatic notation, inspired by the string diagrams of categories, can be treated as a full 2-dimensional syntax for product categories, as explained in [17]. Again in [17] there is a termination result for the rewriting system where associativity, local units and the exchange rule are understood as rewriting rules and not as equivalences, and the concepts of squeezed form and longest normal form are introduced. In this paper, we shall limit ourselves to reasoning on diagrams modulo the above equivalences.
In this section we will describe, as a free 3-category Tof , both all reversible circuits we can
obtain from the generators SWAP, NOT, CNOT (or T2, for Tofoli two), and T3 (or CCNOT), and a
particular set of reductions on such circuits. This set of gates is proven to be universal (with
ancillae) in [
Definition 5 (The free 3-category Tof of Reversible Circuits). The free 3-category of Reversible Circuits is the free 3-category specified by the following sets of 0-, 1-, 2- and 3-generators. • 0 = {*} , 1 = { }, where : * → * • 2 contains the following generators for reversible circuits, in this order: SWAP, NOT, T2, T3 2 = ¶
: 2 ⇒ 2, N : 1 ⇒ 1, T2 : 2 ⇒ 2, T3 : 3 ⇒ 3 © • 3 = ∪ ∪ ∪ , where contains the following permutation rules: = ß ⇛ , ⇛ ™ , contains the following annihilation rules: = ® N
N ⇛ , TT22 ⇛ ,
T3 T3 ⇛ contains the following sliding rules: = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩
T2 T3
N ⇛ ⇛ ⇛
N T2 T3 , , , and contains the following Swapped Tofoli rule : = ß ⇛
In this section, we will define a 3-category Move of strings of “moves”, each of them corresponding to the action of a gate on a single wire. Moves are elements of an ordered monoid that expresses the cost of series of singular moves along the wires of the circuit. The circuits are then measured by a componentwise order on all moves on all wires. The reduced circuit should describe an equivalent boolean function with a reduced total cost. The interpretation of circuits into moves will be given as a 3-functor from the free 3-category Tof of reversible circuits and a Tofoli base to Move.
Definition 6 (The ordered monoid (M, <M) of moves).
erated from the letters l, r, t.
2. We order 1, 2 ∈ M first by length, and when the lengths are the same, by the lexicographic order induced by the following order on letters: t <M r <M l.
The letters l, r, t correspond to the three moves “left-to-right", “right-to-left" on the two wires of a SWAP, and to the move “Tofoli" on any wire of a Tofoli circuit. From M we define a 3-category Move.
Definition 7 (Move). Move is a collection of the following sets and ordered sets of -cells , 0 ≤ ≤ 3.
• 0 = {*} , a single element set. • (1, <1) is the set of all cartesian powers M for ∈ N; the singleton M0 is the identical 1-cell, identified with the unique 0-cell * . We define an order on 1-cells as M <1 M if and only if < . We order vectors ⃗ ∈ M componentwise, with the product order <M on M. • (2, <2) is the set of all <1-increasing maps : M → M for some ∈ N (all the identities idM are included). Let , : M → M be 2-cells with the same source and target. We define a strictly pointwise order <2 on 2-cells by: <2 if and only if () <M () for all ∈ M. We write ≤ 2 for = ∨ <2 , that is: either (⃗) = (⃗) for all ⃗, or (⃗) <M (⃗) for all ⃗ ∈ M. • 3 contains all pairs = ⟨, ⟩ of 2-cells with the same source and target M for some , such that ≥ 2 . There is at most one 3-cell between , , which merely signals the existence of a ≤ 2-relation between the two functions. We think of each pair ⟨, ⟩ as a reduction from to . The reduction is identical if = , it is non-identical if <2 . The -compositions on the -cells are defined as follows.
• 0-composition on 1-cells is M ⋆0 M = M+. • 0-composition on 2-cells is the cartesian product of maps. • 1-composition on 2-cells is the usual (sequential) composition of maps. • 0-composition on 3-cells is defined as ⟨, ⟩ ⋆0 ⟨ ′, ′⟩ = ⟨ × ′, × ′⟩. • 1-composition on 3-cells is defined as ⟨, ⟩ ⋆1 ⟨ ′, ′⟩ = ⟨ ′, ′⟩.
• 2-composition on 3-cells is defined as ⟨, ⟩ ⋆2 ⟨, ℎ⟩ = ⟨, ℎ⟩.
Remark 2. The order <M on words is well-founded, and in fact (M, <M) is order-isomorphic to the order (N, <) on natural numbers. The order <2 on maps is well-founded. In fact, each decreasing sequence >2 ′ >2 ′′ >2 . . . defines a decreasing sequence ⃗( ) >M ′⃗( ) >M ”⃗( ) >M . . ., where⃗ = (, , . . . , ) and is the monoid unit (empty word). Therefore, every decresing sequence from has length at most the number of words which are less than ⃗( ) in M.
Proof. We first prove that ⋆0, ⋆1 are increasing on 2-cells of Move. Assume ≤ 2 ′ and ≤ 2 ′, and either <2 ′ or <2 ′. Then ⋆0 is increasing: for all ∈ M = s1 , ∈ M = s1, we have ( × )(, ) = ( (), ()) <M+ ( ′(), ′()) = ( ′ × ′)(, ). ⋆1 is increasing: if t1( ) = M = s1(), then for all ∈ s1( ) we have ( )() = ( ()) ≤ M ( ′()) ≤ M ′( ′(), and one of the two inequalities is strict, therefore ( ()) <M ′( ′(). We then have also that ⋆0 and ⋆1 are increasing on 3-cells of Move. As a consequence, -cells are closed w.r.t. -compositions. Associativity, unit and exchange axioms are straightforward.
A 3-functor : Tof → Move is strict in a 3-cell if is an identity 3-cell in Tof ⇐⇒ ( ) is an identity 3-cell in Move. is strict if is strict on all 3-cells of Tof .
Then is strict.
→ Move is a 3-functor which is strict on all generators of .
Proof. By induction on , using the fact that is a 3-functor and 0-, 1-, 2- and 3-composition are increasing.
We define a 3-functor : Tof → Move which is strict on all generators for 0-, 1- ,2-cells. Recall that a word is written left-to-right, the last letter being the last move. Definition 9 (Move interpretation). We define a map by the following assignments on the generator gates of Tof .
(* ) = * ( ) = M (
)(, ) = (l, r) ( N )() = t
( T2 )(, ) = (t, t) ( T3 )(, , ) = (t, t, t) () = ⟨ (s2), (t2)⟩ Lemma 1. The map of Def. 9 extends in a unique way to a 3-functor Tof → Move.
Lemma 2 (Termination Lemma). If the free 3-category Tof has a 3-functor to Move which is strict on all generators for 3-cells, then all chains of non-identical 3-cells in Tof terminate.
Tof is freely generated from a free 3-category, therefore is entirely and uniquely defined by the assignments on the generators of Tof , provided we recursively check that the 3-functor preserves sources and targets, and sources and targets of sources.
Theorem 1. The free 3-category of Reversible Boolean Circuits terminates (all reduction sequences are finite). s1( ) = M. By definition of the pointwise order on (s2 )(1, . . . , ) >M (t2 )(1, . . . , ) for all 1, . . . , ∈ M. of Termination for Reversible Boolean Circuits with the Tofoli base. By Lemma 2, we have to prove that is strict on all generators for 3-cells. By definition of strictness, it is enough to prove that for all
∈ 3 in Tof we have that ( ) is not an identity. By definition, ( ) is equal to the pair ⟨ (s2 ), (t2 )⟩. ( ) is not an identity if (s2 ) >2 (t2 ). Suppose
• Permutation rules.
The thesis follows from lr > rl. • Annihilation rules.
Å Ç ã ‖ T3 T3 å ‖ (, , ) Å ã ‖
(, , ) (ll, lr, rr) >M
(ll, rl, rr) (, , ) (
) (, , ) (tt, tt, tt) >M
‖ (, , )
Words on the right-hand-size are all shorter and therefore smaller. • Left-to-Right Sliding rules.
The reduction moving the Tofoli gate upwards and to the right swaps the lowest letter of the monoid t, with a higher letter, l, in all movements , , , but . Below, we consider the case of the circuit Tofoli 3.
Å
T3
(, , , ) ã ‖ Å
T3
(, , , ) ã ‖ (lt, lt, lt, rrr) >M (tl, tl, tl, rrr)
The thesis follows from lt >M tl. The Right-to-Left Sliding rules are the mirror case. • Swapped Tofoli.
This work explores 3-categories as a unified formal framework for modeling two concepts. First, it examines Reversible Boolean Circuits, which are treated as diagrams generated from a base through the iterative application of series/parallel compositions. Then, it investigates the termination of a rewriting system on these circuits. Tof is the free 3-category which efectively formalizes circuits and rewriting rules. Move is the 3-category supplying the well founded-order in a monoid of strings. Termination follows from interpreting Tof into Move by means of a (strict) functor that intuitively represent traces of moves inside the circuit being rewritten, by exploiting the common 3-category structure. A possible extension of this work is to evaluate its efectiveness in proving the termination of reductions of free 3-polygraphs generated from alternative bases which include Fredkin and Peres gates. A second development must focus on confluence: rewriting in Tof is not. We claim that the following circuits has two non-confluent normal forms:
T2 (left-sliding)
(permutation) T2
T2
We are pursuing various directions in order to obtain confluence. However, the problem at hand is known to be non-obvious. Guiraud warns that a 3-polygraph may generate an infinite number of critical pairs which, in specific cases, can be categorized into a finite set of patterns, eventually leading to confluence [12]. [8] G. Meuli, M. Soeken, M. Roetteler, N. Bjorner, G. D. Micheli, Reversible Pebbling Game for Quantum Memory Management, in: 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE), 2019, pp. 288–291. [9] A. Burroni, Higher-dimensional Word Problems with Applications to Equational Logic, Theoret. Comput. Sci. 115 (1993) 43–62. doi:https://doi.org/10.1016/ 0304-3975(93)90054-W. [10] Y. Guiraud, G. Bonfante, Polygraphic programs and polynomial-time functions, Log.
Methods Comput. Sci. 5 (2009). [11] Y. Guiraud, P. Malbos, Higher-dimensional Categories with Finite Derivation Type, Theory
Appl. Categ. 22 (2009) 420–478. [12] Y. Guiraud, Termination orders for three-dimensional rewriting, Journal of Pure and Applied Algebra 207 (2006) 341–371. doi:https://doi.org/10.1016/j.jpaa.2005. 10.011. [13] J. C. Baez, An introduction to n-categories, in: E. Moggi, G. Rosolini (Eds.), Category Theory and Computer Science, Springer Berlin Heidelberg, Berlin, Heidelberg, 1997, pp. 1–33. [14] E. Cheng, A. Lauda, Higher-dimensional categories: an illustrated guide book, https: //eugeniacheng.com/wp-content/uploads/2017/02/cheng-lauda-guidebook.pdf, 2004. [15] R. Street, The algebra of oriented simplexes, Journal of Pure and Applied Algebra 49 (1987) 304–305. [16] F. Métayer, Cofibrant objects among higher-dimensional categories, Homology, Homotopy and Applications 10 (2008) 185–188. doi:10.4310/HHA.2008.v10.n1.a7. [17] M. Acclavio, String Diagram Rewriting: Applications in Category and Proof-theory, Ph.D. thesis, Aix-Marseille Université, 2016.