Reversible Programs Have Reversible Semantics
Reversible Programs Have Reversible Semantics
复制标题
可逆程序具有可逆语义
DOI：
10.1007/978-3-030-54997-8_26
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Yokoyama Tetsuo
中科院分区：
文献类型：
--
作者：
Glueck Robert;Kaarsgaard Robin;Yokoyama Tetsuo
在过去的十年中，可逆编程语言已经正式使用各种既定的语义框架。然而，这些语义不能有效地规定可逆语言的独特性质在元层面上，甚至忽略了中心问题，即所定义的语言是否可逆。在本文中，我们建立在一个可逆语言的基础上的集合和部分内射函数的范畴。我们通过逐步发展的完整语义的r-Turing完全可逆的while-语言与递归程序的方法。这就产生了语义的形式化，其中语言的可逆性及其逆语义是直接的，以及用语言编写的程序的反转。我们进一步讨论了可逆语义的应用和未来的研究方向。
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.