From reversible programming languages to reversible metalanguages

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningfagfællebedømt

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.

OriginalsprogEngelsk
TidsskriftTheoretical Computer Science
Vol/bind920
Sider (fra-til)46-63
Antal sider18
ISSN0304-3975
DOI
StatusUdgivet - 2022

Bibliografisk note

Funding Information:
The authors would like to thank Markus Holzer and Martin Kutrib for editing this special issue, and the anonymous reviewers for their useful feedback. The second author is supported by the Independent Research Fund Denmark under DFF-International Postdoc Fellowship No. 0131-00025B . The third author is supported by JSPS KAKENHI Grant Number 18K11250 and Nanzan University Pache Research Subsidy I-A-2 for the 2021 academic year.

Funding Information:
The authors would like to thank Markus Holzer and Martin Kutrib for editing this special issue, and the anonymous reviewers for their useful feedback. The second author is supported by the Independent Research Fund Denmark under DFF-International Postdoc Fellowship No. 0131-00025B. The third author is supported by JSPS KAKENHI Grant Number 18K11250 and Nanzan University Pache Research Subsidy I-A-2 for the 2021 academic year.

Publisher Copyright:
© 2022 Elsevier B.V.

ID: 307745540