Church-Turing Thesis

The Capstone

The Church-Turing thesis states that the class of functions computable by any effective mechanical procedure is exactly the class of functions computable in lambda calculus (equivalently, by Turing machines, or by mu-recursive functions).

This means lambda calculus is not a toy. It is not a simplified model that captures "some" computation. It captures all of it. Anything a computer can compute -- any program in any language -- has an equivalent lambda calculus expression.

The thesis is the capstone of everything we have built: three forms, one operation, and from them, all of computation.

Three Models

In the 1930s, three independent formalisations of "computation" emerged:

• Lambda calculus (Church, 1936): computation as function application and substitution
• Turing machines (Turing, 1936): computation as a head reading and writing symbols on a tape
• Mu-recursive functions (Kleene, 1936): computation as composition of basic arithmetic operations with minimisation

These three systems look nothing alike. Lambda calculus has no tape. Turing machines have no functions. Mu-recursive functions have no substitution. Yet all three compute exactly the same class of functions. Every function computable in one system is computable in both of the others.

This convergence from radically different starting points is the strongest evidence for the Church-Turing thesis. When every reasonable formalisation of "computation" arrives at the same boundary, that boundary is likely fundamental.

Thesis Not Theorem

The Church-Turing thesis is not called the Church-Turing theorem. This distinction matters.

A theorem is a statement proved from axioms using formal logic. A thesis is a claim about the relationship between an informal concept and a formal one.

The Church-Turing thesis claims that the informal notion of "effectively computable" (what a human could compute by following a mechanical procedure) corresponds exactly to the formal notion of "lambda-definable" (or equivalently, Turing-computable, or mu-recursive).

The problem: "effectively computable" is an intuitive concept, not a mathematical definition. You cannot write a formal proof that an informal idea equals a formal one. The thesis is supported by overwhelming evidence -- every reasonable formalisation of computation has turned out to be equivalent -- but it remains, in principle, unprovable.

Turing Complete

A system is Turing complete if it can simulate any Turing machine. Since Turing machines are a formal model of everything that is computable (per the Church-Turing thesis), Turing completeness means: the system can compute anything that is computable.

Lambda calculus is Turing complete. This is not a conjecture -- it is a proven mathematical fact. Church and Turing showed in 1936 that lambda-definable functions and Turing-computable functions are the same class. Any computation a Turing machine can perform, lambda calculus can perform through substitution alone.

This is why every programming language that is Turing complete (virtually all of them) is equivalent in computational power to lambda calculus. Python, C, Haskell, JavaScript -- none of them can compute anything that lambda calculus cannot.

From Almost Nothing

Lambda calculus has exactly three term forms:

1. Variable: x -- a name
2. Abstraction: λx.M -- a function with a parameter
3. Application: M N -- applying a function to an argument

And one computational operation:

• Beta reduction: (λx.M) N →β M[x := N] -- substitution

That is the entire system. There are no built-in numbers, booleans, conditionals, loops, data structures, or recursion mechanisms. Every one of those concepts was constructed from these three forms and this one operation.

No other formalisation of computation starts from so little and arrives at so much.

What We Built

Starting from nothing but substitution, we constructed:

• Booleans: TRUE and FALSE as selectors (λx.λy.x, λx.λy.y)
• Numbers: Church numerals as iteration counts (λf.λx.f(f(f x)))
• Arithmetic: addition, multiplication, exponentiation from composed iteration
• Pairs: two values bundled with a selector (λx.λy.λs.s x y)
• Lists: chains of pairs with a nil sentinel

Each of these was surprising. But one construction stands above the rest: the ability to define recursion without any self-referential mechanism. The Y combinator creates looping from self-application -- a lambda term that feeds itself to itself.

Recursion is what makes lambda calculus Turing complete. Without it, we could build data and operations but not unbounded computation. With it, we can compute anything.

Equivalent Models

A common reaction to lambda calculus is: "This is elegant, but real programs need loops, variables, memory, and I/O. Lambda calculus is a toy."

The Church-Turing thesis says otherwise. Every Turing complete system computes the same class of functions. Python is Turing complete. Lambda calculus is Turing complete. Therefore any function computable in Python is computable in lambda calculus, and vice versa.

This does not mean lambda calculus is convenient for writing web servers. It means that no programming language can compute something that lambda calculus cannot. The features that real languages add -- loops, mutable state, objects, types -- are conveniences for humans. They add no computational power that substitution does not already provide.

The Journey

The journey through lambda calculus traces a single arc:

Start: Three term forms (variable, abstraction, application) and one operation (substitution). No built-in meaning of any kind.

Middle: Church encodings reveal that booleans, numbers, arithmetic, data structures, and recursion were already present in the patterns. We did not add features -- we discovered capabilities.

End: The Church-Turing thesis confirms that what we built is not a fragment of computation. It is all of computation. Lambda calculus computes exactly the class of functions that any mechanical process can compute.

From almost nothing, everything.