Computational Category Theory

Authors : D.E. Rydeheard, University of Manchester and R.M. Burstall, University of Edinburgh
Publication Date : July 2001

Terms and Conditions:


Book Excerpts:

This book is an account of a project in which basic constructions of category theory are expressed as computer programs. The programs are written in a functional programming language, called ML, and have been executed on examples. The authors have used these programs to develop algorithms for the unification of terms and to implement a categorical semantics.

In general, this book is a bridge-building exercise between category theory and computer programming. These efforts are a first attempt at connecting the abstract mathematics with concrete programs, whereas others have applied categorical ideas to the theory of computation.

The original motivation for embarking on the exercise of programming categorical constructions was a desire to get a better grip on categorical ideas, making use of a programmer's intuition. The abstractness of category theory makes it difficult for many computer scientists to master it; writing code seemed a good way to bring it down to earth. Someone with a computing background who wishes to learn category theory should have recourse to standard texts, some of which are listed later, but could well find this book a helpful companion text. Mathematicians who have learned a little programming, perhaps in conventional languages like Pascal, may profit from seeing how the functional programming style can embody abstract mathematics and do it in a way not too far from mathematical notation.

Intended Audience:

This book should be helpful to computer scientists wishing to understand the computational significance of theorems in category theory and the constructions carried out in their proofs. Specialists in programming languages should be interested in the use of a functional programming language in this novel domain of application, particularly in the way in which the structure of programs is inherited from that of the mathematics. It should also be of interest to mathematicians familiar with category theory - they may not be aware of the computational significance of the constructions arising in categorical proofs.

View/Download Computational Category Theory | PDF | Postscript