Theory and applications of inverting functions as folds.
Written on June 20, 2007
S-C. Mu and R. S. Bird. In Science of Computer Programming Vol. 51 Special Issue for Mathematics of Program Construction 2002, pp. 87-116, 2003.
[GZipped Postscript]
This paper is devoted to the proof, applications, and generalisation of a theorem, due to Bird and de Moor, that
gave conditions under which a total function can be expressed as a relational fold. The theorem is illustrated with three problems, all dealing with constructing trees with various properties. It is then generalised to give conditions under which the inverse of a partial function can be expressed as a relational hylomorphism. Its proof makes use of Doornbos and Backhouse’s theory on well-foundedness and reductivity. Possible applications of the generalised theorem is discussed.
Filed in: Journal.
Tags: Converse-of-a-Function Theorem, Program Derivation, Program Inversion.