Law and Order in Algorithmics

An algorithm is the input-output effect of a computer program; mathematically, the notion of algorithm comes close to the notion of function. Just as arithmetic is the theory and practice of calculating with numbers, so is ALGORITHMICS the theory and practice of calculating with algorithms. Just as a law in arithmetic is an equation between numbers, like a(b+c) = ab + ac, so is a LAW in algorithmics an equation between algorithms. The goal of the research done is: (extending algorithmics by) the systematic detection and use of laws for algorithms. To this end category theory (a branch of mathematics) is used to formalise the notion of algorithm, and to formally prove theorems and laws about algorithms. The underlying motivation for the research is the conviction that algorithmics may be of help in the construction of computer programs, just as arithmetic is of help in solving numeric problems. In particular, algorithmics provides the means to derive computer programs by calculation, from a given specification of the input-output effect. In Chapter 2 the systematic detection and use of laws is applied to category theory itself. The result is a way to conduct and present proofs in category theory, that is an alternative to the conventional way (diagram chasing). In Chapter 3--4 several laws are formally derived in a systematic fashion. These laws facilitate to calculate with those algorithms that are defined by induction on their input, or on their output. Technically, initial algebras and terminal co-algebras play an crucial role here. In Chapter 5 a category theoretic formalisation of the notion of law itself is derived and investigated. This result provides a tool to formulate and prove theorems about laws-in-general, and, more specifically, about equationally specified datatypes. Finally, in Chapter 6 laws are derived for arbitrary recursive algorithms. Here the notion of ORDER plays a crucial role. The results are relevant for current functional programming languages.