A Library of Reversible Circuit Transformations (Work in Progress)

Isomorphisms between finite types directly correspond to combinational, reversible, logical gates. Categorically they are morphisms in special classes of (bi-)monoidal categories. The coherence conditions for these categories determine sound and complete equivalences between isomorphisms. These equivalences were previously shown to correspond to a second-level of isomorphisms between the gate-modeling isomorphisms. In this work-in-progress report, we explore the use of that second level of isomorphisms to express semantic-preserving transformations and optimizations between reversible logical circuits. The transformations we explore are, by design, sound and complete therefore providing the basis for a complete library. Furthermore, we propose in future work, that attaching cost annotations to each level-2 transformation allows the development of strategies to transform circuits to optimal ones according to user-defined cost functions.