λ-calculus, and its equivalence to Turing machines

Parent: logic

Church's λ-calculus (early 1930s) is the other definition of "computable" — born from functions, not machines. Same power, opposite temperament: Turing → computers, Church → proof assistants.

The calculus — three constructs, one rule

Terms and β-reduction

Terms: a variable x; an abstraction λx.M (the function x ↦ M); an application M N. The computation rule (β-reduction): (λx.M) N → M[x := N] — substitute the argument for the bound variable. (Plus α = renaming bound variables, η = extensionality.) Computing = β-reduce repeatedly until a normal form (no redex left), if one exists.

Everything is a function — there are no built-in numbers, booleans, or loops. They're all encoded.

Why it's Turing-strong

Church numerals: n ≡ λf.λx. f (f (… (f x))) — "apply f n times." Then succ, +, ×, exp are all λ-terms.
Data: true ≡ λx.λy.x, false ≡ λx.λy.y, pairs, lists — all encodable.
Recursion with no names: the Y combinator Y ≡ λf.(λx.f (x x)) (λx.f (x x)) satisfies Y g = g (Y g) — a fixed-point operator giving unbounded recursion. This is the λ-analog of Kleene's μ-operator / the while loop — exactly what lifts the calculus from primitive-recursive to full Turing power.

Reduce by hand

K a b = a (the "first" combinator), step by step — each ⇒ is one β-reduction:

(λx.λy.x) a b   ⇒   (λy.a) b   ⇒   a

Church arithmetic is just as mechanical — succ 0 = 1 with 0 ≡ λf.λx.x and succ ≡ λn.λf.λx. f (n f x):

(λn.λf.λx. f (n f x)) (λf.λx.x)
  ⇒  λf.λx. f ((λf.λx.x) f x)
  ⇒  λf.λx. f ((λx.x) x)
  ⇒  λf.λx. f x            = 1

As code — an interpreter is tiny

data Term = Var String | Lam String Term | App Term Term

subst :: String -> Term -> Term -> Term          -- [x := s] t  (naive; closed terms only)
subst x s (Var y)   = if x == y then s else Var y
subst x s (App a b) = App (subst x s a) (subst x s b)
subst x s (Lam y t) = if x == y then Lam y t else Lam y (subst x s t)

beta :: Term -> Maybe Term                        -- one normal-order step
beta (App (Lam x t) s) = Just (subst x s t)       -- the β-redex
beta (App a b)         = case beta a of
                           Just a' -> Just (App a' b)
                           Nothing -> App a <$> beta b
beta (Lam x t)         = Lam x <$> beta t
beta _                 = Nothing

normalize :: Term -> Term
normalize t = maybe t normalize (beta t)

The whole language is three constructors and one rule — β is a single pattern-match. (Real interpreters add α-renaming to avoid variable capture, elided here.)

The equivalence (Church, Kleene, Turing, 1936–37)

λ-definable = Turing-computable = general recursive

A number-theoretic function is definable by a λ-term (via Church numerals) iff it is computed by a Turing machine iff it is general recursive.

Proof

Fix the interface: a closed λ-term F computes f:ℕ→ℕ iff F ⌜n⌝ β-reduces to ⌜f(n)⌝ for every n, where ⌜n⌝ is the Church numeral. Claim: the F-definable and the TM-computable f coincide.

TM → λ. The transition table δ is finite, so it is a λ-term step that case-analyses the encoded (state, scanned symbol) — using the boolean/pair/list encodings — and returns the next configuration (symbol written, head moved, new state). Encode a whole configuration as a λ-term (tape = a pair of lists + head symbol + state). Then Y iterates step, with a boolean halted? test, until a halting state; reading off the tape yields ⌜f(n)⌝. So every TM-function is λ-definable.

λ → TM. Substitution M[x:=N] and "find the leftmost-outermost redex" are primitive-recursive operations on the string encoding of terms — so a Turing machine can perform one normal-order β-step and repeat. By the standardization theorem, normal-order reduction reaches the normal form whenever one exists; so the TM outputs ⌜f(n)⌝ exactly when F ⌜n⌝ has it.

Both simulations are effective, so the two classes of functions are equal (and, by Kleene, equal to the general recursive functions). ∎

Church–Rosser (confluence)

β-reduction is confluent: if a term reduces two different ways, the results can be brought back together. Hence a normal form is unique when it exists — the answer is order-independent even though reduction order is free.

Why it matters downstream

It is Church's witness for the Church–Turing thesis; Turing's 1936 paper added an appendix proving the equivalence, unifying the two roads.
Untyped λ-calculus is the root of functional programming (Lisp → ML → Haskell).
Add types → the typed λ-calculi, where terms carry types and the Curry–Howard correspondence makes programs = proofs, types = propositions → dependent type theory → Lean 4. That's the branch's spine from here.