Descargas: Algebra of Programming

Preface

Our purpose in this book is to show how to calculate programs. We describe an algebraic approach to programming, suitable both for the derivation of individual programs and for the study of programming principles in general. The programming principles we have in mind are those paradigms and strategies of program construction that form the core of the subject known as Algorithm Design. Examples of such principles include: dynamic programming, greedy algorithms, exhaustive search, and divide and conquer.
The main ideas of the algebraic approach are illustrated by an extensive study of optimisation problems, conducted in Chapters 7-10. These are problems that involve finding a largest, smallest, cheapest, and so on, member of a set of possible solutions satisfying some given constraints. It is surprising how many computational problems can be specified in terms of optimising some suitable measure, even problems that do not at first sight fall into the traditional areas of combinatorial optimisation. However, the book is not primarily about optimisation problems, rather it is about one approach to solving programming problems in general.
Our mathematical framework is a categorical calculus of relations. The calculus is categorical because we want to formulate algorithmic strategies without reference to specific datatypes, and relational because we need a degree of freedom in specification and proof that a calculus of functions alone would not provide. With the help of this calculus, the standard principles of algorithm design can be formulated as theorems about classes of problems whose specifications possess a particular structure. The problems are abstract in the sense that they are parameterised by one or more datatypes. These theorems say that, under appropriate conditions, a certain strategy works and leads to a particular form of abstract solution.
Specific algorithms for specific problems are obtained by checking that the conditions hold and instantiating the results. The solution may take the form of a function, but more usually a relation, characterised as the solution to a certain recursive equation. The recursive equation is then refined to a recursive program that delivers a function, and the result is translated into a functional programming language. All the programs derived in Chapters 7-10 follow this pattern, and the popular language Gofer (Jones 1994) is used to implement the results.
A categorical calculus provides not only a means for formulating algorithmic strate*gies abstractly, but also a smooth and integrated framework for conducting proofs.
The style employed throughout the book is one of equational and inequational point-free reasoning with functions and relations. A point-free calculation is one in which the expressions under manipulation denote functions or relations, built functional and relational composition as the basic combining form. In contrast, pointwise reasoning is reasoning conducted at the level of functional or relational application and expressed in a formalism such as the predicate calculus.
The point-free style is intrinsic to a categorical approach, but is less common in proofs about programs. One of the advantages of a point-free style is that one is unencumbered by many of the complications involved in manipulating formula dealing with bound variables introduced by explicit quantifications. Point-free reasoning is therefore well suited to mechanisation, though none of the many calculations recorded in this book were in fact produced with the help of a mechanical proof assistant.

1. Programs
   
   1. Datatypes
   2. Natural numbers
   3. Lists
   4. Trees
   5. Inverses
   6. Polymorphic functions
   7. Pointwise and point-free
   
   
2. Functions and Categories
   
   1. Categories
   2. Functors
   3. Natural transformations
   4. Constructing datatypes
   5. Products and coproducts
   6. Initial algebras
   7. Type functors
   
   
3. Applications
   
   1. Banana-split
   2. Ruby triangles and Horner's rule
   3. The TEX problem - part one
   4. Conditions and conditionals
   5. Concatenation and currying
   
   
4. Relations and Allegories
   
   1. Allegories
   2. Special properties of arrows
   3. Tabular
   4. Locally complete allegories
   5. Boolean allegories
   6. Power allegories
   
   
5. Datatypes in Allegories
   
   1. Relators
   2. Relational products
   3. Relational coproducts
   4. The power relator
   5. Relational catamorphisms
   6. Combinatorial functions
   7. Lax natural transformations
   
   
6. Recursive Programs
   
   1. Digits of a number
   2. Least fixed points
   3. Hylomorphisms
   4. Fast exponentiation and modulus
   5. Unique fixed points
   6. Sorting by selection
   7. Closure
   
   
7. Optimisation Problems
   
   1. Minimum and maximum
   2. Monotonic algebras
   3. Planning a company party
   4. Shortest paths on a cylinder
   5. The security van problem
   
   
8. Thinning Algorithms
   
   1. Thinning
   2. Paths in a layered network
   3. Implementing thin
   4. The knapsack problem
   5. The paragraph problem
   6. Bitonic tours
   
   
9. Dynamic Programming
   
   1. Theory
   2. The string edit problem
   3. Optimal bracketing
   4. Data compression
   
   
10. Greedy Algorithms
    
    1. Theory
    2. The detab-entab problem
    3. The minimum tardiness problem
    4. The TEX problem - part two