An Injective Language for Reversible Computation

Abstract. Erasure of information incurs an increase in entropy and dissipates 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.

• Type: Conference
• Year: 2004
• Where: MPC
• Authors: Shin-Cheng Mu, Zhenjiang Hu, Masato Takeichi
• Keywords: Bennett’s Reversible Turing, Mathematics, MPC 2004, Point-free Functional Language, Reversible Transformations