Tag Archives: Program Derivation

Maximum Segment Sum and Density with Bounded Lengths

It may be surprising that variations of the maximum segment sum (MSS) problem, a textbook example for the squiggolists, are still active topics for algorithm designers. These literate Haskell scripts presents a program solving two recently studied variations:

  1. mssu.lhs: an amortised linear-time algorithm computing the maximum sum of segments not longer than an upper-bound;
  2. msdlb.lhs: an O(n log L) algorithm computing the maximum density (average) of segments not shorter than a lower-bound;
  3. msdll.lhs: computing the maximum density (average) of segments not shorter than a lower-bound. With the discovery of Glodwasser et al. we are able to refine the algorithm to amortised linear time again.

2007/06/26 Update: fixed binary search.
2007/11/04 Update: linear time algorithm for MSDL.

Countdown: a case study in origami programming

R. S. Bird and S-C. Mu. In Journal of Functional Programming Vol. 15(5), pp. 679-702, 2005.
[GZipped Postscript]

Countdown is the name of a game in which one is given a list of source numbers and a target number, with the aim of building an arithmetic expression out of the source numbers to get as close to the target
as possible. Starting with a relational specification we derive a number of functional programs for solving Countdown. These programs are obtained by exploiting the properties of the folds and unfolds of various data types, a style of programming Gibbons has aptly called origami programming. Countdown is attractive as a case study in origami programming both as an illustration of how different algorithms can emerge from a single specification, as well as the space and time trade-offs that have to be taken into account in comparing functional programs.

Inverting the Burrows-Wheeler transform

R. S. Bird and S-C. Mu. In Journal of Functional Programming Vol. 14(6) Special Issue on Functional Pearls, pp. 603-612, Novermber 2004.
[PDF][GZipped Postscript]

The Burrows-Wheeler Transform is a string-to-string transform which, when used as a preprocessing phase in compression, significantly enhances the compression rate. However, it often puzzles people how the inverse transform can be carried out. In this pearl we to exploit simple equational reasoning to derive the inverse of the Burrows-Wheeler transform from its specification. We also outline how to derive the inverse of two more general versions of the transform, one proposed by Schindler and the other by Chapin and Tate.

Theory and applications of inverting functions as folds.

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.
[PDF][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.

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.

A Calculational Approach to Program Inversion

S-C. Mu, A Calculational Approach to Program Inversion. D.Phil Thesis. Oxford University Computing Laboratory. March 2003
[GZipped Postscript][PDF]

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 strategies toward deriving an efficient algorithm are experimented and 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. Not only do we identify the key property why the inverse algorithm works, but, as a bonus, we also outline how two generalisations of the transform may be derived.

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.

Algebraic methods for optimisation problems

R. S. Bird, J. Gibbons and S-C. Mu. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, LNCS 2297, pp. 281-307, January 2002.
[PDF]

We argue for the benefits of relations over functions for modelling programs, and even more so for modelling specifications. To support this argument, we present an extended case study for a class of optimization problems, deriving efficient functional programs from concise relational specifications.

On building trees with minimum height, relationally

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.