Solving Optimisation Problems with Catamorphisms

Richard S. Bird and Oege de Moor^{⋆}

Oxford University Programming Research Group 11 Keble Road, Oxford OX1 3QD

Abstract. This paper contributes to an ongoing effort to construct a calculus for deriving programs for optimisation problems. The calculus is built around the notion of initial data types and catamorphisms which are homomorphisms on initial data types. It is shown how certain optimisation problems, which are specified in terms of a relational catamorphism, can be solved by means of a functional catamorphism. The result is illustrated with a derivation of Kruskal’s algorithm for finding a minimum spanning tree in a connected graph.

1 Introduction

Efficient algorithms for solving optimisation problems can sometimes be expressed as homomorphisms on initial data types. Such homomorphisms, which correspond to the familiar fold operators in functional programming, are called catamorphisms. In this paper, we give conditions under which an optimisation problem can be solved by a catamorphism. Our results are a natural generalisation of earlier work by Jeuring [5, 6], who considered the same problem in a slightly less abstract setting. The main contribution of the paper is to show how several seemingly disparate results about subsequences, permutations, sequence partitions, subtrees, and so on, can all be captured in a single theorem.

The specification of an optimisation problem is usually split into three components, called the generator, filter, and selector, respectively. Consider, for example, the construction of a longest ascending subsequence of a sequence of numbers. This problem might be specified as

las = max(#) · up◁ · subs.

The function subs is the generator and returns the set of all subsequences of a list. The filter up◁ retains only those subsequences which are ascending. The remaining term max(#) is the selector; it is a relation such that a(max(#))x holds if a is a longest sequence in x.

We can develop an algorithm from a specification like the above in two steps. First, we express the composition of the filter and generator as a catamorphism. The conditions under which this is possible are given by a generalisation of Malcolm’s promotion theorem [8]. Second, we take the resulting catamorphism g and try to

⋆ Research supported by the Dutch Organisation for Scientific Research, grant NFI 62–518.

express the composition max(#) · g as a second catamorphism. This is also achieved by promotion but, as we shall see, the conditions are much more restrictive.

Both the generator and the result of the first step are catamorphisms returning sets of values. Using the fact that set–valued functions are isomorphic to relations, we can express many set–valued catamorphisms as relational catamorphisms. Briefly, these are catamorphisms to algebras in which the operators are arbitrary relations rather than functions. It turns out that this observation allows us to simplify the formal treatment substantially.

The structure of the rest of the paper is as follows. In Section 2, we discuss the basic framework of sets and functions, and define the notion of catamorphism formally. We also state and prove the promotion theorem. In Section 3 we exploit the isomorphism between relations and set–valued functions to extend this material to relations. In Section 4 we define the notion of a relational catamorphism. Examples of such catamorphisms are given in Section 5. The next step in the development is to study the properties of the relation max(R), and we do this in Section 6. In particular, we will need a weak form of monotonicity, called maxotonicity. With this machinery we can state and prove the main theorem of the paper. In the last section we show how the theorem applies to one particular example, namely the derivation of Kruskal’s algorithm for minimum cost spanning trees.

2 Preliminaries

Throughout, we assume that we are working in one of two categories: the category Fun of sets and total functions, and (later on) the category Rel of sets and relations. The restriction to set theory is for purely expository reasons, as we could have started with a suitable topos and its category of relations instead of Fun and Rel [9]. It is possible to phrase the axioms of such a topos in terms of elementary identities between relations [4], and most of our results can be derived from these identities by equational reasoning. However, rather than taking such an abstract course, we will explain ideas using set–theoretic concepts. In particular, only a passing acquaintance with category theory is assumed, and we shall review all definitions essential to the exposition.

Functions and functors. Total functions will be denoted by lower case letters. We write f : A → B to indicate that f has source type A and target type B. The identity function of type A → A is written id_{A}, though we usually omit the subscript. Functional composition is denoted by a dot, so (f · g) a = f (g a).

We shall also need the notion of a functor. Functors, which will be denoted by sans serif letters, are homomorphisms between categories that preserve identity arrows and composition. For example, F : Fun → Fun is a functor if FA is an object (i.e. set or ‘type’) of Fun for each object A of Fun and Ff : FA → FB for each arrow (or ‘function’) f : A → B of Fun. Moreover, Fid = id and F(f · g) = Ff · Fg. Functor composition is denoted simply by juxtaposition, so we have (FG)f = F(Gf ). Usually, we write FGf without any brackets.

One important example of a functor is the power functor P. Here, PA denotes the power set of A, and for f : A → B the function Pf : PA → PB is defined by

(Pf )x = {f a | a ∈ x}.

In words, Pf applies f to every element of a set. The verification that P is indeed a functor is straightforward.

Products. The product of two sets B and C is a set B × C together with two projection functions, π_{1} : B × C → B and π_{2} : B × C → C , and a binary operator ⟨-, -⟩ called split. Given two functions f : A → B and g : A → C , we have ⟨f , g⟩ : A → B × C . These operators satisfy

h = ⟨f , g⟩ ≡ (π_{1} · h = f ∧ π_{2} · h = g)

for all h : A → B × C . This property characterises product up to isomorphism, so we are free to choose any representative from the isomorphism class determined by the definition. In set theory, the canonical choice for B ×C is cartesian product, and the split operator is defined by

⟨f , g⟩a = (f a, g a).

The operator × on sets can also be defined on functions: f × g = ⟨f · π_{1}, g · π_{2}⟩. This turns × into a functor (strictly speaking, a bifunctor), because × preserves composition and identities:

(f × g) · (h × k) = (f · h) × (g · k) and id_{A} × id_{B} = id_{A×B} .

Coproducts. Analogous to the definition of product, we can define the notion of coproduct. The coproduct of two sets B and C is a set B + C together with two injection functions ι_{1} : B → (B + C ) and ι_{2} : C → (B + C ), and a binary operator [-, -] called join. Given two functions f : B → A and g : C → A, the function [f , g] has type B + C → A. These operators satisfy

h = [f , g] ≡ (h · ι_{1} = f ∧ h · ι_{2} = g).

This property characterises coproduct up to isomorphism. In set theory, the canonical choice for B + C is the disjoint sum, defined by

B + C = { (1, b) | b ∈ B } ∪ { (2, c) | c ∈ C } .

The join operator is defined by

[f , g](1, b) = f b and [f , g](2, c) = g c.

Just like ×, we can make + into a functor by defining

f + g = [ι_{1} · f , ι_{2} · g].

Polynomial Functors. The class of polynomial functors in Fun → Fun is defined inductively by the following clauses:

1. The identity functor and constant functors are polynomial.

2. If F and G are polynomial functors, then so are their composition FG, their sum F + G, and their product F × G, where

(F + G)(k) = F(k) + G(k)
(F × G)(k) = F(k) × G(k).

As we shall see, polynomial functors enjoy a number of useful properties. One example of a functor that is not polynomial is the power functor P.

Algebras. Let E be a category and F : E → E a functor. By definition, an F–algebra is an arrow f : FA → A of E. For example, consider the set L of finite sequences with elements of type E. Among other ways, we can construct all finite sequences with the help of two functions: the constant function ν : 1 → L, which returns the empty sequence [ ], and the binary operator ++< : L × E → L (pronounced snoc), which takes a sequence and an element, and appends the element to the sequence:

[e_{0}, e_{1}, …, e_{n−1}] ++< e_{n} = [e_{0}, e_{1}, …, e_{n−1}, e_{n}].

(The set 1 in the type of ν stands for some distinguished one–element set and plays the role of unit type.)

The join [ν, ++<] therefore has type type 1 + (L × E) → L. This join is an F–algebra, where F : Fun → Fun is given by by

FA = 1 + (A × E)
Fh = id + (h × id) .

Homomorphisms, initial algebras, and catamorphisms. Let f : FA → A and g : FB → B be F–algebras. By definition, an F–homomorphism from f to g is an arrow h : A → B such that

h · f = g · Fh .

The composition of two F–homomorphisms is again an F–homomorphism, so the F–algebras in E form the objects of a category EF in which the arrows are F– homomorphisms. For many functors F this category has an initial object, which we denote by μF. To say that μF is initial means that for any other F–algebra f , there exists a unique homomorphism, which we denote by ([f ])F, from μF to f . Arrows of the form ([h])F are called catamorphisms.

The defining property of catamorphisms is called the unique extension property and is formalised by the equivalence

g = ([f ])F ≡ g · μF = f · Fg .

From now on we shall write ([f ]) instead of ([f ])F, the functor F being understood from context.

An example of an initial F–algebra is the data type of lists discussed above. The so–called fold–left operator foldl (⊕) e common in functional programming can be defined by two recursion equations

foldl (⊕) e [ ] = e
foldl (⊕) e (x ++< a) = (foldl (⊕) e x) ⊕ a .

These equations are equivalent to the statement that foldl (⊕) e is an F–homomorphism from [ν, ++<] to [e, ⊕]. Since [ν, ++<] is the initial F–algebra μF, we can write foldl (⊕) e = ([[e, ⊕]]). For legibility we will omit the inner brackets in such expressions, writing ([e, ⊕]) instead.

Promotion. The following theorem is called the promotion theorem. In its statement we use the abbreviation f = g (mod h) for f · h = g · h.

Theorem 1. For any functor F : Fun → Fun with an initial algebra we have

f · ([g]) = ([h]) ≡ f · g = h · Ff (mod F([g])).

Proof. The proof is simple:

f · ([g]) = ([h])
≡ {unique extension property}
f · ([g]) · μF = h · F(f · ([g]))
≡ {F is a functor}
f · ([g]) · μF = h · Ff · F([g])
≡ {unique extension property}
f · g · F([g]) = h · Ff · F([g]).

□

3 Relations

So far we have been working in the category Fun of sets and total functions. Now we turn to Rel, the category of sets and relations. Our objective is to see how and when the above theory of functions can be extended to relations.

Relations will be denoted by upper case letters R, S, . . .. We write R : A → B to denote the fact that R has source A and target B. For such an R we write b(R)a to denote the fact that b stands in the relation R to a. Functions are special kinds of relations, namely total and single–valued ones, so if f is a function, then b(f )a means b = f a. We again use a dot for relational composition, so c(R · S)a holds if there is a b with c(R)b and b(S)a. We will assume familiarity with the operations of the relational calculus displayed in Figure 1.

operator pronunciation  meaning
R^{∘} R converse b(R^{∘})a = a(R)b
R ∩ S R and S  b(R ∩ S)a = b(R)a ∧ b(S)a
R ∪ S R or S  b(R ∪ S)a = b(R)a ∨ b(S)a
R ⇒ S R implies S b(R ⇒ S)a = b(R)a ⇒ b(S)a
R/S  R divided by S b(R/S)a = (∀c : a(S)c ⇒ b(R)c)
p?  test p  b(p?)a = (b = a) ∧ (p a)
R□  domain of R  b(R□)a = (b = a) ∧ (∃c : c(R)a)
□R  range of R  b(□R)a = (b = a) ∧ (∃c : b(R)c)

Fig. 1. Operators of the relational calculus.

Power Transpose. In set theory there are various representations of relations, of which the most well–known is to represent a relation R : A → B as a set of pairs (a, b) with a ∈ A and b ∈ B. However, one can also think of a relation R : A → B as a set–valued function A → PB, where PB denotes the power set of B. We will take the view that a relation is a set of pairs, so that b(R)a means (a, b) ∈ R. The operator Λ that sends a relation to the corresponding set–valued function is called power transpose and is defined by the equation

(ΛR) a = {b | b(R)a}.

In particular, (Λf )a = {f a}. The function Λ is an isomorphism and so the inverse function Λ^{−1} is well–defined. For R : A → B and f : A → PB we have

∈_{B} · ΛR = R and Λ(∈_{B} · f ) = f ,

where ∈_{B} : PB → B is the membership relation. Usually, we omit the subscript.

Existential Image. Readers familiar with category theory will recognise that power transpose defines a right adjoint of the inclusion functor Fun → Rel. This right adjoint is known as the existential image, and the adjunction is called the power adjunction. In fact, most of set theory can be derived from the existence of the power adjunction, an observation which lies at the heart of topos theory.

Less abstractly, the existential image of a relation R : A → B is a function ER : PA → PB, defined by

(ER) x = {b | (∃a ∈ x : b(R)a)}.

The existential image preserves identity and composition and, since we can take EA = PA, we have that E is a functor from Rel to Fun.

Note that Ef = Pf for all functions f ; in words, E and P coincide on functions. However, E is not the only functor of Rel that coincides with P on functions. In the next section we shall describe another and more useful one.

The power transpose Λ and the existential image E can each be defined in terms of the other. For R : A → B we have

ΛR = ER · τ_{A} and ER = Λ(R · ∈_{A}) ,

where τ_{A} : A → PA is the function which sends an element a in A to the singleton set {a}. From the first identity we obtain the law of composition

Λ(R · S) = ER · ΛS.

Singleton and Membership. The singleton function τ (again, we omit the subscript) can be defined in terms of power transpose: τ = Λid. The collection of singleton formers is ‘polymorphic’, a fact which is expressed by the identity Pf · τ = τ · f . Category theorists refer to this equation by saying that τ is a natural transformation from the identity functor to P.

The membership relation is dual to singleton in that ∈ = Λ^{−1}id. Membership is also a natural transformation; in symbols, ∈ · ER = R · ∈. This duality is no accident and stems from the fact that membership and singleton form the unit and counit of the power adjunction.

The ‘big union’ function ⋃ is defined by ⋃ = E∈. Big union is also a natural transformation, the proof being

⋃ · EER = E∈ · EER = E(∈ · ER) = E(R · ∈) = ER · E∈ = ER · ⋃.

We also have

ER = E(∈ · ΛR) = ⋃ · E(ΛR).

(For those familiar with monads, (E, τ, ⋃) is the monad defined by the power adjunction.)

Filter. Many other set–theoretic operators can be defined in terms of power transpose and existential image. One important example is the filter operator. Given a Boolean–valued function p : A → Ω, we define p◁ : PA → PA by p◁ = E(p?). The advantage of such definitions is that they are easier to manipulate than traditional set comprehensions. For instance, here is the very short proof that filter distributes through union:

p◁ · ⋃ = E(p?) · ⋃ = ⋃ · EE(p?) = ⋃ · E(p◁).

4 Relators and Cross–operators

Let us now turn to the question of whether each functor F of Fun can be extended to a functor of Rel. An important consideration is that we would like F : Rel → Rel to be monotonic, i.e.

R ⊆ S ⇒ FR ⊆ FS.

Inclusion rather than equality is the ‘natural’ way of comparing relations. Of course, for total functions inclusion means equality. Fortunately, we have

Proposition 2. For each functor F : Fun → Fun there exists at most one monotonic functor in Rel → Rel that coincides with F on functions.

If F does have such an extension, then we say that F is a relator and we use the same symbol for both functors. We can characterise relators as those functors F that satisfy the condition

f^{∘} · g = h · k^{∘} ⇒ (Ff )^{∘} · Fg = Fh · (Fk)^{∘}

It can be shown that every monotonic functor on relations maps functions to functions, so every monotonic functor is the extension of a relator.

For example, all polynomial functors are relators. The list functor L is also a relator; this functor sends a set A to the set of finite sequences with elements from A. On functions, L is defined by the equation

(Lf )[a_{1}, a_{2}, …, a_{n}] = [fa_{1}, fa_{2}, …, fa_{n}].

Thus L is the familiar map operator from functional programming and is similar to P except that it acts on lists rather than sets. The explicit definition of L : Rel → Rel is rather messy:

[b_{1}, …, b_{n}](LR)[a_{1}, …, a_{m}] = (n = m) ∧ (∀i : 1 ≤ i ≤ n : b_{i}(R)a_{i}).

The functor P : Fun → Fun also satisfies the above conditions, although it is not polynomial. The extension P : Rel → Rel is defined explicitly by

y(PR)x = (∀a ∈ x : ∃b ∈ y : b(R)a) ∧ (∀b ∈ y : ∃a ∈ x : b(R)a) .

Hence PR corresponds to the Egli–Milner ordering induced by R. Note that P : Rel → Rel is not the same as E : Rel → Rel since P returns relations and is monotonic, while E returns functions and is not monotonic.

Cross–operators. Relators can be characterised in another useful way, namely in terms of the existence of so–called cross–operators. Cross–operators are a generalisation of the polymorphic cartesian product function.

By definition, a cross–operator on F : Fun → Fun is a collection of functions F†_{A} : FPA → PFA that satisfies the following four axioms:

1. Crossing is polymorphic, i.e. F† · FPf = PFf · F†.

2. Crossing singletons gives a singleton, i.e. F† · Fτ = τ.

3. Crossing distributes over union, i.e. F† · F⋃ = ⋃ · PF† · F†.

4. Crossing is monotonic, i.e. f ⊆ g ⇒ F† · Ff ⊆ F† · Fg, where f ⊆ g means pointwise inclusion of set–valued functions f and g.

Proposition 3. For each functor F : Fun → Fun there exists at most one cross– operator F†. This cross–operator exists if and only if F is a relator, in which case we have F† = Λ(F∈).

For an example of a particular cross–operator, recall the list functor L. The cross– operator L† is the polymorphic function that sends a sequence of sets to its cartesian product:

L†[x_{1}, x_{2}, …, x_{n}] = {[a_{1}, a_{2}, …, a_{n}] | (∀i : a_{i} ∈ x_{i})}.

It is possible to develop a little calculus of cross–operators for synthesising the cross– operator of a composite functor by simple calculation. Reluctantly, we omit a discussion of this calculus for reasons of space.

Relational Catamorphisms. So far we have only considered algebras and catamorphisms in the category Fun of sets and total functions. This is sufficient for many purposes, but for a satisfactory treatment of optimisation problems, and in particular for the selector minR, we would like to move to relations. So, how can the above theory be extended to algebras and catamorphisms in Rel? The obvious setting for relational algebras is the category RelF for some relator F : Fun → Fun with an initial algebra. Fortunately, the initial algebra of F : Rel → Rel coincides with the initial algebra of F : Fun → Fun.

Proposition 4. (Eilenberg and Wright [3]) Let F : Fun → Fun be a relator with initial algebra μF. Then μF is also an initial algebra of the extension of F to Rel → Rel. Furthermore, Λ([R]) = ([ER · F†]).

We also have the following generalisation of the promotion theorem.

Theorem 5. (Backhouse et al. [1]) Let F be a relator and possess an initial algebra. Then

R · ([S]) ⊆ ([T ]) ⇐ R · S ⊆ T · FR (mod F([S])).

Moreover, the same implication holds when ⊆ is replaced by ⊇ (and so also when ⊆ is replaced by =).

We will not prove the generalisation, but we will prove the following corollary:

Corollary 6.

p◁ · Λ([R]) = Λ([S]) ⇐ p? · R = S · F(p?) (mod F([R])).

Proof. We have

p◁ · Λ([R])
= {definition of filter}
E(p?) · Λ([R])
= {power transpose of composition}
Λ(p? · ([R]))
= {promotion}
Λ([S]) .

5 Examples

Let us now give some examples of relational catamorphisms. The first three are catamorphisms on the data type of finite sequences described above.

Subsequences. Consider a finite sequence x. By leaving out some of the elements of x, but retaining the original left–to–right order, we obtain a subsequence of x. Formally, y is a subsequence of x if

y ([ν, π_{1} ∪ ++<]) x .

One can think of (π_{1} ∪ ++<) as a non–deterministic operator which, when given a pair (x, a), either returns x or appends a to x. The catamorphism ([ν, π_{1} ∪ ++<]) is then a relation that holds between a sequence x and a subsequence of x. It follows that the function subs, which returns the set of all subsequences of a sequence, is defined by

subs = Λ([ν, π_{1} ∪ ++<]) .

We can use Proposition 4 to eliminate the power transpose from the right–hand side of this equation. After simplifying, we obtain a characterisation of subs expressed in terms of functions: subs = ([τ · ν, ⊗]), where τ · ν is the constant function returning {[ ]}, and

xs ⊗ a = xs ∪ {x ++< a | x ∈ xs}.

The relational characterisation of subs seems preferable simply because it is shorter.

Let us now instantiate the corollary of the promotion theorem to the function subs. We shall need the following property of predicates. A predicate p is said to be prefix–closed with derivative q if p [ ] holds and p (x ++< a) = p x ∧ q(x, a). More shortly, p is prefix–closed with derivative q if

p? · ν = ν
p? · ++< = ++< · q? · (p? × id).

Assuming this property of p we get

p? · [ν, π_{1} ∪ ++<]
= {coproduct and composition over union}
[p? · ν, (p? · π_{1}) ∪ (p? · ++<)]
= {p is prefix–closed}
[ν, (p? · π_{1}) ∪ (++< · q? · (p? × id)]
= {since p? · π_{1} = π_{1} · (p? × id)}
[ν, (π_{1} ∪ (++< · q?))(p? × id)]
= {coproduct}
[ν, π_{1} ∪ (++< · q?)] · (id + (p? × id))
= {definition of F}
[ν, π_{1} ∪ (++< · q?)] · F(p?).

Hence if p is prefix–closed with derivative q, then

p◁ · subs = Λ([ν, π_{1} ∪ (++< · q?)]).

Eliminating Λ, we get that p◁ · subs = ([τ · ν, ⊗]), where

xs ⊗ a = xs ∪ {x ++< a | x ∈ xs ∧ q(x, a)}.

We will use this result in our final example, and in the appendix we give a more abstract version of the above argument.

Partitions. A partition of a sequence x is a division of x into non–empty contiguous subsequences. For example, the sequence of sequences

[[1, 2], [3], [4, 5, 6]]

is a partition of [1, 2, 3, 4, 5, 6]. The function parts, which returns all partitions of its argument, is the power transpose of a relational catamorphism

parts = Λ([ν, ⊕ ∪ ⊗]),

where ⊕ is a total function defined by xs ⊕ a = xs ++< [a] and ⊗ is the partial function defined on nonempty lists by

(xs ++< x) ⊕ a = xs ++< (x ++< a) .

In words, we get a partition of x ++< a by taking some partition xs of x, and either appending [a] to xs (represented by the term xs ⊕ a), or appending a to the last component of xs (represented by the term xs ⊗ a). The power–transpose can be eliminated in a similar manner as before, but we omit details.

Permutations. The function perms, which returns all permutations of a sequence, is also the power transpose of a relational catamorphism

perms = Λ([ν, (⊕ · ++^{∘} × id)]),

where ++ denotes concatenation, and (y, z) ⊕ a = y ++ [a] ++ z. Thus,

((y, z), a)(++^{∘} × id)(x, a) if x = y ++ z.

Eliminating Λ from this expression, we get perms = ([ν ; τ, ⊗]), where ⊗ is defined by the set comprehension

xs ⊗ a = {y ++ [a] ++ z | (∃x : x ∈ xs ∧ y ++ z = x)}.

Tree Pruning. Finally, we briefly describe a relational catamorphism over a different data type. Consider the type of binary labelled trees in which both the leaves and the internal labels are natural numbers. This type is defined as the initial F–algebra, where F is the polynomial functor given by

FA = N + (A × N × A)
Fk = id_{N} + (k × id_{N} × k) .

We will call the components of the initial F–algebra Tip and Node, so

μF = [Tip, Node] .

Now consider the operator prune which takes a tree and prunes away some of its subtrees in a non–deterministic fashion. Formally, we define prune as a relational catamorphism:

prune = ([Tip, Node ∪ (Tip · π_{2}^{3})]),

where π_{2}^{3} is the projection function that returns the middle component of a triple. The power transpose of prune is the function that returns all possible prunings of its arguments. This function was used by Jeuring [5] to solve various optimisation problems on trees.

6 Minimisation

Now we consider the selection of an optimal element from a set of candidate solutions to an optimisation problem.

Let R : A → A be a preorder, so R is assumed to be reflexive (i.e. id ⊆ R) and transitive (i.e. R ·R ⊆ R). The relation minR : PA → A relates a set to its minimum elements under R. Formally, we define

minR = ∈ ∩ (R/∋),

where ∋ = ∈^{∘}. To understand this succinct definition, put R = (≤). We then get that b(min(≤))x if and only if b is both an element of x and a lower bound of x, i.e. for all a if a ∈ x, then b ≤ a. Note that maxR = minR^{∘}.

From the assumption that R is reflexive we get minR · τ = id. We give the proof:

minR · τ
= {definition of minR}
(∈ ∩ (R/∋)) · τ
= {composition (with a function) distributes over ∩}
(∈ · τ) ∩ (R/∋) · τ
= {∈ · τ = id and (R/∋) · τ = R}
id ∩ R
= {R is reflexive}
id.

From the assumption that R is transitive, we get

minR · ⋃ ⊇ minR · PminR.

We have ⊇ rather than = in this assertion since not every set has a minimum element — in particular, the empty set does not have one. However, we can replace ⊇ by = provided we compose the left–hand side with P((minR)□), so excluding sets without minimum elements under R. For reasons of space, we omit proof of these assertions.

Another useful result is that minimisation operators can always be composed:

minS · Λ(minR) = minT ,

where T = R ∩ (R^{∘} ⇒ S). The proof of this identity, which we omit, has been vigorously studied by a number of researchers in the proof methods community e.g.

Monotonicity and distributivity. In order to combine our results about relational catamorphisms and minimisation, we need to know how minR interacts with F– algebras. Consider, for example, addition of natural numbers + : (N × N) → N. Addition is an algebra of the functor F given by

FA = A × A
Fk = k × k.

Addition is monotonic with respect to ≤, a fact we can express succinctly by the assertion (+) · F(≤) ⊆ (≤) · (+). This assertion translates as

c = a + b ∧ a ≤ a′ ∧ b ≤ b′ ⇒ c ≤ a′ + b′.

More generally, f : FA → A is monotonic with respect to R if

f · FR ⊆ R · f .

Monotonicity is equivalent to distributivity. For example, writing min for the function that returns the (unique) minimum element of a set of numbers, we have

min x + min y = min {a + b | a ∈ x ∧ b ∈ y},

provided the left-hand side is well-defined. The above implication can be expressed more shortly as

(+) · Fmin(≤) ⊆ min(≤) · P(+) · F†.

Generalising to an arbitrary preorder R, we have

f · FR ⊆ f · R ≡ f · FminR ⊆ minR · Pf · F†.

The next proposition is generalisation of this result. It deals with a weaker property than monotonicity, called minotonicity. A function f : FA → A is said to be minotonic (with respect to R) on the range of a set–valued function g : B → PA if

f · F(minR · □g · ∋) ⊆ R · f .

Taking F as the identity functor, this reads

c = f b ∧ b(minR)x ∧ x(□g)x ∧ a ∈ x ⇒ c(R)(f a).

Since

minR · □g · ∋

⊆ {since □g ⊆ id}

minR · ∋

= {definition of minR}

(∈ ∩ (R/∋)) · ∋

⊆ {calculus}

(∈ · ∋) ∩ (R/∋) · ∋

⊆ {since (R/S) · S ⊆ R}

R

we have that F(minR · □g · ∋) ⊆ FR, and so monotonicity implies minotonicity. The following result is called the minotonicity lemma and the proof can be found in [2].

Lemma 7. The function f : FA → A is minotonic with respect to R on the range of g : B → PA if and only if

f · FminR ⊆ minR · Pf · F† (mod Fg).

7 Main Theorem

Now we come to the main theorem. Let F be a fixed relator in what follows, so ([-]) = ([-])F. The theorem addresses the question of when it is possible to find a program for computing minR · Λ([S]) that can be expressed as a catamorphism. We take the view that a program is a total function, so the task is to determine when

([f ]) ⊆ minR · Λ([S])

for some total function f .

Theorem 8. Suppose f is minotonic with respect to a preorder R on the range of Λ([S]). Then

f ⊆ minR · ΛS ⇒ ([f ]) ⊆ minR · Λ([S]).

Proof. We calculate

([f ]) ⊆ minR · Λ([S])

⇔ {Proposition 4}

([f ]) ⊆ minR · ([ES · F†])

⇐ {promotion}

f · FminR ⊆ minR · ES · F† (mod F([ES · F†]))

⇐ {minotonicity}

minR · Pf · F† ⊆ minR · ES · F† (mod F([ES · F†]))

⇐ {logical entailment}

minR · Pf ⊆ minR · ES.

Now we have

minR · Pf

⊆ {given assumption, and monotonicity of P}

minR · P(minR · ΛS)

= {since P is a functor}

minR · PminR · P(ΛS)

⊆ {since R is transitive}

minR · ⋃ · P(ΛS)

= {since ⋃ · P(ΛS) = ES for any S}

minR · ES .

8 Application: Kruskal’s Algorithm

Let us now see how the above theorem applies to one particular example, namely the construction of a minimum cost spanning tree in a connected graph. Each edge of the graph has an associated cost, and we will write cost e for the cost of e. We will assume that the graph is given as a sequence of edges in ascending order of cost, an assumption that will allow us to develop Kruskal’s algorithm.

The problem can be specified as follows:

mcst = minC · Λ(max(#)) · acyclic◁ · subs.

Here, subs returns the set of subsequences of the given sequence of edges, acyclic◁ removes all subsequences containing a cycle, and Λ(max(#)) returns the set of acyclic sequences of edges of greatest length, i.e. the spanning trees of the graph. The function # returns the length of a sequence. It is an abuse of notation to write max(#), since # is not an ordering; strictly speaking, we should write

max(#^{∘} · (≤) · #) .

With the same understanding, C is also a function and is defined as the sum of the costs of the edges in a given sequence. Putting all this together, mcst is a relation that holds between a minimum cost spanning tree and the graph.

As specified, the spanning tree problem involves the composition of two optimal selections. We can use an earlier result about combining minimisation operators to show that

minC · Λ(max(#)) = minR,

where the preorder R is given by

y(R)x = (#y > #x) ∨ (#y = #x ∧ C y ≤ C x) .

It follows that the spanning tree problem is solved by minimising with respect to R. Note that

y(R)x ⇒ (y ++< a)(R)(x ++< a)

for all a.

The next step is to instantiate the main theorem for problems about subsequences. In the appendix, we have stated a ‘categorical’ version of the corollary, and we have spelled out the proof in detail. Here we just state the result as it is applied in practice.

Corollary 9. Assume that R is a preorder, and suppose p is prefix–closed with derivative q and satisfies

q (x, a) ⇒ (x ++< a)(R)x .

Furthermore, assume that

q(y, a) ∧ q(x, a) ⇒ (y ++< a)(R)(x ++< a)
¬q(y, a) ∧ q(x, a) ⇒ y(R)(x ++< a),

for all x and y satisfying

y(minR · p◁ · subs)z ∧ x(∈ · p◁ · subs)z

for some z. Then ([ν, ⊕]) ⊆ minR · p◁ · subs, where x ⊕ a = x ++< a if q(x, a), and x otherwise.

For the spanning tree problem, we have that the predicate acyclic is prefix–closed with derivative q, where q(x, a) holds if a does not create a cycle when added to x. The first condition on R holds because #y > #x ⇒ y(R)x . The second condition holds because y(R)x ⇒ (y ++<a)(R)(x ++<a). This leaves us with the last condition. Let x, y, and z be as stated in the corollary, so y is some minimum cost spanning tree of z and x is some acyclic subsequence of z with y(R)x. Suppose that x ++< a is acyclic, but y ++< a contains a cycle. Since y is acyclic, y ++< a contains a cycle of the form

{(v_{0}, v_{1}), (v_{1}, v_{2}), …, (v_{n−1}, v_{n})},

where a = (v_{0}, v_{n}). Because x ++< a is acyclic, there exists an edge b = (v_{i−1}, v_{i}) in y which is not connected in x. Furthermore, cost b ≤ cost a since the graph is given as a sequence of edges in ascending order of cost. As both x and y are subsequences of z, and b is in y, it follows that there exist x_{1} and x_{2} with x = x_{1} ++ x_{2} and

(x_{1} ++ [b] ++ x_{2})(∈ · p◁ · subs)z.

Finally, we have

y(R)(x_{1} ++ [b] ++ x_{2}) and (x_{1} ++ [b] ++ x_{2})(R)(x_{1} ++ x_{2} ++ [a])

so y(R)(x ++<a). The the corollary is therefore applicable, and the result is Kruskal’s algorithm.

The spanning tree problem illustrates the strength of our claim that the foregoing abstract theory gives clear guidance on the difficult proof obligations that have to be met to obtain efficient algorithms. Indeed, apart from the last condition, the rest of the development consists essentially of instantiating the theory to problems about subsequences. The last condition is less mechanical and is the crucial property in the derivation of Kruskal’s algorithm. (It is, in fact, the verification of the matroid property [7].) But this does not invalidate the claim, because the goal of our research is to provide organising principles for algorithm design, not necessarily to mechanise the whole design process.

We should emphasise that the main theorem has many more applications besides algorithms on subsequences. The papers by Jeuring [5, 6] discuss applications to subtrees, permutations and partitions. In a forthcoming paper [2], we review some of those applications, and show how the present work can be extended to include certain dynamic programming algorithms.

References

1. R.C. Backhouse, P. de Bruin, G. Malcolm, T.S. Voermans, and J. van der Woude. Relational catamorphisms. In B. Möller, editor, Proceedings of the IFIP TC2/WG2.1 Working Conference on Constructing Programs, pages 287–318. Elsevier Science Publishers B.V., 1991.

2. R.S. Bird and O. de Moor. Inductive solutions to optimisation problems. Draft, 1991.

3. S. Eilenberg and J.B. Wright. Automata in general algebras. Information and Control, 11(4):452–470, 1967.

4. P.J. Freyd and A. Ščedrov. Categories, Allegories, volume 39 of Mathematical Library. North–Holland, 1990.

5. J. Jeuring. Deriving algorithms on binary labelled trees. In P.M.G. Apers, D. Bosman, and J. van Leeuwen, editors, Proceedings SION Computing Science in the Netherlands, pages 229–249, 1989.

6. J. Jeuring. Algorithms from theorems. In M. Broy and C.B. Jones, editors, Programming Concepts and Methods, pages 247–266. North–Holland, 1990.

7. B. Korte, L. Lovasz, and R. Schrader. Greedoids, volume 4 of Algorithms and combinatorics. Springer–Verlag, 1991.

8. G. Malcolm. Data structures and program transformation. Science of Computer Programming, 14:255–279, 1990.

9. O. de Moor. Categories, relations and dynamic programming. D.Phil. thesis. Technical Monograph PRG-98, Computing Laboratory, Oxford, 1992.

10. J.C.S.P. van der Woude. Free style spec wrestling ii: Preorders. The Squiggolist, 2(2):48–53, 1991.

Appendix: Instantiation for Subsequences

Here we show how the main theorem may be instantiated for problems about subsequences. The proofs are spelled out in great detail, to support our claim that the instantiation is largely mechanical. Throughout, F stands for the functor

FA = 1 + (A × E)
Ff = id + (f × id) ,

and α abbreviates the initial algebra [ν, ++<] : FL → L, where L is the type of lists over E.

Recall that subs = ([ν, ++< ∪ π_{1}]). It is convenient to rewrite this in the form

subs = Λ([α ∪ δ]) ,

where δ = [0, π_{1}], and 0 is the empty relation. We have

[R, S] ∪ [U , V ] = [R ∪ U , S ∪ V ] ,

so the two expressions for subs are equivalent. The advantage of naming δ is that we can refer to its algebraic properties. In particular, we have that δ is a collection of partial functions

δ · δ^{∘} ⊆ id ,

which furthermore satisfies

δ · FQ = Q · δ .

The second property asserts that δ is a natural transformation. Both of these inclusions are straightforward to verify.

Our first task is to express p◁ · subs in the form p◁ · subs = Λ([S]) for some S. Recall Corollary 1 of the promotion theorem which says that

p◁ · Λ([R]) = Λ([S]) ⇐ p? · R = S · Fp? .

Also, recall that p is prefix–closed with derivative q if

p? · ν = ν
p? · ++< = ++< · q? · (p? × id) .

These two identities can also be formulated as a single equation, namely

p? · α = α · r? · Fp?

with r = [true, q]. Assuming the latter equation, we reason:

p? · (α ∪ δ)

= {composition over union}
(p? · α) ∪ (p? · δ)
= {assumption: p? · α = α · r? · Fp? }
(α · r? · Fp?) ∪ (p? · δ)
= {naturality of δ}
(α · r? · Fp?) ∪ (δ · Fp?)
= {composition over union}
((α · r?) ∪ δ) · Fp?

Hence by Corollary 1,

p◁ · subs = Λ([(α · r?) ∪ δ]) .

Note that (α · r?) ∪ δ = [ν, (++< · q?) ∪ π_{1}], giving the result cited in Section 5.

The next task is to expand the minotonicity condition

f · F(minR · □Λ([S]) · ∋) ⊆ R · f

of the main theorem, in the case S = (α · r?) ∪ δ and f = [ν, ⊕], where

x ⊕ a = \{ \begin{matrix}x ++< a & if q(x, a) \\ x & otherwise \end{matrix}

We can rewrite f using the McCarthy conditional (p → R, S) defined by

(p → R, S) = (R · p?) ∪ (S · ¬p?) ,

where ¬p? = (¬p)?. Recall that r was defined by r = [true, q], so we have

f = (r → α, δ) .

Writing T = minR · □Λ([(α · r?) ∪ δ]) · ∋, we need conditions under which

(r → α, δ) · FT ⊆ R · (r → α, δ)  (1)

holds. We can rewrite (1) using the following two properties of conditionals

R · (p → S, T ) = (p → R · S, R · T )
R ⊆ (p → S, T ) ≡ (R · p? ⊆ S) ∧ (R · ¬p? ⊆ T ) .

Now, inclusion (1) translates to

(r → α, δ) · FT · r? ⊆ R · α
(r → α, δ) · FT · ¬r? ⊆ R · δ .

Using the definition of conditions, these inclusions expand to four more:

α · r? · FT · r? ⊆ R · α
δ · ¬r? · FT · r? ⊆ R · α
α · r? · FT · ¬r? ⊆ R · δ
δ · ¬r? · FT · ¬r? ⊆ R · δ .

We shall assume that the first two conjuncts are satisfied. Given that α · r? ⊆ R · δ, we can prove the last two:

α · r? · FT · ¬r?
⊆ {since ¬r? ⊆ id}
α · r? · FT
⊆ {assumption: α · r? ⊆ R · δ}
R · δ · FT
= {naturality of δ}
R · T · δ
⊆ {since T ⊆ R (Section 6)}
R · R · δ
⊆ {assumption: R transitive}
R · δ .

The proof of the last inclusion is:

δ · ¬r? · FT · ¬r?
⊆ {since ¬r? ⊆ id}
δ · FT
= {naturality of delta}
T · δ
⊆ {since T ⊆ R (Section 6)}
R · δ .

This completes the instantiation of minotonicity.

Finally we need to expand the hypothesis of the main theorem, namely

f ⊆ minR · ΛS

where f = (r → α, δ) and S = (α · r?) ∪ δ. Using the definition of conditionals, the hypothesis reads

α · r? ⊆ minR · Λ((α · r?) ∪ δ)
δ · ¬r? ⊆ minR · Λ((α · r?) ∪ δ) .

To establish these results, we use the following equivalence (which was not needed in the main text), whose proof we omit

U ⊆ minR · ΛV ≡ (U ⊆ V ) ∧ (U · V^{∘} ⊆ R) .

The hypothesis is therefore established if we can show

α · r? ⊆ (α · r?) ∪ δ
δ · ¬r? ⊆ (α · r?) ∪ δ
α · r? · ((α · r?) ∪ δ)^{∘} ⊆ R
δ · ¬r? · ((α · r?) ∪ δ)^{∘} ⊆ R .

The first inclusion is immediate, and the second follows from ¬r? ⊆ id. For the third we reason

α · r? · ((α · r?) ∪ δ)^{∘}
⊆ {since α · r? is a partial function}
id ∪ (α · r? · δ^{∘})
⊆ {assumption: α · r? ⊆ R · δ}
id ∪ (R · δ · δ^{∘})
⊆ {since δ is a partial function}
id ∪ R
= {assumption: R reflexive}
R .

This proves the first inequation. For the second, we reason:

δ · ¬r? · ((α · r?) ∪ δ)^{∘}

= {relation calculus}

(δ · ¬r? · r?^{∘} · α^{∘}) ∪ (δ · ¬r? · δ^{∘})

= {since ¬r? · r?^{∘} = 0}

δ · ¬r? · δ^{∘}

⊆ {since ¬r? ⊆ id}

δ · δ^{∘}

⊆ {since δ is a partial function}

id

⊆ {assumption: R reflexive}

R .

This completes the instantiation of the hypothesis in the main theorem.

Let us now summarize the conditions. We have assumed R is reflexive and transitive, and so a preorder. We have supposed p? · α = α · Fp? · r?, which is true when p is prefix-closed with derivative q, for then one can take r = [true, q]. We have also supposed that

α · r? ⊆ R · δ
α · r? · FT · r? ⊆ R · α
δ · r? · FT · ¬r? ⊆ R · α .

With r = [true, q], these are precisely the three conditions enunciated in Corollary 2 of the main theorem.

This article was processed using the LaTEX macro package with LLNCS style