Expressive reversible language: Aspects of semantics and implementation

Abstract

In this thesis we investigate some of the issues involved in creating a reversible variant of the formal software development language B. We consider the effects of regarding computation as a potentially reversible process, yielding a number of new programming structures which we integrate into an implementation-level language RB0, a more expressive variant of B0, the current implementation-level language for B. Since reversibility simplifies garbage collection, in RB0 we make use of more abstract, set-based data types, normally available in B only at the specification level. Similarly, we propose extending the domain of abstract functions currently specifiable in B to allow them to become concrete functions, thereby furnishing B with a functional sub-language. We also investigate expanding the use of Lambda calculus from the abstract stage of B to the implementation. Unlike B0, RB0 will not disallow non-determinism, and can also specify what we call Prospective Value computations (which are described). The executable language implements all of these features. After introducing some preliminary concepts, we review the work leading to the rise of Reversible Computing as a possible answer to the growing problem of energy dissipation in modern processors. We describe the language RB0, and demonstrate the use of its features, introducing the companion language RB1 and its role in the process. We then introduce our execution platform, the Reversible Virtual Machine (RVM), and translate some of the examples developed earlier into RVM code. For the concrete functions, we provide a proposed syntax and translation schema to enable consistent translation to RVM, and introduce a postfix Lambda notation to link the RB0 specification to the RVM’s own postfix notation. We provide comprehensive translation schemas for those parts of RB0 which would be found in B operations; these will form the basis of an automated translation engine. In addition, we look at a denotational semantics for Bunch theory, which has proved useful in formalising the underlying concepts.