Tag Archives: Program Derivation

Zipping Half of a List with Its Reversal

I found this note with one page of Haskell code, without comments, when I was cleaning up my files. It took me quite a while to figure out what it might probably be about: given a list, zip its first half with the reverse of its second half, in only “one and a half” traversals of the list. It gives us a fast algorithm to, for example, check whether a list is a palindrome. I thought it was probably something we discussed in AoP, but it turns out that I must have taken the note when people in IPL were studying There and Back Again of Danvy and Goldberg. Recorded in the note was my attempt to understand it.

Let convolute (xs,ys) = zip xs (reverse ys) and half be a function cutting a list in half, the problem is simply specified by revzip = convolute . half. The first trick is that convolute can be expressed in terms of its generalisation:

> convolute :: ([a],[b]) -> [(a,b)]
> convolute = fstn . uncurry walk
>   where fstn (xs,[]) = xs

where walk is defined by:

  walk xs ys = (zip xs (reverse (take n ys)), drop n ys)
      where n = length xs

The reason introducing walk is that it can be defined as a fold:

> walk = foldr ((.).shift) (split (nil, id))
> shift x (zs,y:ys) = ((x,y):zs, ys)
> nil _ = []

But the definition below is probably a lot more comprehensible:

  walk [] ys = ([],ys)
  walk (x:xs) ys = shift x (walk xs ys)

Some of these auxiliary functions should be part of the Haskell Prelude:

> prod (f,g) (a,b) = (f a, g b)
> split (f,g) a = (f a, g a)

The following implementation of half splits a list into two halfs using two pointers:

> half :: [a] -> ([a],[a])
> half = race . dup 
> race (xs,[]) = ([],xs)
> race (_:xs,[_]) = ([],xs)
> race (x:xs,_:_:ys) = cross ((x:),id) (race (xs,ys))
> dup a = (a,a)

Furthermore, uncurry f = apply . prod (f,id) where

> apply (f,a) = f a

Therefore the specification has become:

  revzip = fstn . apply . prod (walk,id) . race . dup

Now we try to fuse prod (walk,id) . race and get

> wrace (xs,[]) = (split (nil, id), xs)
> wrace (_:xs, [_]) = (split (nil, id), xs)
> wrace (x:xs, _:_:ys) = prod ((shift x .), id) (wrace (xs,ys))

Hence the result:

> revzip = fstn . apply . wrace . dup

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.