From reversible programming languages to reversible metalanguages
Research output: Contribution to journal › Journal article › Research › peer-review
During the past decade reversible programming languages have been formalized using various established semantics frameworks. However, these semantics fail to effectively specify the distinct properties of reversible languages at the metalevel, even including the central question of whether the defined language is reversible. In this paper, we build a metalanguage foundation for reversible languages from categorical principles, based on the category of sets and partial injective functions. We exemplify our approach by a step-by-step development of the full semantics of an r-Turing complete reversible while-language with recursive procedures. The use of the metalanguage leads to a formalization of the reversible semantics. A language defined in the metalanguage is guaranteed to have reversibility and inverse semantics. Also, program inverters for this language are obtained for free. We further discuss applications and directions for reversible semantics.
Original language | English |
---|---|
Journal | Theoretical Computer Science |
Volume | 920 |
Pages (from-to) | 46-63 |
Number of pages | 18 |
ISSN | 0304-3975 |
DOIs | |
Publication status | Published - 2022 |
Bibliographical note
Publisher Copyright:
© 2022 Elsevier B.V.
- Formal semantics, Iteration, Partial injective functions, Recursion, Reversible programming
Research areas
ID: 307745540