S-C. Mu, Z. Hu and M. Takeichi. In Mathematics of Program Construction 2004, LNCS 3125, pp. 289-313, July 2004.
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.
S-C. Mu and R. S. Bird. In The First Asian Symposium on Programming Languages and Systems, LNCS 2895, pp. 265-282, Bejing, 2003.
Given the inorder and preorder traversal of a binary tree whose labels are all distinct, one can reconstruct
the tree. This article examines two existing algorithms for rebuilding the tree in a functional framework, using existing theory on function inversion. We also present a new, although complicated, algorithm by trying another possibility not explored before.
S-C. Mu and R. S. Bird. In Sixth International Conference on Mathematics of Program Construction, Dagstuhl, Germany, July 2002
This paper is devoted to the proof and applications of a theorem giving conditions under which the inverse of a partial function can be expressed as a relational hylomorphism. The theorem is a generalisation of a previous result, due to Bird and de Moor, that gave conditions under which a total function can be expressed a relational fold. The theorem is illustrated with three problems, all dealing with constructing trees with various properties.