Lambda Calculus
Computation from Functions Alone

add = lambda x: lambda y: x + y      # curried: one argument at a time
inc = add(1)                         # partial application
print(inc(41), add(2)(3), (lambda x: x * x)(5))

42 5 25

Conventions (to drop brackets)

• Application is left-associative: f a b = (f a) b.
• A body stretches as far right as it can: λx. x y = λx. (x y).
• Nested λs merge: λx y. M = λx. λy. M.

Examples

Currying

There are only one-argument functions. A two-argument function returns a function: λx. λy. M. The idea is named after Haskell Curry, but Schönfinkel had it first (1924).

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

print(sorted(free(parse(r"λx. x y z"))))

['y', 'z']

Shadowing

In λx. (λx. x) x the inner x refers to the inner binder. The last x refers to the outer one. It is exactly like nested scopes in Python:

f = lambda x: (lambda x: x)(x + 1)
print(f(1))   # inner x is 2

Output: 2

λx. x y z        => (λx. ((x y) z))        FV = ['y', 'z']
λx y. y x        => (λx. (λy. (y x)))      FV = []
(λx. x) y z      => (((λx. x) y) z)        FV = ['y', 'z']
λx. (λy. x y) y  => (λx. ((λy. (x y)) y))  FV = ['y']
x λy. y x        => (x (λy. (y x)))        FV = ['x']

Output of the deck's parse and free, printed with full brackets.

A worked reduction

(λx. λy. x) a b
= ((λx. λy. x) a) b
→_β (λy. a) b
→_β a

Two steps, normal form a. Our reducer agrees (next slides):

t, n = normalize(parse(r"(λx. λy. x) a b"))
print(show(t), n)

a 2

SUCC 1 = 2

SUCC = λn f x. f (n f x) and 1 = λf x. f x.

0: (λn.λf.λx.f (n f x)) (λf.λx.f x)
1: λf.λx.f ((λf.λx.f x) f x)
2: λf.λx.f ((λx.f x) x)
3: λf.λx.f (f x)

1. Step 1. The redex is the whole term. Put 1 in for n.
2. Step 2. No redex at the top: it is a λ. So go under the binders. The leftmost redex is (λf.λx.f x) f. Put f in for f.
3. Step 3. Now (λx.f x) x. Put x in for x. Done: two fs, the numeral 2.

def trace(t):                         # print every normal-order step
    n = 0; print(f"{n}: {show(t)}")
    while (t2 := step(t)) is not None:
        n += 1; t = t2; print(f"{n}: {show(t)}")
trace(parse(r"(λn f x. f (n f x)) (λf x. f x)"))

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:
    fn: object
    arg: object

def show(t):
    if isinstance(t, Var): return t.name
    if isinstance(t, Lam): return f"λ{t.param}.{show(t.body)}"
    f = show(t.fn) if not isinstance(t.fn, Lam) else f"({show(t.fn)})"
    a = show(t.arg) if isinstance(t.arg, Var) else f"({show(t.arg)})"
    return f"{f} {a}"

Frozen dataclasses give free structural equality and hashing.

print(show(parse(r"λx. λy. x y")))
print(show(parse(r"(λx. x x) (λx. x x)")))

λx.λy.x y
(λx.x x) (λx.x x)

import re

def parse(src):
    toks = re.findall(r"[λ\\.()]|[A-Za-z0-9_']+", src)
    pos = 0
    def peek(): return toks[pos] if pos < len(toks) else None
    def eat(t=None):
        nonlocal pos
        tok = toks[pos]; pos += 1
        assert t is None or tok == t, f"expected {t}, got {tok}"
        return tok
    def term():                        # term := λx y. term | application
        if peek() in ("λ", "\\"):
            eat(); names = []
            while peek() != ".": names.append(eat())
            eat(".")
            body = term()
            for n in reversed(names): body = Lam(n, body)
            return body
        t = atom()
        while peek() not in (None, ")"):   # application is left-assoc
            t = App(t, atom() if peek() not in ("λ", "\\") else term())
        return t
    def atom():
        if peek() == "(":
            eat("("); t = term(); eat(")"); return t
        return Var(eat())
    t = term(); assert pos == len(toks); return t

def step(t):
    """One leftmost-outermost β-step, or None if t is normal."""
    if isinstance(t, App):
        if isinstance(t.fn, Lam):
            return subst(t.fn.body, t.fn.param, t.arg)
        r = step(t.fn)
        if r is not None: return App(r, t.arg)
        r = step(t.arg)
        return None if r is None else App(t.fn, r)
    if isinstance(t, Lam):
        r = step(t.body)
        return None if r is None else Lam(t.param, r)
    return None

def normalize(t, limit=10_000):
    for n in range(limit):
        nxt = step(t)
        if nxt is None: return t, n
        t = nxt
    raise RuntimeError("no normal form within limit")

That is why normalize uses this order. Other orders can loop on terms that do have an answer. The next slide shows one.

The limit is required. Whether a term has a normal form is undecidable, so no reducer can always tell.

omega = parse(r"(λx. x x) (λx. x x)")
print(show(step(omega)) == show(omega))

True

Throw-away argument

Now take K∗ = λx. λy. y. It ignores its first argument.

t, n = normalize(parse(r"(λx. λy. y) ((λx. x x) (λx. x x))"))
print(show(t), n)

λy.y 1

Normal order is done in one step. It never touches Ω.

Consequences

• Normal forms are unique up to α. The order you pick can change whether you finish, never what you get.
• M =_β N exactly when both reduce to a common term.
• The theory is consistent. λx y. x and λx y. y are different normal forms, so they are not equal.

Proof sketch (Tait & Martin-Löf)

1. Plain →_β lacks the one-step diamond. A step can copy a redex, which then needs two steps.
2. Define parallel reduction ⇒. It fires any set of existing redexes at once.
3. Show ⇒ has the diamond property. Use the complete development M*, which fires all redexes. Every M ⇒ N has N ⇒ M*.
4. →_β ⊆ ⇒ ⊆ →*, so both have the same closure. Diamond for ⇒ tiles into confluence.

Next: with only β, we will build booleans, numbers, pairs, lists and recursion.

Check: AND TRUE FALSE

(λp q. p q p) TRUE FALSE
→* TRUE FALSE TRUE
→* FALSE

We run these in the reducer. A macro table DEFS expands names into terms before normalizing:

DEFS = {"TRUE": r"λt f. t", "FALSE": r"λt f. f",
        "AND": r"λp q. p q p", "NOT": r"λp. p FALSE TRUE",
        "PAIR": r"λa b s. s a b", "FST": r"λp. p TRUE", ...}

t, n = run("AND TRUE FALSE"); print(show(t))
t, n = run("NOT FALSE"); print(show(t))
t, n = run("FST (PAIR a b)"); print(show(t))

λt.λf.f
λt.λf.t
a

The full DEFS, expand and run are in the test file. run expands macros, then calls normalize.

def church(k):
    body = Var("x")
    for _ in range(k): body = App(Var("f"), body)
    return Lam("f", Lam("x", body))

def to_int(t):
    """Read back λf.λx. f (f ... x)."""
    t, _ = normalize(t)
    f, x, body, k = t.param, t.body.param, t.body.body, 0
    while isinstance(body, App):
        assert body.fn == Var(f); body = body.arg; k += 1
    assert body == Var(x)
    return k

for expr in ["PLUS 2 3", "MULT 3 3", "POW 2 3", "PRED 5", "SUB 7 4"]:
    t, n = run(expr)
    print(f"{expr:<9} = {to_int(t)}   ({n} β-steps)")

PLUS 2 3  = 5   (6 β-steps)
MULT 3 3  = 9   (9 β-steps)
POW 2 3   = 8   (16 β-steps)
PRED 5    = 4   (15 β-steps)
SUB 7 4   = 3   (68 β-steps)

Numbers are unary, so costs grow with the value. SUB 7 4 runs PRED four times, which is why it is slow.

Adding an f is easy. Removing one is not, because a numeral only knows how to apply f. Church thought PRED might be impossible.

Pair version (easier to read)

STEP = λp. PAIR (SND p) (SUCC (SND p))
PRED = λn. FST (n STEP (PAIR 0 0))

Start at (0,0). Each step maps (a,b) ↦ (b,b+1). After n steps: (n−1, n). Take the first part. PRED 0 = 0.

The compact version we ran

PRED = λn f x. n (λg h. h (g f)) (λu. x) (λu. u)

• λu. x is a "container" that skips the first f.
• Each step wraps one more f around the contents.
• λu. u opens the final container.

From the numerals slide: PRED 5 = 4 in 15 steps and SUB 7 4 = 3 in 68 steps.

Church numerals make PRED cost O(n). Other encodings (Scott, Parigot) make it O(1) and pay elsewhere.

TRUE  = lambda t: lambda f: t
FALSE = lambda t: lambda f: f
AND   = lambda p: lambda q: p(q)(p)
NOT   = lambda p: p(FALSE)(TRUE)
ZERO  = lambda f: lambda x: x
SUCC  = lambda n: lambda f: lambda x: f(n(f)(x))
PLUS  = lambda m: lambda n: lambda f: lambda x: m(f)(n(f)(x))
MULT  = lambda m: lambda n: lambda f: m(n(f))
POW   = lambda b: lambda e: e(b)
PRED  = lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f)))(lambda u: x)(lambda u: u)

to_py  = lambda n: n(lambda k: k + 1)(0)
to_bool = lambda b: b(True)(False)
ONE, TWO = SUCC(ZERO), SUCC(SUCC(ZERO))
THREE = PLUS(ONE)(TWO)

print(to_py(MULT(THREE)(THREE)), to_py(POW(TWO)(THREE)), to_py(PRED(THREE)))
print(to_bool(AND(TRUE)(NOT(FALSE))))

9 8 2
True

Why this works in Python

• Python has first-class closures. A lambda captures its free variables.
• Curried, one-argument lambdas match λ exactly.
• Python is call-by-value. That is fine here, since nothing diverges.

Compare numerals: 3 = λf x. f (f (f x)). A numeral is a list with no payload. Both are instances of Böhm–Berarducci encoding. Any algebraic data type can be written as its own fold.

NIL    = lambda c: lambda n: n
CONS   = lambda h: lambda t: lambda c: lambda n: c(h)(t(c)(n))
FOLD   = lambda xs: lambda f: lambda z: xs(f)(z)
xs = CONS(1)(CONS(2)(CONS(3)(NIL)))
print(FOLD(xs)(lambda h: lambda acc: h + acc)(0))
print(FOLD(xs)(lambda h: lambda acc: [h] + acc)([]))

6
[1, 2, 3]

We want FACT = λn. IF (ISZERO n) 1 (MULT n (FACT (PRED n))). But a term cannot mention itself. So we abstract the self-reference away:

F = λr n. IF (ISZERO n) 1 (MULT n (r (PRED n)))

Now FACT must satisfy FACT = F FACT. FACT is a fixed point of F.

Y in the pure reducer

DEFS["Y"] = r"λf. (λx. f (x x)) (λx. f (x x))"
DEFS["FACT"] = r"Y (λr n. IF (ISZERO n) 1 (MULT n (r (PRED n))))"
t, n = run("FACT 3")
print("FACT 3 =", to_int(t), f"({n} β-steps)")

FACT 3 = 6 (694 β-steps)

This works because normal order unfolds Y F only when the IF needs it. At n = 0, the recursive branch is simply thrown away.

F = λr n. IF (ISZERO n) 1 (MULT n (r (PRED n))) and FACT = Y F. Use Y F = F (Y F) as a macro step:

   FACT 2
=  Y F 2
=  F (Y F) 2                          unfold Y once
-> IF (ISZERO 2) 1 (MULT 2 (Y F (PRED 2)))
-> MULT 2 (Y F 1)                     ISZERO 2 = FALSE
=  MULT 2 (F (Y F) 1)                 unfold Y again
-> MULT 2 (MULT 1 (Y F 0))            ISZERO 1 = FALSE
=  MULT 2 (MULT 1 (F (Y F) 0))        unfold Y a third time
-> MULT 2 (MULT 1 1)                  ISZERO 0 = TRUE: stop
-> 2

Each "unfold" is Y F =_β F (Y F). Each "→" hides several β-steps.

Counted with the deck's run and to_int. Unary numbers make costs grow fast.

Y in Python loops forever

Y = lambda f: (lambda x: f(x(x)))(lambda x: f(x(x)))
try:
    Y(lambda self: lambda n: 1 if n == 0 else n * self(n - 1))
except RecursionError:
    print("Y: RecursionError (Python is call-by-value)")

Y: RecursionError (Python is call-by-value)

Python evaluates x(x) before it calls f. That gives another x(x), and so on. The stack blows up before any number is used.

Z = lambda f: (lambda x: f(lambda v: x(x)(v)))(lambda x: f(lambda v: x(x)(v)))
fact = Z(lambda self: lambda n: 1 if n == 0 else n * self(n - 1))
fib  = Z(lambda self: lambda n: n if n < 2 else self(n - 1) + self(n - 2))
print(fact(10), [fib(i) for i in range(10)])

3628800 [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

Python's recursion limit still applies. Each self(...) call adds a few stack frames.

The output blows up. Naive translation can be exponential in term size. Turner's extra combinators B and C (1979) fix most of that. His SASL and Miranda ran on SKI graph reduction.

def abstract(x, t):
    if t == Var(x): return C("I")
    if not occurs(x, t): return App(C("K"), t)
    return App(App(C("S"), abstract(x, t.fn)), abstract(x, t.arg))

def bracket(t):
    """Compile a λ-term to S, K, I by bracket abstraction."""
    if isinstance(t, (Var, C)): return t
    if isinstance(t, App): return App(bracket(t.fn), bracket(t.arg))
    return abstract(t.param, bracket(t.body))

for src in [r"λx. x", r"λx y. x", r"λx y. y x", r"λf x. f (f x)"]:
    print(f"{src:<15} ⇒  {sshow(bracket(parse(src)))}")
swap = bracket(parse(r"λx y. y x"))
print(sshow(ski_norm(App(App(swap, Var("a")), Var("b")))))

λx. x           ⇒  I
λx y. x         ⇒  S (K K) I
λx y. y x       ⇒  S (K (S I)) (S (K K) I)
λf x. f (f x)   ⇒  S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))
b a

S (K K) I is η-equal to K. Add the rule [x](M x) = M when x ∉ FV(M) to get K directly. C, occurs, sshow and the S/K/I step function ski_norm are in the test file.

Sketch: μ-recursive ⇒ λ

• Zero, successor, projections: λx. 0, SUCC, λx₁…x_k. x_i.
• Composition: plain application.
• Primitive recursion: iterate a pair, as with PRED.
• μ (unbounded search): use Y to loop until a test is zero.

Sketch: λ ⇒ Turing machine

Write terms on the tape as strings. A TM can find the leftmost redex and do substitution. Our step function is exactly such a program.

Scott–Curry theorem: any nontrivial set of terms closed under =_β is undecidable. It is the λ version of Rice's theorem.

• α-equivalence becomes plain equality. No renaming, no capture.
• Cost: β must shift indices of free variables when moving under a binder.
• Used inside Coq, Lean, Agda, and many compilers. Humans still read named syntax.

(λ M) N → ↑⁻¹( M[0 := ↑¹N] )

def debruijn(t, ctx=()):
    if isinstance(t, Var):
        return str(ctx.index(t.name)) if t.name in ctx else t.name
    if isinstance(t, Lam):
        return "λ " + debruijn(t.body, (t.param,) + ctx)
    f = debruijn(t.fn, ctx); a = debruijn(t.arg, ctx)
    f = f"({f})" if isinstance(t.fn, Lam) else f
    a = f"({a})" if not isinstance(t.arg, Var) else a
    return f"{f} {a}"

for src in [r"λx. x", r"λx y. x", r"λz w. z", r"λf x. f (f x)", r"λx. λy. x (λz. z y)"]:
    print(f"{src:<22} {debruijn(parse(src))}")

λx. x                  λ 0
λx y. x                λ λ 1
λz w. z                λ λ 1
λf x. f (f x)          λ λ 1 (1 0)
λx. λy. x (λz. z y)    λ λ 1 (λ 0 1)

ctx.index finds the nearest binder, since new names go on the front. Note the same variable y is 1 inside the inner λ but would be 0 outside it.

def typeof(t, env={}):
    if isinstance(t, Var):
        return env[t.name]
    if isinstance(t, TLam):
        return Arrow(t.ty, typeof(t.body, {**env, t.param: t.ty}))
    fn, arg = typeof(t.fn, env), typeof(t.arg, env)
    if not isinstance(fn, Arrow) or fn.a != arg:
        raise TypeError(f"cannot apply {tshow(fn)} to {tshow(arg)}")
    return fn.b

print(tshow(typeof(K)))          # λx:A. λy:B. x
print(tshow(typeof(compose)))    # λf:B→C. λg:A→B. λx:A. f (g x)
try:
    typeof(TLam("x", A, App(Var("x"), Var("x"))))
except TypeError as e:
    print("TypeError:", e)

A → B → A
(B → C) → (A → B) → A → C
TypeError: cannot apply A to A

Read the types we just checked

• K : A → B → A proves "if A, then (if B then A)".
• compose : (B→C) → (A→B) → A → C proves that implication is transitive.
• S : (A→B→C) → (A→B) → A → C. With K, these are the two axioms of Hilbert-style logic. So SKI is a Hilbert proof system.

Curry saw it for combinators (1934). Howard wrote it for natural deduction (1969, published 1980).

Leave out every type. Can we still find one? Yes. Give each unknown a type variable, gather equations, and solve them by unification (Robinson, 1965).

• Var: look up its type.
• λx. M: new variable a for x. The type is a → type(M).
• M N: new r. Unify type(M) with type(N) → r.
• Occurs check: a = a → b has no finite answer, so reject it.
• let-polymorphism: let gets ∀ types. It is left out here for size.

Worst case is exponential (nested lets). It is near-linear in practice. ML, OCaml, Haskell, F#, Elm and Rust's local inference all build on it.

def infer(t, env, s):
    if isinstance(t, Var): return env[t.name], s
    if isinstance(t, Lam):
        a = tv(); b, s = infer(t.body, {**env, t.param: a}, s)
        return Arrow(a, b), s
    f, s = infer(t.fn, env, s); a, s = infer(t.arg, env, s)
    r = tv(); s = unify(f, Arrow(a, r), s)
    return r, s

for src in [r"λx. x", r"λx y. x", r"λf g x. f (g x)",
            r"λf x. f (f x)", r"λx. x x"]:
    try:
        ty, s = infer(parse(src), {}, {})
        print(f"{src:<18} : {pretty(resolve(ty, s))}")
    except TypeError as e:
        print(f"{src:<18} : TypeError: {e}")

λx. x              : a → a
λx y. x            : a → b → a
λf g x. f (g x)    : (a → b) → (c → a) → c → b
λf x. f (f x)      : (a → a) → a → a
λx. x x            : TypeError: infinite type

tv, unify (with occurs check), resolve and pretty are in the test file, about 30 lines. Note the type of Church numeral 2: (a→a)→a→a.