Abstract
During the past decade, reversible programming languages have been formalized using various established semantic frameworks. However, these semantics fail to effectively specify the distinct properties of reversible languages at the metalevel, and even neglect the central question of whether the defined language is reversible. In this paper, we build on a metalanguage foundation for reversible languages based on the category of sets and partial injective functions. We exemplify our approach through step-by-step development of the full semantics of an r-Turing complete reversible while-language with recursive procedures. This yields a formalization of the semantics in which the reversibility of the language and its inverse semantics are immediate, as well as the inversion of programs written in the language. We further discuss applications and future research directions for reversible semantics.
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
Notes
- 1.
An online interpreter for R-WHILE with procedures and the example program considered in this paper are available at http://tetsuo.jp/ref/RPLA2019.
References
Axelsen, H.B., Glück, R., Yokoyama, T.: Reversible machine code and its abstract processor architecture. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol. 4649, pp. 56–69. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74510-5_9
Cockett, R., Lack, S.: Restriction categories III: colimits, partial limits and extensivity. Math. Struct. Comput. Sci. 17(4), 775–817 (2007)
Frank, M.P.: Reversibility for efficient computing. Ph.D. thesis, MIT (1999)
Giles, B.: An investigation of some theoretical aspects of reversible computing. Ph.D. thesis, University of Calgary (2014)
Glück, R., Kaarsgaard, R.: A categorical foundation for structured reversible flowchart languages: Soundness and adequacy. Log. Methods Comput. Sci. 14(3) (2018)
Glück, R., Kawabe, M.: Revisiting an automatic program inverter for Lisp. SIGPLAN Not. 40(5), 8–17 (2005)
Glück, R., Yokoyama, T.: A minimalist’s reversible while language. IEICE Trans. Inf. Syst. E100-D 100(5), 1026–1034 (2017)
Glück, R., Yokoyama, T.: Constructing a binary tree from its traversals by reversible recursion and iteration. IPL 147, 32–37 (2019)
Haghverdi, E.: A categorical approach to linear logic, geometry of proofs and full completeness. Ph.D. thesis, Carlton Univ. and Univ. Ottawa (2000)
Hoey, J., Ulidowski, I., Yuen, S.: Reversing parallel programs with blocks and procedures. In: Pérez, J.A., Tini, S. (eds.) Expressiveness in Concurrency, Structural Operational Semantics. Electronic Proceedings in TCS, vol. 276, pp. 69–86 (2018)
Holzer, M., Kutrib, M.: Reversible nondeterministic finite automata. In: Phillips, I., Rahaman, H. (eds.) RC 2017. LNCS, vol. 10301, pp. 35–51. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-59936-6_3
James, R.P., Sabry, A.: Information effects. In: POPL, pp. 73–84. ACM (2012)
Kaarsgaard, R., Axelsen, H.B., Glück, R.: Join inverse categories and reversible recursion. J. Log. Algebr. Methods 87, 33–50 (2017)
Kari, J.: Reversible cellular automata: from fundamental classical results to recent developments. New Gener. Comput. 36(3), 145–172 (2018)
Kuhn, S., Ulidowski, I.: A calculus for local reversibility. In: Devitt, S., Lanese, I. (eds.) RC 2016. LNCS, vol. 9720, pp. 20–35. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40578-0_2
Morita, K.: Reversible computing and cellular automata – a survey. Theor. Comput. Sci. 395(1), 101–131 (2008)
Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke, B. (ed.) New Structures for Physics. LNP, vol. 813, pp. 289–355. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-12821-9_4
Wille, R., Schönborn, E., Soeken, M., Drechsler, R.: SyReC: a hardware description language for the specification and synthesis of reversible circuits. Integration 53, 39–53 (2016)
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)
Yokoyama, T., Axelsen, H.B., Glück, R.: Towards a reversible functional language. In: De Vos, A., Wille, R. (eds.) RC 2011. LNCS, vol. 7165, pp. 14–29. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29517-1_2
Yokoyama, T., Axelsen, H.B., Glück, R.: Fundamentals of reversible flowchart languages. Theor. Comput. Sci. 611, 87–115 (2016)
Yokoyama, T., Glück, R.: A reversible programming language and its invertible self-interpreter. In: PEPM, pp. 144–153. ACM (2007)
Acknowledgments
Support in the form of EU COST Action IC1405 is acknowledged. The third author is supported by JSPS KAKENHI Grant Number 18K11250.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Glück, R., Kaarsgaard, R., Yokoyama, T. (2020). Reversible Programs Have Reversible Semantics. In: Sekerinski, E., et al. Formal Methods. FM 2019 International Workshops. FM 2019. Lecture Notes in Computer Science(), vol 12233. Springer, Cham. https://doi.org/10.1007/978-3-030-54997-8_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-54997-8_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-54996-1
Online ISBN: 978-3-030-54997-8
eBook Packages: Computer ScienceComputer Science (R0)