Turing completeness

Turing completeness is the presence of branching, repetition and data. All the ingredients have already been assembled in the previous sections:

• data — Church encoding (section “Church encoding”): booleans, pairs, numerals, lists;
• branching — a Church boolean picks the branch itself: $\mathrm{if}$ $\equiv \lambda b\,t\,e.\,b\,t\,e$;
• loops — the fixed-point combinator (section “Curry's Y combinator”): $\mathrm{Y}\,F$ $=_\beta F\,(\mathrm{Y}\,F)$, recursion without names and without counters.

This is enough to model a Turing machine: the tape is a list, the state is a numeral, a step is branching, repeating the steps is $\mathrm{Y}$. Turing completeness comes at a price — undecidability. There is no algorithm that, given a term, decides whether it has a normal form: this is the λ-counterpart of the halting problem.

Now, totality. A language is called total if every one of its programs terminates on every input. Turing completeness is incompatible with totality. In the λ-calculus infinite loops are possible:

Languages that chose totality do exist — for example, Agda. The Agda compiler checks every function: all input cases must be covered, and recursive calls must go to structurally smaller arguments. Addition of natural numbers passes the check — the recursive call is on $n$ — a strictly smaller part of $\mathtt{suc}\ n$:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero  + m = m
suc n + m = suc (n + m)   -- the call is on n: strictly smaller than suc n

And this one Agda will reject:

loop : ℕ → ℕ
loop n = loop n           -- Termination checking failed: n does not decrease

The price is symmetric: Agda is not Turing complete — $\Omega$ cannot be written in it. In return, every program is a total function, and by the Curry–Howard correspondence (section “The Curry–Howard correspondence”) it can be read as a proof. Haskell picks the middle ground: a typed core plus general recursion ($\mathtt{fix}$, recursive let) — completeness returns, and with it infinite loops.