10.4 Formal Models of Computation

The Church Turing thesis says that the informal idea of effective computation is captured by several equivalent formal models, and this section describes the main models that are used in computability theory. The purpose is not to develop every model in full technical detail, but to explain what each model treats as a computation, how it represents data, and why it defines the same class of computable functions.

A formal model of computation must specify three things. First, it must specify how inputs and outputs are represented. Second, it must specify what counts as one computational step. Third, it must specify when a computation has halted and what output has been produced. Once these ingredients are fixed, the phrase “computable by the model” becomes a precise mathematical notion.

Turing Machines

A Turing machine is an abstract machine with a finite set of internal states, an infinite tape divided into cells, a tape head that can read and write symbols, and a transition rule that determines the next step from the current state and the symbol currently being read.

The tape should be understood as an idealized memory. At any moment, only finitely many cells contain nonblank symbols, but the tape is unbounded so that the computation never fails merely because it runs out of storage.

Definition 10.28 (Turing Machine)

A Turing machine consists of the following data:

M = (Q,\Gamma,\Sigma,\delta,q_0,q_{\mathrm{halt}})

Here $Q$ is a finite set of states, $\Gamma$ is a finite tape alphabet, $\Sigma \subseteq \Gamma$ is the input alphabet, $\delta$ is the transition function, $q_0 \in Q$ is the initial state, and $q_{\mathrm{halt}}\in Q$ is the halting state.

The transition function has the form:

\delta : (Q \setminus \{q_{\mathrm{halt}}\}) \times \Gamma \to Q \times \Gamma \times \{L,R\}.

If:

\delta(q,a) = (q',b,D),

then the machine, when in state $q$ reading symbol $a$ , changes to state $q'$ , writes symbol $b$ on the current tape cell, and moves the head in direction $D$ , where $D$ is either $L$ for left or $R$ for right.

Some definitions also allow a stay put move $S$ , but this does not change the class of computable functions.

Configurations

A configuration records the complete instantaneous state of a Turing machine computation. It includes the current state, the tape contents, and the position of the tape head.

Although the tape is infinite, only finitely many cells are nonblank at any finite stage of computation, so a configuration can be represented by finite data.

Definition 10.29 (Configuration)

A configuration of a Turing machine is a finite description of:

the current state $q$ ,

the finite nonblank portion of the tape,

the position of the tape head.

A configuration is halting if its state is:

q_{\mathrm{halt}}.

A computation of a Turing machine is a sequence of configurations:

C_0,C_1,C_2,\dots

where $C_0$ is the initial configuration and each $C_{i+1}$ is obtained from $C_i$ by one application of the transition function.

Turing Computable Functions

A Turing machine computes a partial function by starting with an input encoded on the tape and either halting with an output or running forever.

Definition 10.30 (Turing Computable Function)

A partial function:

f : \mathbb{N}^n \rightharpoonup \mathbb{N}

is Turing computable if there is a Turing machine $M$ such that, for every input:

(x_1,\dots,x_n)\in\mathbb{N}^n,

the machine $M$ halts with output $f(x_1,\dots,x_n)$ whenever this value is defined, and does not halt whenever this value is undefined.

This definition uses an encoding of tuples of natural numbers on the tape. Any standard effective encoding gives the same class of computable functions.

Example 10.31

The successor function:

S(x)=x+1

is Turing computable.

A machine computing $S$ may read the input number in unary notation, move to the end of the block of marks, add one additional mark, and halt. If $x$ is represented by $x$ marks, then adding one mark represents $x+1$ .

This example is simple, but it illustrates the central idea: computation consists of finite symbolic manipulation according to fixed local rules.

Register Machines

A register machine is another formal model of computation. Instead of a tape, it has finitely many registers, each holding a natural number. A program consists of simple instructions that modify registers and control the flow of execution.

Register machines are closer to ordinary low level programming than Turing machines, because they use named storage locations and explicit instructions.

Definition 10.32 (Register Machine)

A register machine has registers:

R_0,R_1,R_2,\dots,R_k

each containing a natural number, and a finite program made from instructions of the following kinds:

increment a register,

decrement a register if it is nonzero,

test whether a register is zero,

jump to another instruction,

halt.

The input is placed in some designated registers at the start of the computation, and the output is read from a designated register when the machine halts.

Example 10.33

A register machine can compute addition:

\operatorname{add}(x,y)=x+y.

Place $x$ in $R_0$ and $y$ in $R_1$ . Repeatedly decrement $R_1$ and increment $R_0$ until $R_1$ becomes $0$ . When the process halts, $R_0$ contains $x+y$ .

This algorithm is mechanical because each step is one of the allowed register instructions.

Lemma 10.34

Every register machine computable function is Turing computable.

Proof

A Turing machine can simulate a register machine by coding the contents of the registers on its tape. Since the register machine has only finitely many registers in its program, the Turing machine can store their values as finite blocks of symbols separated by delimiters.

To simulate an increment instruction, the Turing machine locates the block for the chosen register and adds one mark. To simulate a decrement instruction, it checks whether the block is empty; if it is not empty, it removes one mark. To simulate a zero test, it checks whether the block for the register contains any marks. To simulate a jump, it updates the coded instruction pointer.

Each register instruction is simulated by finitely many Turing machine steps. Therefore a finite register machine computation is simulated by a finite Turing machine computation, and an infinite register machine computation is simulated by an infinite Turing machine computation. Hence every register machine computable function is Turing computable.

Lemma 10.35

Every Turing computable function is register machine computable.

Proof

A register machine can simulate a Turing machine by coding the tape, head position, and state as natural numbers stored in registers.

One standard method codes the left part of the tape as one number and the right part of the tape as another number, using base expansion. The current state is stored in a separate register. Reading the current tape symbol corresponds to extracting a digit from one of these codes. Writing a symbol corresponds to changing that digit. Moving the head left or right corresponds to shifting digits between the two tape codes.

The required digit extraction, digit replacement, and shifting operations are computable by register machine programs using loops and arithmetic on natural numbers. Therefore one step of the Turing machine can be simulated by a finite register machine computation.

By repeating this simulation, the register machine follows the Turing machine computation exactly. If the Turing machine halts, the register machine halts with the same output. If the Turing machine does not halt, the register machine also does not halt. Hence every Turing computable function is register machine computable.

Recursive Functions

Recursive functions define computation without explicitly describing a machine. Instead, they define computable functions by closure under certain operations.

This model is arithmetical. It treats computation as a class of numerical functions generated from simple initial functions.

Definition 10.36 (Recursive Model)

The recursive function model begins with the zero functions, successor function, and projection functions, and closes under composition, primitive recursion, and minimization.

The functions obtained in this way are the partial recursive functions.

A partial function:

f : \mathbb{N}^n \rightharpoonup \mathbb{N}

is computable in this model if it is partial recursive.

Lemma 10.37

Every partial recursive function is Turing computable.

Proof

The proof is by induction on the construction of partial recursive functions.

The initial functions are Turing computable. A Turing machine can compute the zero function by erasing or ignoring the input and writing $0$ . It can compute the successor function by adding one to a numeral. It can compute a projection function by extracting one component from a coded tuple.

Composition is preserved by Turing computability. If $g$ and $h_1,\dots,h_k$ are computed by Turing machines, then a Turing machine can compute each $h_i$ on the input, store the results, and then run the machine for $g$ on those results.

Primitive recursion is preserved by Turing computability because a Turing machine can iterate the recursive step a finite number of times. Given:

f(\vec{x},0)=g(\vec{x})

and:

f(\vec{x},y+1)=h(\vec{x},y,f(\vec{x},y)),

the machine first computes $g(\vec{x})$ , then repeatedly applies the machine for $h$ exactly $y$ times.

Minimization is preserved by Turing computability because a Turing machine can search:

0,1,2,\dots

until it finds the least $y$ such that the given function has value $0$ . If no such $y$ exists, the search never terminates, which correctly represents partiality.

Thus every partial recursive function is Turing computable.

Lambda Calculus

Lambda calculus is a formal system for computation based on functions. Its expressions are called lambda terms, and computation is performed by rewriting terms using substitution.

Unlike Turing machines, lambda calculus has no tape and no states. Unlike recursive functions, it does not begin with numerical operations. Instead, it treats function abstraction and application as primitive.

Definition 10.38 (Lambda Terms)

Lambda terms are defined inductively as follows.

Every variable is a lambda term.

If $M$ is a lambda term and $x$ is a variable, then:

\lambda x . M

is a lambda term.

If $M$ and $N$ are lambda terms, then:

MN

is a lambda term.

The term $\lambda x . M$ represents the function that sends $x$ to $M$ , and the term $MN$ represents applying $M$ to $N$ .

Definition 10.39 (Beta Reduction)

Beta reduction is the rewriting rule:

(\lambda x . M)N \to M[x:=N].

Here $M[x:=N]$ means the term obtained by substituting $N$ for the free occurrences of $x$ in $M$ , avoiding variable capture.

Beta reduction is the basic computational step of lambda calculus.

Example 10.40

Consider:

(\lambda x . x)N.

By beta reduction:

(\lambda x . x)N \to N.

Thus $\lambda x . x$ acts as the identity function.

Lambda Definability

Natural numbers can be represented in lambda calculus by Church numerals.

The Church numeral for $n$ is:

\lambda f . \lambda x . f^n(x),

where $f^n(x)$ means applying $f$ to $x$ exactly $n$ times.

For example:

0 = \lambda f . \lambda x . x,

1 = \lambda f . \lambda x . f x,

2 = \lambda f . \lambda x . f(fx).

Definition 10.41 (Lambda Definable Function)

A function:

f : \mathbb{N}^n \rightharpoonup \mathbb{N}

is lambda definable if there is a lambda term $F$ such that, whenever $f(x_1,\dots,x_n)=y$ , the term:

F\overline{x_1}\cdots\overline{x_n}

reduces to:

\overline{y},

where $\overline{x}$ denotes the Church numeral for $x$ .

If $f(x_1,\dots,x_n)$ is undefined, the corresponding reduction does not reach a numeral.

Lemma 10.42

Every lambda definable function is Turing computable.

Proof

A lambda term is a finite symbolic object, and beta reduction is a mechanical rewriting operation on finite symbolic expressions. A Turing machine can store a lambda term on its tape, search for a reducible expression of the form:

(\lambda x . M)N,

and replace it by:

M[x:=N].

The substitution operation is effective because the terms are finite strings with a finite parse tree. Renaming bound variables to avoid capture is also effective.

Therefore a Turing machine can simulate beta reduction step by step. If a lambda term reduces to a numeral, the Turing machine eventually reaches that numeral and outputs the corresponding natural number. If the lambda reduction does not terminate, the Turing machine does not halt. Hence every lambda definable function is Turing computable.

Lemma 10.43

Every Turing computable function is lambda definable.

Proof

A Turing machine computation can be encoded inside lambda calculus by representing states, tape symbols, finite sequences, and transition rules as lambda terms.

Church numerals provide a representation of natural numbers. Pairs and finite lists can also be represented by lambda terms. Once configurations are represented, the transition function of the Turing machine can be represented as a lambda term that maps one configuration to the next.

A lambda term can then iterate this transition function until a halting configuration is reached. If the simulated Turing machine halts, the lambda term reduces to the encoded output. If the simulated Turing machine does not halt, the reduction does not terminate.

Thus every Turing computable function can be represented in lambda calculus.

Markov Algorithms and Rewriting Systems

Another way to formalize computation is by rewriting strings according to fixed rules. A rewriting system begins with an input string and repeatedly applies the first applicable rule until a halting rule is reached or no rule applies.

Definition 10.44 (String Rewriting System)

A string rewriting system consists of a finite alphabet and a finite list of rewriting rules:

u \to v,

where $u$ and $v$ are finite strings over the alphabet.

A computation begins with an input string and repeatedly replaces an occurrence of $u$ by $v$ according to the rules of the system.

Lemma 10.45

String rewriting systems can be simulated by Turing machines.

Proof

A Turing machine can store the current string on its tape. At each stage, it scans the string to find an occurrence of the left side of an applicable rewriting rule. If one is found, the machine replaces it with the corresponding right side. Since the list of rules is finite and each string involved is finite, this search and replacement process is effective.

If the rewriting system reaches a halting condition, the Turing machine halts with the corresponding output. If the rewriting process continues forever, the Turing machine also continues forever. Therefore every function computed by such a rewriting system is Turing computable.

Equivalence of the Models

The different formal models are equivalent because each model can simulate the basic computational steps of the others. This means that the choice of model affects convenience, not computability.

Theorem 10.46 (Equivalence of Formal Models)

The following classes of partial functions:

\mathbb{N}^n \rightharpoonup \mathbb{N}

are the same:

Turing computable functions,

partial recursive functions,

lambda definable functions,

functions computable by standard finite string rewriting systems.

Proof

The equivalence is obtained by the simulation lemmas.

Lemmas 10.34 and 10.35 show that Turing machines and register machines compute the same functions.

Lemma 10.37 shows that every partial recursive function is Turing computable, and the converse is proved by coding Turing machine configurations as natural numbers, defining the one step transition function recursively, and using minimization to find a halting time when one exists.

Lemmas 10.42 and 10.43 show that lambda definability and Turing computability coincide.

Lemma 10.45 shows that string rewriting systems are Turing computable, and the converse follows because the finite transition rules of a Turing machine can be encoded as rewriting rules on strings representing configurations.

Since each model can simulate a Turing machine and can itself be simulated by a Turing machine, all these models define the same class of partial numerical functions.

Why Several Models Are Useful

Although these models are equivalent in computational power, they are useful for different purposes.

Turing machines are useful for undecidability proofs because their configurations and halting behavior are concrete.

Recursive functions are useful for arithmetic and proof theory because they define computability using functions on natural numbers.

Lambda calculus is useful for programming language theory because it treats computation as symbolic function application.

String rewriting systems are useful because they connect computation with formal grammars, term rewriting, and symbolic manipulation.

The equivalence theorem allows results proved in one setting to be transferred to the others.