Expressive reversible language: Aspects of semantics and implementation

Hdl Handle:
http://hdl.handle.net/10149/132190
Title:
Expressive reversible language: Aspects of semantics and implementation
Authors:
Lynas, A. R. (Angel Robert)
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
URI:
http://hdl.handle.net/10149/132190
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
Language:
en
Keywords:
reversible computation; formal specification; translation

Full metadata record

DC FieldValue Language
dc.contributor.advisorStoddart, W. J. (Bill)en
dc.contributor.advisorDunne, S. E. (Steve)en
dc.contributor.authorLynas, A. R. (Angel Robert)en
dc.date.accessioned2011-05-26T14:24:52Z-
dc.date.available2011-05-26T14:24:52Z-
dc.date.issued2011-02-
dc.identifier.urihttp://hdl.handle.net/10149/132190-
dc.description.abstractIn 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.en
dc.language.isoenen
dc.publisherTeesside Universityen
dc.subjectreversible computationen
dc.subjectformal specificationen
dc.subjecttranslationen
dc.titleExpressive reversible language: Aspects of semantics and implementationen
dc.typeThesis or dissertationen
dc.publisher.departmentTeesside Universityen
dc.type.qualificationnamePhDen
dc.type.qualificationlevelDoctoralen
or.citation.harvardLynas, A. R. (2011) Expressive reversible language: Aspects of semantics and implementation. Unpublished PhD Thesis. Teesside University.en
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.