## Algebraic Data Types and Program Transformation

#### Grant Malcolm

PhD Thesis, Rijksuniversiteit Groningen, 1990.

• The thesis is written in English, with the exception of this summary. Click here for the original Dutch version.

Computer programs manipulate data that is structured in some way; the structure of the data often determines to some extent the structure of the program. This principle has been exploited in functional programming languages that allow users to define their own data structures. Such programming languages usually allow some form of pattern matching, which facilitates the definition of recursive functions following the structure of the given data. The role of data structures in programming is the starting point for the research reported in this thesis.

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.

Grant Malcolm