|Title: ||Expressive reversible language: Aspects of semantics and implementation|
|Advisors: ||Stoddart, W. J. (Bill)|
Dunne, S. E. (Steve)
|Citation: ||Lynas, A. R. (2011) Expressive reversible language: Aspects of semantics and implementation. Unpublished PhD Thesis. Teesside University.|
|Publisher: ||Teesside University|
|Issue Date: ||Feb-2011 |
|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.|
|Type: ||Thesis or dissertation|
|Keywords: ||reversible computation|
|Appears in Collections: ||PhD Theses|
|Files in This Item:|
|132190.pdf||Final Thesis||983Kb||Adobe PDF|
|132190.pdf||Licence Agreement (Administrator Use Only)||549Kb||Adobe PDF|
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.