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.
|Title of host publication||Unifying Theories of Programming|
|Subtitle of host publication||UTP 2006|
|Place of Publication||Berlin|
|Publication status||Published - 2006|
|Name||Lecture Notes in Computer Science|
Stoddart, W. J. B., Zeyda, F. F., & Lynas, R. R. (2006). A design-based model of reversible computation . In Dunne, & Stoddart (Eds.), Unifying Theories of Programming: UTP 2006 (Vol. 4010, pp. 63-83). (Lecture Notes in Computer Science; Vol. 4010). Springer Verlag. https://doi.org/10.1007/11768173_4