From reversible programming languages to reversible metalanguages
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Standard
From reversible programming languages to reversible metalanguages. / Glück, Robert; Kaarsgaard, Robin; Yokoyama, Tetsuo.
I: Theoretical Computer Science, Bind 920, 2022, s. 46-63.Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - From reversible programming languages to reversible metalanguages
AU - Glück, Robert
AU - Kaarsgaard, Robin
AU - Yokoyama, Tetsuo
N1 - Publisher Copyright: © 2022 Elsevier B.V.
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
KW - Formal semantics
KW - Iteration
KW - Partial injective functions
KW - Recursion
KW - Reversible programming
U2 - 10.1016/j.tcs.2022.02.024
DO - 10.1016/j.tcs.2022.02.024
M3 - Journal article
AN - SCOPUS:85125445401
VL - 920
SP - 46
EP - 63
JO - Theoretical Computer Science
JF - Theoretical Computer Science
SN - 0304-3975
ER -
ID: 307745540