Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Carette, J., Sabry, A.: Computing with semirings and weak rig groupoids. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 123–148. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49498-1_6
Cockett, R., Comfort, C., Srinivasan, P.: The category CNOT. In: Coecke, B., Kissinger, A. (eds.) Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, Nijmegen, The Netherlands, 3–7 July 2017, volume 266 of EPTCS, pp. 258–293 (2017)
Fiore, M.P., Di Cosmo, R., Balat, V.: Remarks on isomorphisms in typed calculi with empty and sum types. Ann. Pure Appl. Logic 141(1–2), 35–50 (2006)
Fiore, M.: Isomorphisms of generic recursive polynomial types. In: POPL, pp. 77–88. ACM (2004)
Fredkin, E., Toffoli, T.: Conservative logic. Int. J. Theor. Phys. 21(3), 219–253 (1982)
Goldberg, E., Novikov, Y.: How good can a resolution based SAT-solver be? In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 37–52. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_4
James, R.P., Sabry, A.: Information effects. In: POPL, pp. 73–84. ACM (2012)
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. Trans. Comp. Aided Des. Integ. Cir. Sys 21(12), 1377–1394 (2006)
Laplaza, M.L.: Coherence for distributivity. In: Kelly, G.M., Laplaza, M., Lewis, G., Mac Lane, S. (eds.) Coherence in Categories. LNM, vol. 281, pp. 29–65. Springer, Heidelberg (1972). https://doi.org/10.1007/BFb0059555
Michael Miller, D., Maslov, D., Dueck, G.W.: A transformation based algorithm for reversible logic synthesis. In: Proceedings of the 40th Annual Design Automation Conference, DAC 2003, pp. 318–323 (2003). ACM, New York
Shende, V.V., Prasad, A.K., Markov, I.L., Hayes, J.P.: Synthesis of reversible logic circuits. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 22(6), 710–722 (2003)
Sparks, Z., Sabry, A.: Superstructural reversible logic. In: 3rd International Workshop on Linearity (2014)
Toffoli, T.: Reversible computing. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 632–644. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10003-2_104
Xu, S.: Reversible Logic Synthesis with Minimal Usage of Ancilla Bits. Ph.D thesis, MIT (2015)
Yamashita, S., Markov, I.L.: Fast equivalence-checking for quantum circuits. In: Proceedings of the 2010 IEEE/ACM International Symposium on Nanoscale Architectures, NANOARCH 2010, pp. 23–28. IEEE Press, Piscataway (2010)
Acknowledgments
We thank the anonymous reviewers for their valuable comments and Kyle Carter for insights on the cost semantics.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Hutslar, C., Carette, J., Sabry, A. (2018). A Library of Reversible Circuit Transformations (Work in Progress). In: Kari, J., Ulidowski, I. (eds) Reversible Computation. RC 2018. Lecture Notes in Computer Science(), vol 11106. Springer, Cham. https://doi.org/10.1007/978-3-319-99498-7_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-99498-7_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99497-0
Online ISBN: 978-3-319-99498-7
eBook Packages: Computer ScienceComputer Science (R0)