Notions of computability at higher types I

Summary

Abstract. This is the first of a series of three articles devoted to the conceptual problem of identifying the natural notions of computability at higher types (over the natural numbers) and establishing the relationships between these notions. In the present paper, we undertake an extended survey of the different strands of research to date on higher type computability, bringing together material from recursion theory, constructive logic and computer science, and emphasizing the historical development of the ideas. The paper thus serves as a reasonably comprehensive survey of the literature on higher type computability.

Introduction. This article is essentially a survey of fifty years of research on higher type computability. It was a great privilege to present much of this material in a series of three lectures at the Paris Logic Colloquium.

In elementary recursion theory, one begins with the question: what does it mean for an ordinary first order function on N to be “computable”? As is well known, many different approaches to defining a notion of computable function — via Turing machines, lambda calculus, recursion equations, Markov algorithms, flowcharts, etc. — lead to essentially the same answer, namely the class of (total or partial) recursive functions. Indeed, Church's thesis proposes that for functions from N to N we identify the informal notion of an “effectively computable” function with the precise mathematical notion of a recursive function.

An important point here is thatmany prima facie independentmathematical constructions lead to the same class of functions. Whilst one can argue over whether this is good evidence that the recursive functions include all effectively computable functions (see Odifreddi [1989] for a discussion), it is certainly good evidence that they represent a mathematically natural and robust class of functions. And since no other serious contenders for a class of effectively computable functions are known, most of us are happy to accept Church's thesis most of the time.

Now suppose we consider second order functions which map first order functions to natural numbers (say), and then third order functions which map second order functions to natural numbers, and so on. We will use the word functional to mean a function that takes functions of some kind as arguments.