Let ψ be a partial recursive function (of one argument) with λ-defining term F∈Λ°. This means There are several proposals for what F⌜n⌝ should be in case ψ(n) is undefined: (1) a term without a normal form (Church); (2) an unsolvable term (Barendregt); (3) an easy term (Visser); (4) a term of order 0 (Statman).

These four possibilities will be covered by one ‘master’ result of Statman which is based on the ‘Anti Diagonal Normalization Theorem’ of Visser (1980). That ingenious theorem about precomplete numerations of Ershov is a powerful tool with applications in recursion theory, metamathematics of arithmetic and lambda calculus.

At the recent TC2 working conference on constructing programs from specifications (Moeller, 1991), I presented the derivation of a functional program for solving a problem posed by Knuth (1990). Slightly simplified, the problem was to construct a shortest decimal fraction representing a given integer multiple of 1/216. Later in the conference – and in a different context – Robert Dewar described a second problem that he had recently set as an examination question. In brief, the problem was to replace sequences of blanks in a file by tab characters wherever possible. Although Knuth's and Dewar's problems appear to have little in common, I suspected that both had the same ‘deep structure’ and were instances of a single general result about greedy algorithms. The purpose of this note is to bring the genral result to light and to unify the treatment of the two problems. We begin by describing the problems more precisely.

In my previous Functional Pearls article (Bird, 1992), I proved a theorem giving conditions under which an optimization problem could be implemented by a greedy algorithm. A greedy algorithm is one that picks a ‘best’ element at each stage. Here, we return to this theorem and extend it in various ways. We then use the theory to solve an intriguing problem about unravelling sequences into a smallest number of ascending subsequences.