A Calculation Approach to Program Inversion

Abstract

Many problems in computation can be specified in terms of computing the inverse of an easily constructed function. However, studies on how to derive an algorithm from a problem specification involving inverse functions are relatively rare. The aim of this thesis is to demonstrate, in an example-driven style, a number of techniques to do the job. The techniques are based on the framework of relational, algebraic program derivation. Simple program inversion can be performed by just taking the converse of the program, sometimes known as to "run a program backwards". The approach, however, does not match the pattern of some more advanced algorithms. Previous results, due to Bird and de Moor, gave conditions under which the inverse of a total function can be written as a fold. In this thesis, a generalised theorem stating the conditions for the inverse of a partial function to be a hylomorphism is presented and proved. The theorem is applied to many examples, including the classical problem of rebuilding a binary tree from its preorder and inorder traversals. This thesis also investigates into the interplay between the above theorem and previous results on optimisation problems. A greedy linear-time algorithm is derived for one of its instances — to build a tree of minimum height. The necessary monotonicity condition, though looking intuitive, is difficult to establish. For general optimal bracketing problems, however, the thinning strategy gives an exponential-time algorithm. The reason and possible improvements are discussed in a comparison with the traditional dynamic programming approach. The greedy theorem is also generalised to a generic form allowing mutually defined algebras. The generalised theorem is applied to the optimal marking problem defined on non-polynomial based datatypes. This approach delivers polynomial-time algorithms without the need to convert the inputs to polynomial based datatypes, which is sometimes not convenient to do. The many techniques are applied to solve the Countdown problem, a problem derived from the popular television program of the same name. Different derivation strategies are compared. Finally, it is shown how to derive from its specification the inverse of the Burrows-Wheeler transform, a string-to-string transform useful in compression. As a bonus, we also outline how two generalisations of the transform may be derived.