The Logic of Reversible Computing: Theory and Practice

TY - BOOK

T1 - The Logic of Reversible Computing

T2 - Theory and Practice

AU - Kaarsgaard, Robin

PY - 2017

Y1 - 2017

N2 - Reversible computing is the study of models of computation that exhibit both forward andbackward determinism. While reversible computing initially gained interest through itspotential to reduce the energy consumption of computing machinery, via a result fromphysics now known as Landauer’s principle, a number of other applications in computerscience have since been proposed, from syntax descriptions to model-based testing, debugging,and even robotics.In spite of its numerous current (and potential future) applications, the establishedfoundations for computation and programming, such as Turing machines, -calculi, andvarious categorical models, are largely ill equipped to handle reversible computing, as theseoften tacitly rely on irreversible operations to function. To set reversible computing ona foundation as solid as the one for conventional computing requires both a significantadaptation of existing techniques and the development of new ones.In this thesis, we investigate reversible computing from a perspective of logic, broadlyconstrued. To complement the operational point of view from which reversible computingis often studied, we offer a denotational account of reversibility in computation based onrecent work in category theory. We propose two new techniques, founded in formal logic,for reasoning about reversible logic circuits. Further, we account for the behaviour of fixedpoints in certain proposed categorical models of reversible computing, and connect theseresults to the behaviour of recursive functions and data types in established reversible programminglanguages. In an application and extension of some of these results, we proposea uniform categorical foundation for a large class of reversible imperative programminglanguages known as structured reversible flowchart languages. We investigate the role of reversibleeffects in reversible functional programming, and show that a wide palette of thesemay be modelled as arrows (in the sense of Hughes) satisfying certain additional equations.Finally, we propose a brief vision for the future of the reversible functional programminglanguage Rfun.

AB - Reversible computing is the study of models of computation that exhibit both forward andbackward determinism. While reversible computing initially gained interest through itspotential to reduce the energy consumption of computing machinery, via a result fromphysics now known as Landauer’s principle, a number of other applications in computerscience have since been proposed, from syntax descriptions to model-based testing, debugging,and even robotics.In spite of its numerous current (and potential future) applications, the establishedfoundations for computation and programming, such as Turing machines, -calculi, andvarious categorical models, are largely ill equipped to handle reversible computing, as theseoften tacitly rely on irreversible operations to function. To set reversible computing ona foundation as solid as the one for conventional computing requires both a significantadaptation of existing techniques and the development of new ones.In this thesis, we investigate reversible computing from a perspective of logic, broadlyconstrued. To complement the operational point of view from which reversible computingis often studied, we offer a denotational account of reversibility in computation based onrecent work in category theory. We propose two new techniques, founded in formal logic,for reasoning about reversible logic circuits. Further, we account for the behaviour of fixedpoints in certain proposed categorical models of reversible computing, and connect theseresults to the behaviour of recursive functions and data types in established reversible programminglanguages. In an application and extension of some of these results, we proposea uniform categorical foundation for a large class of reversible imperative programminglanguages known as structured reversible flowchart languages. We investigate the role of reversibleeffects in reversible functional programming, and show that a wide palette of thesemay be modelled as arrows (in the sense of Hughes) satisfying certain additional equations.Finally, we propose a brief vision for the future of the reversible functional programminglanguage Rfun.

UR - https://rex.kb.dk/primo-explore/fulldisplay?docid=KGL01011006986&context=L&vid=NUI&search_scope=KGL&tab=default_tab&lang=da_DK

M3 - Ph.D. thesis

BT - The Logic of Reversible Computing

PB - Department of Computer Science, Faculty of Science, University of Copenhagen

ER -