What do reversible programs compute?
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
What do reversible programs compute? / Axelsen, Holger Bock; Glück, Robert.
Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings. ed. / Martin Hofmann. Springer, 2011. p. 42-56 (Lecture notes in computer science, Vol. 6604).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - What do reversible programs compute?
AU - Axelsen, Holger Bock
AU - Glück, Robert
N1 - Conference code: 14
PY - 2011
Y1 - 2011
N2 - Reversible computing is the study of computation models that exhibit both forward and backward determinism. Understanding the fundamental properties of such models is not only relevant for reversible programming, but has also been found important in other fields, e.g., bidirectional model transformation, program transformations such as inversion, and general static prediction of program properties.Historically, work on reversible computing has focussed on reversible simulations of irreversible computations. Here, we take the viewpoint that the property of reversibility itself should be the starting point of a computational theory of reversible computing. We provide a novel semantics-based approach to such a theory, using reversible Turing machines (RTMs) as the underlying computation model.We show that the RTMs can compute exactly all injective, computable functions. We find that the RTMs are not strictly classically universal, but that they support another notion of universality; we call this RTM-universality. Thus, even though the RTMs are sub-universal in the classical sense, they are powerful enough as to include a self-interpreter. Lifting this to other computation models, we propose r-Turing completeness as the ‘gold standard’ for computability in reversible computation models.
AB - Reversible computing is the study of computation models that exhibit both forward and backward determinism. Understanding the fundamental properties of such models is not only relevant for reversible programming, but has also been found important in other fields, e.g., bidirectional model transformation, program transformations such as inversion, and general static prediction of program properties.Historically, work on reversible computing has focussed on reversible simulations of irreversible computations. Here, we take the viewpoint that the property of reversibility itself should be the starting point of a computational theory of reversible computing. We provide a novel semantics-based approach to such a theory, using reversible Turing machines (RTMs) as the underlying computation model.We show that the RTMs can compute exactly all injective, computable functions. We find that the RTMs are not strictly classically universal, but that they support another notion of universality; we call this RTM-universality. Thus, even though the RTMs are sub-universal in the classical sense, they are powerful enough as to include a self-interpreter. Lifting this to other computation models, we propose r-Turing completeness as the ‘gold standard’ for computability in reversible computation models.
U2 - 10.1007/978-3-642-19805-2_4
DO - 10.1007/978-3-642-19805-2_4
M3 - Article in proceedings
SN - 978-3-642-19804-5
T3 - Lecture notes in computer science
SP - 42
EP - 56
BT - Foundations of Software Science and Computational Structures
A2 - Hofmann, Martin
PB - Springer
Y2 - 26 March 2011 through 3 April 2011
ER -
ID: 44240484