A theory of data structures for computing science should satisfy certain requirements. It should offer a notation for defining new data structures and provide some guidance in defining recursive functions on these structures. Above all, the notation for these functions should facilitate formal reasoning. It is often relatively strightforward to write a correct, but sadly inefficient program for some specification. Therefore it is desirable that programs can be transformed in such a way that correctness is preserved while efficiency is improved. In short, a theory of data structures should also comprise a calculus for program transformation.
This thesis discusses a notation for defining data types by means of initial algebras (as well as the related notion of final coalgebras). This notation is based on universal properties, which gives a method for writing recursive functions and provides the basis for a calculus of program transformations. The universal properties give rise to a proof technique, which we call "promotion", that leads to short and elegant program transformations. The notation and some examples are set out in the second chapter of the thesis. The third chapter treats a simple extension of the notation that allows data types with infinite elements, such as infinite lists, to be defined. The fourth chapter discusses the use of relations instead of functions in defining and transforming programs defined on subtypes; here, both the algebraic and the logical structure of the data type play an important role. The fifth chapter examines the existence of the defined data types, in particular parameterised data types.