Law and Order in Algorithmics
Fokkinga, Martinus Maria (1992) Law and Order in Algorithmics. thesis.

PDF
850kB 
Abstract:  An algorithm is the inputoutput 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 inputoutput 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 34 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 coalgebras 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 lawsingeneral, 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. 
Item Type:  Thesis 
Additional information:  Imported from EWI/DB PMS [dbutwente:phdt:0000003413] 
Faculty:  Electrical Engineering, Mathematics and Computer Science (EEMCS) 
Research Group:  
Link to this item:  http://purl.utwente.nl/publications/66251 
Export this item as:  BibTeX EndNote HTML Citation Reference Manager 
Repository Staff Only: item control page
Metis ID: 118387