Category Archives: Conference

An injective language for reversible computation

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.

Rebuilding a tree from its traversals: a case study of program inversion

S-C. Mu and R. S. Bird. In The First Asian Symposium on Programming Languages and Systems, LNCS 2895, pp. 265-282, Bejing, 2003.
[GZipped Postscript]

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.

Inverting functions as folds

S-C. Mu and R. S. Bird. In Sixth International Conference on Mathematics of Program Construction, Dagstuhl, Germany, July 2002
[GZipped Postscript]

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.