TCS: Church-Turing Thesis

Church-Turing Thesis

Recursion from Fixed Points

The fixed-point combinator from Lecture 1 turns a recursive equation into a term. First write a function that receives its recursive call as a parameter, then take its fixed point

For factorial, using the Boolean and numeral encodings from Lecture 2, define

$$\begin{aligned} F&=\lambda fn.\mathbf{if}\,(\mathbf{iszero}\,n)\, \overline1\,(\mathbf{mult}\,n\,(f(\mathbf{pred}\,n)))\\ \mathbf{fact}&=\mathbf YF \end{aligned}$$

Since $\mathbf{fact}=_\beta F\mathbf{fact}$, unfolding once gives the intended recurrence

$$\mathbf{fact}\,\overline n=_\beta \begin{cases} \overline1 & n=0\\ \mathbf{mult}\,\overline n\, (\mathbf{fact}\,\overline{n-1}) & n>0 \end{cases}$$

Induction on $n$ proves that normal-order evaluation reaches $\overline{n!}$. The evaluation strategy matters: eager evaluation of the recursive argument of $\mathbf Y$ can diverge before a conditional selects its branch

Pairs, Tuples and Lists

Data as an Interface

A pair packages two terms and waits for a selector to say how they should be used

The projection equations follow by substitution

$$\mathbf{fst}(\mathbf{pair}\,M\,N)\to_\beta^*M \qquad \mathbf{snd}(\mathbf{pair}\,M\,N)\to_\beta^*N$$

Similarly, encode a tuple as $\lambda c.cM_1\cdots M_k$ and obtain its $i$-th component by supplying $\lambda x_1\cdots x_k.x_i$

A Pair-Based List Encoding

Choose the following representation, with $h::t$ abbreviating $\mathbf{cons}\,h\,t$

$$\begin{aligned} \mathbf{nil}&=\lambda u.\mathbf T\\ \mathbf{cons}&=\mathbf{pair}\\ \mathbf{head}&=\mathbf{fst}\\ \mathbf{tail}&=\mathbf{snd}\\ \mathbf{empty}&=\lambda l.l(\lambda ht.\mathbf F) \end{aligned}$$

Applying $\mathbf{empty}$ to $\mathbf{nil}$ returns $\mathbf T$. Applying it to $h::t$ passes $h,t$ to a function that returns $\mathbf F$

The list operations use $\mathbf{head}$ and $\mathbf{tail}$ only after checking that the list is nonempty. Their behavior on the empty list is not part of their intended interface

Fold, Map and Filter

Define a right fold by its two equations

$$\begin{aligned} \mathbf{fold}\,\mathbf{nil}\,f\,z&=_\beta z\\ \mathbf{fold}\,(h::t)\,f\,z&=_\beta fh(\mathbf{fold}\,t\,f\,z) \end{aligned}$$

A fixed point realizes these equations

$$\mathbf{fold}=\mathbf Y \bigl(\lambda rlfz. \mathbf{if}\,(\mathbf{empty}\,l)\,z\, (f(\mathbf{head}\,l)(r(\mathbf{tail}\,l)fz))\bigr)$$

Then map and filter become choices of the combining function

$$\begin{aligned} \mathbf{map}&=\lambda lf. \mathbf{fold}\,l\,(\lambda ht.\mathbf{cons}\,(fh)\,t)\,\mathbf{nil}\\ \mathbf{filter}&=\lambda lp. \mathbf{fold}\,l\, (\lambda ht.\mathbf{if}\,(ph)\,(\mathbf{cons}\,h\,t)\,t)\, \mathbf{nil} \end{aligned}$$

For a finite list, structural induction establishes their intended behavior. All the data constructors and control flow are ordinary $\lambda$-terms

What Counts as Computation?

This is a claim connecting an informal notion with a formal model. In contrast, the equivalence between Turing machines and the $\lambda$-calculus is a mathematical theorem about two formal definitions

The thesis concerns which functions can be computed with unbounded finite time and memory. A separate efficiency thesis concerns the cost of simulating computational models

Turing Machines and Their Encodings

A deterministic Turing machine has finitely many states and tape symbols. Each transition reads the current symbol, writes a symbol, changes state, and moves the head

Its finite transition table can be encoded as a string $\langle M\rangle$. A universal machine interprets such a description and simulates $M$ on an input $w$

$$U(\langle M\rangle,w)\simeq M(w)$$

Here $\simeq$ allows partial behavior: if the simulated machine runs forever, the universal simulation also runs forever. Code and input are both finite strings, so programs can construct and inspect descriptions of other programs

Deciding, Recognizing and Reducing

A decider halts on every input with the correct membership answer. A recognizer accepts members but may run forever on nonmembers

Consider the halting language

$$\operatorname{HALT} =\{\langle M,w\rangle:M\text{ eventually halts on }w\}$$

It is recognizable by universal simulation. If a decider $H$ existed, construct $D$ that, on input $z$, loops when $H(\langle z,z\rangle)$ says the encoded machine halts, and halts otherwise. Running $D$ on its own description contradicts either answer

The acceptance language $\operatorname{ACC}_{\mathrm{TM}}$ is likewise recognizable and undecidable. For a deterministic computation model, a language is decidable exactly when both it and its complement are recognizable: dovetail the two recognizers until one accepts

Mapping Reductions

To prove a target problem $B$ undecidable, reduce an already undecidable problem to $B$. The transformation must finish on every input; it cannot wait indefinitely to discover whether the source machine halts

For example, transform $\langle M,w\rangle$ into a machine $N$ that ignores its input, simulates $M(w)$, and accepts if that simulation halts. Then $M$ halts on $w$ exactly when $N$ accepts the empty string

Why Lambda Calculus Is Turing Complete

The simulation has two directions

1. A Turing machine can store a finite $\lambda$-term as a syntax tree, perform capture-avoiding substitution, and follow normal-order reduction
2. A $\lambda$-term can encode machine states, tape symbols, finite lists, and the transition operation of a Turing machine

For the second direction, represent a configuration by its state, the current symbol, and lists containing the tape to the left and right of the head. A head movement pops one list and pushes onto the other, inserting a blank when necessary

Since the transition table is finite, comparisons and Boolean case selection implement a term $\mathbf{step}_M$ that maps a configuration to its successor

$$\mathbf{run}_M=\mathbf Y \bigl(\lambda rc. \mathbf{if}\,(\mathbf{halt}_M c)\, (\mathbf{output}_M c)\, (r(\mathbf{step}_M c))\bigr)$$

Each encoded machine step takes finitely many reductions. The recursive term returns the encoded output when the simulated machine halts, and continues unfolding when it does not

Thus both models represent the same partial computable functions under effective input and output encodings