Lambda Calculus

The whole language in three rules

In 1936 Alonzo Church was trying to pin down what "an effectively calculable function" actually means. His answer was startlingly small. Strip away numbers, loops, types, assignment, and data structures — keep only functions — and you still have enough to compute anything that any computer, in any language, ever could. That stripped-down system is the lambda calculus.

There are exactly three ways to build a term:

• Variable — a name like x.
• Abstraction — a one-argument anonymous function, written λx.M ("the function that takes x and returns the body M").
• Application — feeding one term to another, written M N ("apply function M to argument N").

That is the entire grammar: e ::= x | λx.e | e e. No built-in integers, no if, no while. Functions take exactly one argument; a two-argument function is faked by returning another function (this is currying, and it is why λx.λy.M is so common). Application binds tighter on the left, so f g h means (f g) h, and a lambda's body extends as far right as possible, so λx.x y is λx.(x y), not (λx.x) y.

Beta reduction: the only thing that "runs"

Computation is a single rewrite rule. When a function meets an argument, substitute the argument into the body:

(λx. M) N   →   M[x := N]

The left side — an abstraction applied to an argument — is called a redex (reducible expression). Running a program means finding a redex, performing the substitution, and repeating until none remain. The final irreducible form is the normal form, i.e. the answer. For example, the identity function applied to y:

(λx. x) y        →   y
(λx. λy. x) a b   →   (λy. a) b   →   a    // "const", ignores second arg

The hard part hides inside the word "substitute." Replacing a variable is only safe if you do not accidentally capture a different variable that happens to share a name. Consider (λx.λy.x) y: if you blindly replace x with the outer y, the inner binder swallows it and you get the wrong function. The fix is alpha conversion — silently rename bound variables so they never clash — which we cover in the implementation below. Get this wrong and your interpreter computes confidently incorrect answers.

Building numbers, booleans, and data out of functions

If the only thing you have is functions, then numbers, booleans, and lists must be functions. This is Church encoding.

A Church numeral n is the function that applies f to x exactly n times:

0 = λf.λx. x
1 = λf.λx. f x
2 = λf.λx. f (f x)
3 = λf.λx. f (f (f x))
SUCC = λn.λf.λx. f (n f x)      // add one more application
PLUS = λm.λn.λf.λx. m f (n f x) // chain m then n applications

Booleans are choices. TRUE picks its first argument, FALSE picks its second — which makes IF trivial:

TRUE  = λa.λb. a
FALSE = λa.λb. b
IF    = λc.λt.λe. c t e      // (IF TRUE  t e) → t,  (IF FALSE t e) → e
AND   = λp.λq. p q p
NOT   = λp. p FALSE TRUE

A pair bundles two values into a function that hands them to a selector, and lists are pairs of pairs — the same trick Lisp's cons uses. With numerals, booleans, and pairs you can encode every data structure you have ever used. The cost is that arithmetic on Church numerals is wildly inefficient compared to a register, but the point was never speed — it was demonstrating that everything reduces to substitution.

When the lambda calculus actually matters

• Designing or proving things about a language. Almost every functional language — Lisp, Scheme, ML, Haskell, OCaml, Elm — is lambda calculus plus syntax sugar. Type systems, evaluation order, and semantics are usually specified in a lambda-calculus core first, then desugared.
• Type theory and proof assistants. The Curry–Howard correspondence equates typed lambda terms with mathematical proofs and types with propositions. Coq, Lean, and Agda are, at their heart, dependently typed lambda calculi.
• Compiler intermediate representations. GHC's Core, and continuation-passing-style IRs in many compilers, are lambda calculus with annotations. Optimizations like inlining are literally beta reduction.
• Understanding closures and currying. JavaScript arrow functions, Python lambdas, and Rust closures all inherit their capture semantics straight from this model.

What it is not good for: writing real programs by hand. Nobody computes 5 × 7 with Church numerals in production. The value is conceptual and foundational, not operational.

Lambda calculus vs other models of computation

	Lambda calculus	Turing machine	SKI combinators	μ-recursive functions	Register machine
Core primitive	Function + application	Tape + state table	Two combinators (S, K)	Composition + recursion	Registers + jumps
State	None (rewriting)	Explicit tape head	None (rewriting)	None	Register contents
Variables / binding	Yes (the hard part)	No	None — variable-free	Numeric arguments	Register indices
Computational power	Turing-complete	Turing-complete	Turing-complete	Turing-complete	Turing-complete
Closest to real code	Functional languages	CPU fetch/execute	Point-free combinator libs	Math definitions	Assembly
Year	1936 (Church)	1936 (Turing)	1924–1930 (Schönfinkel/Curry)	1930s (Gödel/Kleene)	1960s (Shepherdson–Sturgis)

All five define exactly the same set of computable functions — that equivalence is the content of the Church–Turing thesis. They differ only in how they express computation. Turing machines model the imperative, state-mutating CPU; lambda calculus models the declarative, value-transforming function. SKI combinators are lambda calculus with the variables compiled away, which is why they power some of the most compact Turing-complete systems known.

What the numbers actually say

• Three primitives, zero built-ins. The full grammar is one line. By contrast a Turing machine needs an alphabet, a state set, and a transition table; the lambda calculus needs none of that scaffolding to reach the same power.
• Two combinators suffice. Every lambda term can be translated into combinations of just S = λx.λy.λz. x z (y z) and K = λx.λy. x. A single combinator (the Iota combinator) is even enough on its own.
• Church numeral arithmetic is wildly wasteful. Multiplying m × n by composing applications builds a term whose evaluation does on the order of m · n beta steps for a result a CPU produces in one instruction. Encoding is a proof of possibility, not a recipe for performance.
• Halting is undecidable. The term Ω = (λx.x x)(λx.x x) reduces to itself forever. No total algorithm can decide whether an arbitrary lambda term has a normal form — that is the lambda-calculus form of the halting problem, proved the same year.
• Reduction order changes whether you terminate, not the answer. The Church–Rosser theorem guarantees that if a term has a normal form, every terminating reduction path reaches the same one. Normal-order (leftmost-outermost) reduction will find that normal form whenever one exists; call-by-value may loop where normal order would have halted.

JavaScript implementation

The most direct way to feel the calculus is to embed it in a language with closures. JavaScript functions are lambda abstractions, so Church encodings run natively:

// Church booleans
const TRUE  = a => b => a;
const FALSE = a => b => b;
const IF    = c => t => e => c(t)(e);

// Church numerals
const ZERO = f => x => x;
const SUCC = n => f => x => f(n(f)(x));
const PLUS = m => n => f => x => m(f)(n(f)(x));
const MULT = m => n => f => m(n(f));

// Decode a Church numeral back to a JS number to inspect it
const toInt = n => n(x => x + 1)(0);

const TWO   = SUCC(SUCC(ZERO));
const THREE = SUCC(TWO);
console.log(toInt(PLUS(TWO)(THREE)));  // 5
console.log(toInt(MULT(TWO)(THREE)));  // 6

// Recursion with no names: the Y combinator (Z, the strict variant JS needs)
const Z = f => (x => f(v => x(x)(v)))(x => f(v => x(x)(v)));
const FACT = Z(self => n => n === 0 ? 1 : n * self(n - 1));
console.log(FACT(5));  // 120 — recursion built from a self-application trick

Notice that FACT never refers to its own name. Z hands the function a copy of itself as self. JavaScript is call-by-value, so we use the applicative-order fixed-point combinator Z rather than the textbook Y — plain Y would loop forever under eager evaluation because it tries to fully expand self before calling it.

Python implementation: a real interpreter

Closures show that the encodings work, but they hide the actual machinery. Here is a tiny interpreter that performs capture-avoiding substitution and beta reduction on an explicit syntax tree — the part that an interpreter really has to get right:

from dataclasses import dataclass

@dataclass(frozen=True)
class Var: name: str
@dataclass(frozen=True)
class Lam: param: str; body: object
@dataclass(frozen=True)
class App: func: object; arg: object

_counter = [0]
def fresh(base):
    _counter[0] += 1
    return f"{base}#{_counter[0]}"

def free_vars(t):
    if isinstance(t, Var): return {t.name}
    if isinstance(t, Lam): return free_vars(t.body) - {t.param}
    return free_vars(t.func) | free_vars(t.arg)

def subst(t, x, s):
    """t[x := s], renaming binders to avoid capture."""
    if isinstance(t, Var):
        return s if t.name == x else t
    if isinstance(t, App):
        return App(subst(t.func, x, s), subst(t.arg, x, s))
    # Lam
    if t.param == x:
        return t                       # x is shadowed: stop
    if t.param in free_vars(s):        # would capture: alpha-rename first
        new = fresh(t.param)
        body = subst(t.body, t.param, Var(new))
        return Lam(new, subst(body, x, s))
    return Lam(t.param, subst(t.body, x, s))

def reduce_once(t):
    """One normal-order (leftmost-outermost) beta step, or None if normal form."""
    if isinstance(t, App):
        if isinstance(t.func, Lam):                       # found a redex
            return subst(t.func.body, t.func.param, t.arg)
        f = reduce_once(t.func)
        if f is not None: return App(f, t.arg)
        a = reduce_once(t.arg)
        if a is not None: return App(t.func, a)
    if isinstance(t, Lam):
        b = reduce_once(t.body)
        if b is not None: return Lam(t.param, b)
    return None

def normalize(t, fuel=10_000):
    for _ in range(fuel):
        nxt = reduce_once(t)
        if nxt is None: return t       # normal form reached
        t = nxt
    raise RuntimeError("no normal form within fuel (maybe diverges)")

# (λx.λy.x) a b  →  a
I, K = Lam("x", Var("x")), Lam("x", Lam("y", Var("x")))
print(normalize(App(App(K, Var("a")), Var("b"))))   # Var(name='a')
print(normalize(App(I, Var("z"))))                  # Var(name='z')

The fuel parameter is not a stylistic choice — it is the halting problem made concrete. Because some terms (like Ω) never reach a normal form, any practical evaluator must bound its work or risk looping forever. There is no way to detect divergence in general before it happens.

Variants worth knowing

Simply typed lambda calculus (STLC). Add types and require every application to be well-typed. The price is dramatic: STLC is strongly normalizing — every term halts — which means it is no longer Turing-complete. You lose Ω and the Y combinator along with general recursion.

System F (polymorphic lambda calculus). Adds universal quantification over types (∀α. ...), the theory behind generics in ML and Haskell. Still strongly normalizing, vastly more expressive than STLC.

Calculus of Constructions / dependent types. Types can depend on values. This is the engine of proof assistants like Coq and Lean, where checking a proof is type-checking a lambda term.

SKI / BCKW combinator calculus. Lambda calculus with all variables compiled away into a fixed set of combinators. Equivalent in power, and the basis of "graph reduction" machines that implemented lazy functional languages in hardware.

Lambda calculus with explicit evaluation strategy. Call-by-name, call-by-value, and call-by-need (lazy) are not different calculi but different choices of which redex to reduce next. Haskell is call-by-need; ML and most mainstream languages are call-by-value.

Common bugs and edge cases

• Variable capture during substitution. The single most common interpreter bug. Substituting x := y into λy.x without renaming the binder turns a constant function into the identity. Always alpha-rename binders whose name is free in the incoming term.
• Choosing the wrong reduction order. Call-by-value evaluates arguments before calling, so it can diverge on a term that normal order would have discarded — e.g. (λx.λy.y) Ω loops eagerly but returns the identity lazily.
• Using plain Y under eager evaluation. The classic Y = λf.(λx.f (x x))(λx.f (x x)) diverges in a call-by-value language. You need the eta-expanded Z combinator to delay the self-application.
• Confusing alpha-equivalence with structural equality. λx.x and λy.y are the same function. Comparing terms by raw variable names gives false negatives; compare up to alpha (e.g. via de Bruijn indices, which drop names entirely).
• Expecting a normal form to always exist. By the halting problem it may not, so naïve "reduce until done" loops can hang. Bound the steps or detect known divergent patterns.
• Forgetting currying when counting arguments. λx.λy.M applied to one argument returns a function, not a partial error. Multi-argument intuitions from C or Python mislead here.