A design-based model of reversible computation 

W. J. (Bill) Stoddart, F. (Frank) Zeyda, R. (Robert) Lynas

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    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.
    Original languageEnglish
    Title of host publicationUnifying Theories of Programming
    Subtitle of host publicationUTP 2006
    Editors Dunne, Stoddart
    Place of PublicationBerlin
    PublisherSpringer Verlag
    ISBN (Electronic)9783540347521
    ISBN (Print)9783540347507
    Publication statusPublished - 2006

    Publication series

    NameLecture Notes in Computer Science

    Cite this