S-C. Mu, Z. Hu and M. Takeichi. In Mathematics of Program Construction 2004, LNCS 3125, pp. 289-313, July 2004.
[PDF]
Erasure of information incurs an increase in entropy and dissipatse heat. Therefore, information-preserving computation is essential for constructing computers that use energy more effectively. A more recent motivation to understand reversible transformations also comes from the design of editors where editing actions on a view need to be reflected back to the source data.
In this paper we present a point-free functional language, with a relational semantics, in which the programmer is allowed to define injective functions only. Non-injective functions can be transformed into a program returning a history. The language is presented with many examples, and its relationship with Bennett’s reversible Turing machine is explained.
The language serves as a good model for program construction and reasoning for reversible computers, and hopefully for modelling bi-directional updating in an editor.