A design-based model of reversible computation 

Hdl Handle:
http://hdl.handle.net/10149/58312
Title:
A design-based model of reversible computation 
Book Title:
Unifying theories of programming
Authors:
Stoddart, W. J. (Bill); Zeyda, F. (Frank); Lynas, R. (Robert)
Affiliation:
University of Teesside
Citation:
Stoddart, W. J., Zeyda, F. and Lynas, A. R.(2006) ‘A design-based model of reversible computation’, First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006, in Unifying theories of programming, Lecture notes in computer science. Heidelberg: Springer, pp.63-83.
Publisher:
Springer Verlag
Conference:
First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006
Issue Date:
Jun-2006
URI:
http://hdl.handle.net/10149/58312
DOI:
10.1007/11768173_4
Abstract:
We investigate, within the UTP framework of Hoare He Designs, the effect of seeing computation as an essentially reversible process. We describe the theoretical link between reversibility and the minimum power requirements of a computation, and we review Zuliani’s work on Reversible Probabilistic Guarded Command Language. We propose an alternative formalisation of reversible computing which accommodates backtracking. To obtain a basic backtracking language able to search for a single result we exploit the already recognised properties of non-deterministic choice, using it as provisional choice rather than implementor’s choice. We add a “prospective values” formalism which can describe programs that return all the possible results of a search, and we show how to formally describe the premature termination of such a search, a mechanism analogous to the “cut” of Prolog. An appendix describes some aspects of the wp calculus in terms of Designs, as needed for our proofs. Support for the programming structures described has been incorporated in a reversible virtual machine for i386 platforms with Posix compatibility.
Type:
Meetings and Proceedings; Book Chapter
Keywords:
reversible computing; backtracking; Hoare He Designs; wp calculus; prospective values; programming theories
Series/Report no.:
Lecture notes in computer science; 4010/2006
ISBN:
978-3-540-34750-7
Citation Count:
0 [Scopus, 4/12/2009]

Full metadata record

DC FieldValue Language
dc.contributor.authorStoddart, W. J. (Bill)-
dc.contributor.authorZeyda, F. (Frank)-
dc.contributor.authorLynas, R. (Robert)-
dc.date.accessioned2009-04-01T10:48:44Z-
dc.date.available2009-04-01T10:48:44Z-
dc.date.issued2006-06-
dc.identifier.isbn978-3-540-34750-7-
dc.identifier.doi10.1007/11768173_4-
dc.identifier.urihttp://hdl.handle.net/10149/58312-
dc.description.abstractWe investigate, within the UTP framework of Hoare He Designs, the effect of seeing computation as an essentially reversible process. We describe the theoretical link between reversibility and the minimum power requirements of a computation, and we review Zuliani’s work on Reversible Probabilistic Guarded Command Language. We propose an alternative formalisation of reversible computing which accommodates backtracking. To obtain a basic backtracking language able to search for a single result we exploit the already recognised properties of non-deterministic choice, using it as provisional choice rather than implementor’s choice. We add a “prospective values” formalism which can describe programs that return all the possible results of a search, and we show how to formally describe the premature termination of such a search, a mechanism analogous to the “cut” of Prolog. An appendix describes some aspects of the wp calculus in terms of Designs, as needed for our proofs. Support for the programming structures described has been incorporated in a reversible virtual machine for i386 platforms with Posix compatibility.-
dc.publisherSpringer Verlag-
dc.relation.ispartofseriesLecture notes in computer science-
dc.relation.ispartofseries4010/2006-
dc.subjectreversible computing-
dc.subjectbacktracking-
dc.subjectHoare He Designs-
dc.subjectwp calculus-
dc.subjectprospective values-
dc.subjectprogramming theories-
dc.titleA design-based model of reversible computation -
dc.typeMeetings and Proceedings-
dc.typeBook Chapter-
dc.contributor.departmentUniversity of Teesside-
dc.title.bookUnifying theories of programming-
dc.identifier.conferenceFirst International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006-
ref.assessmentRAE 2008-
ref.citationcount0 [Scopus, 4/12/2009]-
or.citation.harvardStoddart, W. J., Zeyda, F. and Lynas, A. R.(2006) ‘A design-based model of reversible computation’, First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5-7, 2006, in Unifying theories of programming, Lecture notes in computer science. Heidelberg: Springer, pp.63-83.-
prism.startingPage63-
prism.endingPage83-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.