Formal Characterisations of 'Algorithm'

The notion of computable function has been widely studied in theoretical computer science, and it is often assumed that any questions we have about algorithms can be answer by using one of the traditional models of computation (Turing machines, recursive functions, etc.). This assumption fails to square with the way algorithm is used in computer science practice. When discussing algorithms, we are not merely interested in input/output behaviour, since we mark a distinction between different algorithms for the same task. On the other hand, an algorithm is not a program or Turing machine, since multiple programs, in different programming languages, can implement the same algorithm. An adequate formal characterisation of algorithm has yet to be proposed.

This project focusses on analysing the notion of algorithm, with a view to formalising statements like “MergeSort runs in $O(n \log n)$ time”, “Program $\pi$ implements Algorithm $A$” and “Kruskal’s algorithm is correct for the Minimum Spanning Tree problem”. Major existing work in this area can be found by authors including Yuri Gurevich, Yiannia Moschovakis and Walter Dean.