2. Substitution and Beta-Reduction

2. Substitution and Beta-Reduction#

Goal. Implement capture-avoiding substitution and explore beta-reduction. Then compare normal-order and applicative-order evaluation.

You will learn

The meaning of substitution t[x := u] and why capture avoidance is necessary
How to implement capture-avoiding substitution with alpha-renaming
What a beta-redex is and how beta-reduction performs function application
How normal-order and applicative-order strategies differ (termination vs divergence)
How to read substitution and reduction traces using the visual widgets

Roadmap#

Define substitution and identify variable capture.
Implement capture-avoiding substitution subst.
Implement one-step beta-reduction and normalization.
Compare normal-order and applicative-order on terminating/diverging examples.
Use the substitution diagram and reduction player to build intuition.

Definition (Substitution)

t[x := u] means: replace free occurrences of x in t by u.

Substitution must avoid variable capture, which happens when a free variable in u becomes bound after substitution.

We’ll reuse the same AST from the first notebook for a self-contained implementation.

from pathlib import Path
import sys

book_root = Path.cwd()
if not (book_root / "lc_core.py").exists():
    book_root = book_root.parent
if str(book_root) not in sys.path:
    sys.path.insert(0, str(book_root))

from lc_core import (
    Var,
    Lam,
    App,
    show,
    free_vars,
    all_vars,
    rename_bound,
    alpha_rename,
    fresh_var,
    subst,
    is_redex,
    beta_step_normal,
    beta_step_applicative,
    normalize,
)

Definition (Capture-Avoiding Substitution)

When substituting into λx. t, if the bound variable x would capture a free variable in the replacement, we must first rename the binder.

# `subst` is imported from lc_core as the canonical capture-avoiding implementation.
print("Using shared subst from lc_core")

Using shared subst from lc_core

Example (Avoiding Capture)

Substitute y := x into λx. y. Naive substitution would give λx. x, which changes meaning.

Capture-avoiding substitution renames the binder first, giving λx0. x.

term = Lam("x", Var("y"))
replaced = subst(term, "y", Var("x"))
print(show(term))
print(show(replaced))

(lambda x. y)
(lambda x0. x)

Visual: Substitution Diagram (Capture Avoidance)#

Capture-avoiding substitution: [x := y] in λy. (x y)

Start: λy. (x y)

binder y conflicts with free y in replacement

alpha-rename: λy0. (x y0)

fresh name y0 avoids capture

substitute x := y

beta-safe replacement

Result: λy0. (y y0)

Definition (Beta-Reduction)

A beta-redex is an application of a lambda abstraction: (λx. t) u.

Beta-reduction replaces it by t[x := u].

def is_redex(t: Term) -> bool:
    return isinstance(t, App) and isinstance(t.fn, Lam)

def beta_step_normal(t: Term):
    if is_redex(t):
        return subst(t.fn.body, t.fn.param, t.arg), True
    if isinstance(t, App):
        new_fn, changed = beta_step_normal(t.fn)
        if changed:
            return App(new_fn, t.arg), True
        new_arg, changed = beta_step_normal(t.arg)
        if changed:
            return App(t.fn, new_arg), True
        return t, False
    if isinstance(t, Lam):
        new_body, changed = beta_step_normal(t.body)
        if changed:
            return Lam(t.param, new_body), True
        return t, False
    return t, False

def beta_step_applicative(t: Term):
    if isinstance(t, App):
        new_fn, changed = beta_step_applicative(t.fn)
        if changed:
            return App(new_fn, t.arg), True
        new_arg, changed = beta_step_applicative(t.arg)
        if changed:
            return App(t.fn, new_arg), True
        if is_redex(t):
            return subst(t.fn.body, t.fn.param, t.arg), True
        return t, False
    if isinstance(t, Lam):
        new_body, changed = beta_step_applicative(t.body)
        if changed:
            return Lam(t.param, new_body), True
        return t, False
    return t, False

def normalize(step_fn, t: Term, limit: int = 50):
    current = t
    for _ in range(limit):
        current, changed = step_fn(current)
        if not changed:
            return current
    return current

Example

Compare normal-order vs applicative-order on a diverging argument.

In this notebook, both strategies compute full normal forms (they also reduce under λ), not just weak-head forms.

# Omega = (λx. x x) (λx. x x)
omega = App(Lam("x", App(Var("x"), Var("x"))), Lam("x", App(Var("x"), Var("x"))))
const_y = Lam("x", Var("y"))
term = App(const_y, omega)

normal = normalize(beta_step_normal, term, limit=30)
applic = normalize(beta_step_applicative, term, limit=30)

print("Normal-order:", show(normal))
print("Applicative-order (truncated):", show(applic))

Normal-order: y
Applicative-order (truncated): ((lambda x. y) ((lambda x. (x x)) (lambda x. (x x))))

Visual: Animated Reduction Trace#

((lambda x. x) ((lambda z. z) w))

((lambda z. z) w)

w

The controls let you scrub the reduction path step by step.

Exercise

Show that (λx. x) ((λy. y) z) reduces to z.
Find a term that normalizes under normal-order but diverges under applicative-order.
Compute subst(λy. x, x := y) and explain why the binder must be renamed.
Implement a weak-head normalizer (do not reduce under λ) and compare its output to full normalization on λx. ((λy. y) x). See solution: Exercise 2 (Substitution and Reduction)

Summary#

Substitution replaces free occurrences; correct substitution must avoid variable capture.
Beta-reduction is substitution-driven: (λx. t) u -> t[x := u].
Normal-order can terminate on terms where applicative-order diverges (classic Omega examples).
Full normalization reduces under lambdas; weak-head normalization does not.
Operationally: use normalize(beta_step_normal, t) to explore normal-order, and compare to the applicative reducer.
Next: Church booleans and building logical connectives from functions alone (Chapter 3).