S-C. Mu and R. S. Bird. In First Asian Workshop on Programming Languages and Systems, Singapore, December 2000.
[GZipped Postscript]
The algebraic style of reasoning about programs has been proposed and studied by computing scientists. We rephrase the old problem of building trees of minimum height as an optimisation problem and apply the greedy theorem to derive a linear time algorithm. To put the problem in the right form, we find it necessary to generalise from functions to relations and make use of the converse of a function theorem to write the inverse of a function as a fold.