What do reversible programs compute?

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

T2 - 14th International Conference on Foundations of Software Science and Computational Structures

Y2 - 26 March 2011 through 3 April 2011

ER -