The Church Turing thesis, formal models of computation, equivalence of models, and the distinction between mathematical theorem and foundational principle.
The purpose of computability theory is to make precise the idea of an effective procedure. Informally, an effective procedure is a method that can be followed step by step, without guesswork, and which produces an answer after finitely many steps whenever it is meant to halt. The central question is whether this informal idea can be captured by a formal mathematical definition.
Recursive functions give one such definition. Turing machines give another. Lambda calculus gives another. These formalisms look different, but they all define the same class of computable functions. The Church Turing thesis is the claim that this common formal class captures exactly the functions that are effectively computable.
Effective Computability
An effective computation is a procedure that can be carried out mechanically. This means that each step is determined by a fixed rule, the amount of information inspected at each step is finite, and no appeal is made to intuition, creativity, or external mathematical insight during the computation.
For example, the usual algorithm for adding two natural numbers is effective. Given two numerals, one can follow a fixed finite procedure to obtain their sum. The procedure does not depend on understanding what numbers “really are”; it depends only on manipulating symbols according to rules.
A procedure for checking whether a natural number is prime is also effective, because one may test all possible divisors up to the number itself or up to its square root. The procedure may be slow, but it is finite and mechanical.
By contrast, the instruction “choose a clever transformation” is not by itself an effective procedure, because it does not specify a fixed mechanical rule for what to do next.
Definition 10.18 (Effective Procedure)
An effective procedure is an informal method satisfying the following conditions.
It is given by a finite description.
It operates on finite symbolic inputs.
At each step, the next action is determined by a fixed rule.
Each step can be carried out mechanically.
If the procedure returns an output, it does so after finitely many steps.
This is not a formal mathematical definition, because phrases such as “mechanically” and “effective” are informal. The importance of the Church Turing thesis is that it identifies this informal notion with precise mathematical models.
Formal Models
A formal model of computation is a mathematical system designed to represent algorithms. Such a model must specify what counts as input, what counts as a step of computation, and what it means for the computation to halt with an output.
Several formal models are central in computability theory.
Recursive functions define computability through basic numerical functions and closure operations such as composition, primitive recursion, and minimization.
Turing machines define computability through an abstract machine with a finite control, a tape, a head that reads and writes symbols, and a transition function.
Lambda calculus defines computability through symbolic expressions built from variables, abstraction, and application.
Register machines define computability through simple programs acting on finitely many registers containing natural numbers.
Although these models are different in notation and motivation, they agree on which functions are computable.
Definition 10.19 (Turing Computable Function)
A partial function:
is Turing computable if there exists a Turing machine such that, for every input:
the machine halts with output whenever this value is defined, and does not halt whenever this value is undefined.
Thus Turing computability allows partial functions, because a machine may fail to halt on some inputs.
Definition 10.20 (Recursive Computable Function)
A partial function:
is recursive computable if it belongs to the class of partial recursive functions, meaning that it can be obtained from the initial functions by finitely many applications of composition, primitive recursion, and minimization.
When such a function is defined on every input, it is called general recursive or total recursive.
Definition 10.21 (Lambda Definable Function)
A partial function:
is lambda definable if there is a lambda term that, under a fixed coding of natural numbers, transforms the codes of:
into the code of:
whenever this value is defined.
The details of this definition depend on a coding of natural numbers inside lambda calculus, but different standard codings lead to the same class of computable functions.
Principle 10.22 (Church Turing Thesis)
A numerical function is effectively computable if and only if it is computable by a Turing machine, equivalently if and only if it is partial recursive, equivalently if and only if it is lambda definable.
This is called a thesis rather than a theorem because one side of the statement uses the informal phrase “effectively computable”. A theorem can relate two formal definitions, but the Church Turing thesis relates a formal definition to an informal concept.
The thesis does not say that every mathematical function is computable. It says that whenever there is an algorithm in the ordinary sense, that algorithm can be represented in the formal models of computation.
Why It Is Not a Theorem
A theorem requires precisely defined hypotheses and conclusions. For example, the statement “every primitive recursive function is recursive” is a theorem, because both “primitive recursive” and “recursive” are formal definitions.
The Church Turing thesis has a different status. The phrase “effectively computable” was introduced to capture an intuitive notion of algorithmic calculability. Since that notion is not itself a formal mathematical definition, there is no direct formal proof that it is equivalent to Turing computability.
What can be proved are equivalence theorems between formal systems. One can prove that Turing computable functions are exactly the partial recursive functions, and one can prove that lambda definable functions are exactly the Turing computable functions. These results give strong evidence for the thesis, but the final identification with the informal notion remains a foundational principle.
Theorem 10.23 (Equivalence of Standard Formal Models)
The following classes of partial numerical functions are the same.
The partial recursive functions.
The Turing computable functions.
The lambda definable functions.
The register machine computable functions.
Proof
We prove the theorem by describing simulations between the models. Since each model can simulate the others, every function computable in one model is computable in the remaining models.
First, every partial recursive function is Turing computable. The initial functions are easily computed by Turing machines. A Turing machine can compute the zero function by ignoring its input and writing . It can compute the successor function by adding one to the input. It can compute projection functions by extracting the required component from a coded tuple.
The closure operations are also Turing computable. If and are Turing computable, then their composition is Turing computable by first computing each on the input and then applying the machine for to the resulting outputs. If a function is defined by primitive recursion, a Turing machine can compute it by iterating the recursive step a finite number of times, using the recursion variable as a counter. If a function is defined by minimization, a Turing machine can search through:
until it finds the first value satisfying the required condition. If no such value exists, the machine never halts, which matches the intended partiality of minimization.
Thus every partial recursive function is Turing computable.
Second, every Turing computable function is partial recursive. To see this, encode configurations of a Turing machine by natural numbers. A configuration records the current state, the tape contents, and the head position. Since each finite tape segment can be coded by a natural number, every complete finite configuration can be represented by one natural number.
The transition function of the Turing machine then becomes an arithmetical function on codes of configurations. This one step transition function is primitive recursive because it only inspects and updates finitely many coded components. By iterating this transition function, one obtains a primitive recursive function giving the code of the configuration after steps.
Now define a predicate:
which says that the machine with code , on input , has halted by time . This predicate is primitive recursive because one can compute the configuration after steps and check whether it is halting.
The output of the machine is obtained by minimization:
If the machine halts, this finds the first halting time and then extracts the output from the halting configuration. If the machine never halts, the minimization search never terminates. Therefore the function computed by the Turing machine is partial recursive.
Third, lambda calculus can simulate recursive functions and Turing machines by representing natural numbers and finite data using lambda terms. The standard Church numerals represent natural numbers, and lambda terms can express composition, recursion, and conditional behavior. Conversely, reduction of lambda terms can be simulated by a Turing machine, since lambda terms are finite symbolic expressions and beta reduction is a mechanical rewriting operation.
Finally, register machines can simulate Turing machines by storing tape data and machine states in registers, while Turing machines can simulate register machines by coding registers on a tape. Therefore the register machine computable functions coincide with the same class.
Since all these models compute the same partial functions on natural numbers, the standard formal models of computation are equivalent.
Coding Finite Objects by Natural Numbers
The proof above relies on the fact that finite symbolic objects can be coded by natural numbers. This idea is fundamental in computability theory.
A finite sequence:
can be coded by a single natural number. One common method uses prime powers:
The exponents can be recovered by prime factorization. Other codings are possible, and the choice of coding does not affect computability as long as encoding and decoding are themselves computable.
This allows machines, programs, formulas, proofs, and finite computation histories to be treated as natural numbers. Once this is done, statements about computation can be converted into statements about arithmetic.
Lemma 10.24 (Finite Sequences Can Be Effectively Coded)
There is an effective coding of finite sequences of natural numbers by natural numbers such that the length function, projection functions, and concatenation operation are computable.
Proof
Choose a standard coding of finite sequences. For example, encode:
by:
where is the th prime number.
The length of the sequence can be recovered by searching for the largest prime whose exponent is nonzero. The th entry can be recovered by computing the exponent of in the prime factorization and subtracting . Concatenation can be computed by multiplying the appropriate prime powers after shifting indices.
Each of these operations is effective because it involves bounded or systematic search over natural numbers, divisibility tests, and arithmetic operations that are computable. Therefore finite sequences can be encoded and manipulated effectively.
Programs as Numbers
Because finite sequences can be coded by natural numbers, programs can also be coded by natural numbers. A Turing machine has finitely many states, finitely many tape symbols, and finitely many transition rules, so its full description is a finite object.
Thus every Turing machine has a code:
We may write:
for the partial function computed by the machine with code on input .
The notation:
means that the computation halts, and:
means that the computation does not halt.
This notation is important because it lets us speak about all computable functions in a single enumeration:
Lemma 10.25 (Enumeration of Partial Computable Functions)
The partial computable functions can be effectively enumerated as:
Proof
Every program or Turing machine has a finite description, and every finite description can be coded by a natural number. Therefore we can list all natural numbers and interpret each one as a possible machine code.
Some numbers may not code valid machines. In that case, assign them a default machine, such as a machine that never halts. This ensures that every natural number indexes some partial computable function.
Since every valid machine has some finite code, every partial computable function computed by a machine appears somewhere in the list. Hence the partial computable functions admit an effective enumeration.
Universal Computation
Once programs can be coded by numbers, there can be a single machine that takes a program code and an input, and then simulates the program on that input.
Theorem 10.26 (Universal Machine)
There exists a partial computable function:
such that:
whenever is defined, and:
whenever .
Proof
On input , the universal computation first decodes as the description of a Turing machine. If does not code a valid machine, the universal computation may run forever or simulate a default nonhalting machine.
If codes a valid machine, the universal computation reconstructs the machine’s transition rules and begins simulating its execution on input . At each stage, it stores the simulated configuration, applies one transition rule, and updates the simulated configuration.
If the simulated machine eventually halts with output , the universal computation halts and outputs . If the simulated machine never halts, the simulation also never halts.
All steps of decoding, updating configurations, and checking halting states are effective operations on finite symbolic data. Therefore the universal function is partial computable.
Relation to the Halting Problem
The universal machine shows that computation itself can be treated as data. This is one of the main reasons undecidability appears.
The halting relation is:
This relation asks whether the program with code halts on input .
The Church Turing thesis lets us interpret the undecidability of this relation as a statement about all algorithms, not merely about one particular formal machine model. If no Turing machine decides the halting problem, then no effective procedure decides it.
Theorem 10.27 (Halting Relation is Semidecidable)
The relation:
is semidecidable.
Proof
To semidecide , run the universal machine .
If halts, then the universal machine eventually observes this halting computation and halts. If does not halt, then the universal machine continues the simulation forever.
Thus there is a procedure that halts exactly on the pairs for which halts. Therefore is semidecidable.
Why the Thesis Matters
The Church Turing thesis makes computability theory mathematically useful because it permits proofs about one formal model to be read as proofs about algorithms in general.
If a function is shown to be Turing computable, then it is reasonable to regard it as effectively computable.
If a problem is shown to be impossible for Turing machines, then by the thesis it is impossible for any effective procedure.
This is why undecidability results are strong. They do not merely say that a specific programming language fails to solve a problem. They say that no algorithmic method can solve the problem.
Decidable and Semidecidable Problems
A decision problem is decidable if there is an algorithm that halts on every input and gives the correct yes or no answer.
A decision problem is semidecidable if there is an algorithm that halts on yes instances, but may run forever on no instances.
The distinction between decidability and semidecidability is one of the central themes of computability theory. The Church Turing thesis justifies treating this distinction as a statement about effective methods in general.
For example, the halting relation is semidecidable because one can simulate a computation and wait for it to halt. It is not decidable, as later sections will show, because there is no general effective method for determining in finite time that an arbitrary computation will never halt.
The Extended Church Turing Thesis
The Church Turing thesis concerns what can be computed at all. A stronger statement, often called the extended Church Turing thesis, concerns efficient computation.
The extended thesis says that every physically realizable computation can be simulated by a probabilistic Turing machine with at most polynomial overhead.
This is not the same as the ordinary Church Turing thesis. The ordinary thesis concerns computability, while the extended thesis concerns complexity.
Quantum computation challenges some interpretations of the extended thesis, because quantum algorithms appear to solve certain problems more efficiently than known classical algorithms. This does not refute the ordinary Church Turing thesis, because quantum computers still compute functions that are Turing computable.
Mathematical Consequences
The acceptance of the Church Turing thesis gives a precise working meaning to the phrase “there is an algorithm”. Instead of reasoning informally about all possible mechanical procedures, one may reason formally about Turing machines, recursive functions, or any other equivalent model.
This has several consequences.
First, computability becomes a mathematical property of functions.
Second, algorithms can be encoded as natural numbers and studied arithmetically.
Third, universal computation becomes possible, since one machine can simulate all machines.
Fourth, undecidability results become robust, because they apply to every effective procedure rather than to a single formalism.
Fifth, the boundary between total computable functions and partial computable functions becomes a central object of study.