Computation is sure to become one of the most important of the sciences. This is because it is the science of how machines can be made to carry out intellectual processes. We know that any intellectual process that can be carried out mechanically can be performed by a general purpose digital computer. Moreover, the limitations on what we have been able to make computers do so far clearly come far more from our weakness as programmers than from the intrinsic limitations of the machines. We hope that these limitations can be greatly reduced by developing a mathematical science of computation.
There are three established directions of mathematical research relevant to a science of computation. The first and oldest of these is numerical analysis. Unfortunately, its subject matter is too narrow to be of much help in forming a general theory, and it has only recently begun to be affected by the existence of automatic computation.
The second relevant direction of research is the theory of computability as a branch of recursive function theory. The results of the basic work in this theory, including the existence of universal machines and the existence of unsolvable problems, have established a framework in which any theory of computation must fit. Unfortunately, the general trend of research in this field has been to establish more and better unsolvability theorems, and there has been very little attention paid to positive results and none to establishing the properties of the kinds of algorithms that are actually used. Perhaps for this reason the formalisms for describing algorithms are too cumbersome to be used to describe actual algorithms.
The third direction of mathematical research is the theory of finite automata. Results which use the finiteness of the number of states tend not to be very useful in dealing with present computers which have so many states that it is impossible for them to go through a substantial fraction of them in a reasonable time.
The present paper is an attempt to create a basis for a mathematical theory of computation. Before mentioning what is in the paper, we shall discuss briefly what practical results can be hoped for from a suitable mathematical theory. This paper contains direct contributions towards only a few of the goals to be mentioned, but we list additional goals in order to encourage a gold rush.
1. To develop a universal programming language. We believe that this goal has been written off prematurely by a number of people. Our opinion of the present situation is that ALGOL is on the right track but mainly lacks the ability to describe different kinds of data, that COBOL is a step up a blind alley on account of its orientation towards English which is not well suited to the formal description of procedures, and that UNCOL is an exercise in group wishful thinking. The formalism for describing computations in this paper is not presented as a candidate for a universal programming language because it lacks a number of features, mainly syntactic, which are necessary for convenient use.
2. To define a theory of the equivalence of computation processes. With such a theory we can define equivalence preserving transformations. Such transformations can be used to take an algorithm from a form in which it is easily seen to give the right answers to an equivalent form guaranteed to give the same answers but which has other advantages such as speed, economy of storage, or the incorporation of auxiliary processes.
3. To represent algorithms by symbolic expressions in such a way that significant changes in the behavior represented by the algorithms are represented by simple changes in the symbolic expressions. Programs that are supposed to learn from experience change their behavior by changing the contents of the registers that represent the modifiable aspects of their behavior. From a certain point of view, having a convenient representation of one's behavior available for modification is what is meant by consciousness.
4. To represent computers as well as computations in a formalism that permits a treatment of the relation between a computation and the computer that carries out the computation.
5. To give a quantitative theory of computation. There might be a quantitative measure of the size of a computation analogous to Shannon's measure of information. The present paper contains no information about this.
The present paper is divided into two sections. The first contains several descriptive formalisms with a few examples of their use, and the second contains what little theory we have that enables us to prove the equivalence of computations expressed in these formalisms. The formalisms treated are the following:
1. A way of describing the functions that are computable in terms of given base functions, using conditional expressions and recursive function definitions. This formalism differs from those of recursive function theory in that it is not based on the integers, strings of symbols, or any other fixed domain.
2. Computable functionals, i.e. functions with functions as arguments.
3. Non-computable functions. By adjoining quantifiers to the computable function formalism, we obtain a wider class of functions which are not a priori computable. However, such functions can often be shown to be equivalent to computable functions. In fact, the mathematics of computation may have, as one of its major aspects, rules which permit us to transform functions from a non-computable form into a computable form.
4. Ambiguous functions. Functions whose values are incompletely specified may be useful in proving facts about functions where certain details are irrelevant to the statement being proved.
5. A way of defining new data spaces in terms of given base spaces and of defining functions on the new spaces in terms of functions on the base spaces. Lack of such a formalism is one of the main weaknesses of ALGOL but the business data processing languages such as FLOWMATIC and COBOL have made a start in this direction, even though this start is hampered by concessions to what the authors presume are the prejudices of business men.
The second part of the paper contains a few mathematical results about the properties of the formalisms introduced in the first part. Specifically, we describe the following:
1. The formal properties of conditional expressions.
2. A method called recursion induction for proving the equivalence of recursively defined functions.
3. Some relations between the formalisms introduced in this paper and other formalisms current in recursive function theory and in programming.
We hope that the reader will not be angry about the contrast between the great expectations of a mathematical theory of computation and the meager results presented in this paper.