8. Mathematical Induction in the Lambda Calculus

8. Mathematical Induction in the Lambda Calculus#

Goal. Prove identities about Church arithmetic for all n (not just for a few numerals) and learn how to document the proof steps as runnable code.

You will learn

How to read a Church numeral n as an induction/iteration principle
How to separate formal proofs, proof sketches, and finite checks in this book
How to use a symbolic lambda-calculus AST (Var/Lam/App) to record beta-reduction traces
How to prove basic arithmetic laws by induction (base + step)
How these induction lemmas support later arithmetic proofs (Chapter 9)

Roadmap#

Reintroduce Church numerals and the arithmetic operations we will reason about.
Set up a tiny symbolic lambda-calculus engine for readable reduction traces.
Prove the key step laws for add and mul (trace style).
Write induction proof scripts for core identities (base + step).
Connect right-recursive multiplication mulR to Church mul.
Use the trace visualizer to inspect one nontrivial step.

Definition (Induction as Iteration)

A Church numeral n is an iterator: given a base case and a step, it applies the step n times.

Induction combinator (informal): IND n base step ≡ n step base

If base is a proof of P(0) and step maps a proof of P(n) to a proof of P(S n), then IND n base step yields a proof of P(n).

Remark (Proof Notions Used Below)

We use two proof styles side-by-side:

Formal proof: a symbolic derivation (beta/eta/alpha) plus an explicit induction base/step argument.
Finite check: a bounded Python loop over small numerals, used only as a sanity check.

When both appear, treat the finite check as a unit test for the general proof.

Setup (Church Numerals)#

from pathlib import Path
import sys

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

from church_core import (
    TRUE,
    FALSE,
    AND,
    to_bool,
    church,
    to_int,
    from_int,
    succ,
    add,
    mul,
    pair,
    fst,
    snd,
    pred,
    sub,
    is_zero,
    eq_church,
)

zero = church(0)
one = church(1)
two = church(2)

eq = eq_church

A Tiny Lambda‑Calculus Engine (for Proof Traces)#

We implement a symbolic lambda calculus to show explicit beta‑reduction steps. This is used to document the algebraic proofs.

Equality checks in this chapter compare terms up to beta-reduction, eta-reduction, and alpha-equivalence (binder renaming).

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,
    trace_reduce,
    nf,
    alpha_eq,
    eta_step,
    eta_nf,
    defeq,
)

Definitions as Lambda Terms#

We now encode 0, succ, add, and mul as symbolic lambda terms, to get explicit reduction traces.

# Lambda-calculus encodings (symbolic)

def L(x, body):
    return Lam(x, body)


def A(f, a):
    return App(f, a)


def add_term(a, b):
    return A(A(add_l, a), b)


def mul_term(a, b):
    return A(A(mul_l, a), b)


def succ_term(a):
    return A(succ_l, a)


zero_l = L("f", L("x", Var("x")))

succ_l = L(
    "n",
    L(
        "f",
        L(
            "x",
            A(Var("f"), A(A(Var("n"), Var("f")), Var("x"))),
        ),
    ),
)

add_l = L(
    "m",
    L(
        "n",
        L(
            "f",
            L("x", A(A(Var("m"), Var("f")), A(A(Var("n"), Var("f")), Var("x"))))
        ),
    ),
)

mul_l = L(
    "m",
    L(
        "n",
        L("f", A(Var("m"), A(Var("n"), Var("f"))))
    ),
)

Proof Trace Style (Key Lemmas)#

Lemma 1: `add (S n) m = S (add n m)`#

We reduce the left-hand side and show it matches the right-hand side.

# Trace for add (succ n) m
n = Var("n")
m = Var("m")
term = add_term(succ_term(n), m)

steps = trace_reduce(term, max_steps=10)
for i, s in enumerate(steps):
    print(f"{i}: {show(s)}")

(((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)) m)
((lambda n0. (lambda f. (lambda x. ((((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n) f) ((n0 f) x))))) m)
(lambda f. (lambda x. ((((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n) f) ((m f) x))))
(lambda f. (lambda x. (((lambda f. (lambda x. (f ((n f) x)))) f) ((m f) x))))
(lambda f. (lambda x. ((lambda x. (f ((n f) x))) ((m f) x))))
(lambda f. (lambda x. (f ((n f) ((m f) x)))))

You should see the normal form:

λf. λx. f (n f (m f x))

which is exactly S (add n m).

Lemma 2: `mul (S n) m = add m (mul n m)`#

With Church multiplication as repeated composition,

\[ (S\,n)\cdot m = m + (n\cdot m), \]

which is definitionally aligned with the normal forms produced by the symbolic reducer.

left = mul_term(succ_term(n), m)
right = add_term(m, mul_term(n, m))

left_nf = nf(left)
right_nf = nf(right)

print("Left NF :", show(left_nf))
print("Right NF:", show(right_nf))
print("Match:", show(left_nf) == show(right_nf))

Left NF : (lambda f. (lambda x. ((m f) ((n (m f)) x))))
Right NF: (lambda f. (lambda x. ((m f) ((n (m f)) x))))
Match: True

Induction Proof Scripts (Executable)#

We now document full induction proofs with explicit base and step reasoning. The scripts print the term equalities that justify each step.

# Utility: rewrite exact subterm occurrences

def rewrite(term: Term, pattern: Term, replacement: Term) -> Term:
    if term == pattern:
        return replacement
    if isinstance(term, Var):
        return term
    if isinstance(term, Lam):
        return Lam(term.param, rewrite(term.body, pattern, replacement))
    if isinstance(term, App):
        return App(rewrite(term.fn, pattern, replacement), rewrite(term.arg, pattern, replacement))
    raise TypeError("Unknown term")


def print_defeq(label, a, b):
    print(label)
    print("  LHS NF:", show(nf(a)))
    print("  RHS NF:", show(nf(b)))
    print("  Equal:", defeq(a, b))


n = Var("n")
m = Var("m")

Theorem 1: `n + 0 = n`#

Full proof (by induction on n).

Base n = 0:

add 0 0 = (λm. λn. λf. λx. m f (n f x)) 0 0 → λf. λx. 0 f (0 f x) → λf. λx. x (by unfolding 0) = 0.
Step assume add n 0 = n.

Then:

add (S n) 0 = S (add n 0) by Lemma 1 = S n by IH.

# Base case: add 0 0 = 0
base_lhs = add_term(zero_l, zero_l)
base_rhs = zero_l
print_defeq("Base: add 0 0 = 0", base_lhs, base_rhs)

# Step: add (S n) 0 = S (add n 0), then rewrite by IH
step_lhs = add_term(succ_term(n), zero_l)
step_mid = succ_term(add_term(n, zero_l))
print_defeq("Step 1: add (S n) 0 = S (add n 0)", step_lhs, step_mid)

# Apply IH rewrite: add n 0 -> n
step_mid_rewritten = rewrite(step_mid, add_term(n, zero_l), n)
print("Step 2: apply IH to get", show(step_mid_rewritten))
print("Result equals S n:", show(step_mid_rewritten) == show(succ_term(n)))

Base: add 0 0 = 0
  LHS NF: (lambda f. (lambda x. x))
  RHS NF: (lambda f. (lambda x. x))
  Equal: True
Step 1: add (S n) 0 = S (add n 0)
  LHS NF: (lambda f. (lambda x. (f ((n f) x))))
  RHS NF: (lambda f. (lambda x. (f ((n f) x))))
  Equal: True
Step 2: apply IH to get ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) n)
Result equals S n: True

Theorem 2: `n + S(m) = S(n + m)`#

Full proof (by induction on n, for fixed m).

Base n = 0:

add 0 (S m) = S m and S (add 0 m) = S m.
Step assume add n (S m) = S (add n m).

Then:

add (S n) (S m) = S (add n (S m)) by Lemma 1 = S (S (add n m)) by IH = S (add (S n) m) by Lemma 1.

# Base case for fixed m
base_lhs = add_term(zero_l, succ_term(m))
base_rhs = succ_term(add_term(zero_l, m))
print_defeq("Base: add 0 (S m) = S (add 0 m)", base_lhs, base_rhs)

# Step case
step_lhs = add_term(succ_term(n), succ_term(m))
step_mid1 = succ_term(add_term(n, succ_term(m)))
print_defeq("Step 1: add (S n) (S m) = S (add n (S m))", step_lhs, step_mid1)

# Apply IH: add n (S m) -> S (add n m)
step_mid2 = rewrite(step_mid1, add_term(n, succ_term(m)), succ_term(add_term(n, m)))
print("Step 2: apply IH:", show(step_mid2))

# Reduce RHS: S (add (S n) m)
step_rhs = succ_term(add_term(succ_term(n), m))
print_defeq("Step 3: S (S (add n m)) = S (add (S n) m)", step_mid2, step_rhs)

Base: add 0 (S m) = S (add 0 m)
  LHS NF: (lambda f. (lambda x. (f ((m f) x))))
  RHS NF: (lambda f. (lambda x. (f ((m f) x))))
  Equal: True
Step 1: add (S n) (S m) = S (add n (S m))
  LHS NF: (lambda f. (lambda x. (f ((n f) (f ((m f) x))))))
  RHS NF: (lambda f. (lambda x. (f ((n f) (f ((m f) x))))))
  Equal: True
Step 2: apply IH: ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) m)))
Step 3: S (S (add n m)) = S (add (S n) m)
  LHS NF: (lambda f. (lambda x. (f (f ((n f) ((m f) x))))))
  RHS NF: (lambda f. (lambda x. (f (f ((n f) ((m f) x))))))
  Equal: True

Theorem 3: `n * 0 = 0`#

Full proof (by induction on n).

Base n = 0:

mul 0 0 = 0 by beta‑reduction.
Step assume mul n 0 = 0.

Then:

mul (S n) 0 = add (mul n 0) 0 by Lemma 2 = add 0 0 = 0 by IH and Theorem 1.

# Base case: mul 0 0 = 0
base_lhs = mul_term(zero_l, zero_l)
base_rhs = zero_l
print_defeq("Base: mul 0 0 = 0", base_lhs, base_rhs)

# Step case
step_lhs = mul_term(succ_term(n), zero_l)
step_mid = add_term(mul_term(n, zero_l), zero_l)
print_defeq("Step 1: mul (S n) 0 = add (mul n 0) 0", step_lhs, step_mid)

# Apply IH: mul n 0 -> 0
step_mid2 = rewrite(step_mid, mul_term(n, zero_l), zero_l)
print("Step 2: apply IH:", show(step_mid2))
print_defeq("Step 3: add 0 0 = 0", step_mid2, zero_l)

Base: mul 0 0 = 0
  LHS NF: (lambda f. (lambda x. x))
  RHS NF: (lambda f. (lambda x. x))
  Equal: True
Step 1: mul (S n) 0 = add (mul n 0) 0
  LHS NF: (lambda f. (lambda x. ((n (lambda x. x)) x)))
  RHS NF: (lambda f. (lambda x. ((n (lambda x. x)) x)))
  Equal: True
Step 2: apply IH: (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) (lambda f. (lambda x. x))) (lambda f. (lambda x. x)))
Step 3: add 0 0 = 0
  LHS NF: (lambda f. (lambda x. x))
  RHS NF: (lambda f. (lambda x. x))
  Equal: True

Right‑Recursive Multiplication and the Peano Identity#

The Peano axiom for multiplication is usually stated as:

n * S(m) = n*m + n.

Our Church encoding of mul is left‑recursive (it reduces neatly when the left argument is a successor). To give a full induction proof of the Peano identity, we define a right‑recursive multiplication mulR by primitive recursion on the right argument. The proof below is then a direct induction on m.

# Right‑recursive multiplication by primitive recursion on the right argument
# Uses eager fixpoint; see execution_notes.md for IF_THUNK
IF_THUNK = lambda b: (lambda t: (lambda f: b(t)(f)()))
Z = lambda f: (lambda x: f(lambda v: x(x)(v)))(lambda x: f(lambda v: x(x)(v)))

mulR = Z(
    lambda rec: (
        lambda n: (
            lambda m: IF_THUNK(is_zero(m))(
                lambda: zero
            )(
                lambda: add(n)(rec(n)(pred(m)))
            )
        )
    )
)

Theorem 4 (Peano Form): `n * S(m) = n*m + n` (for `mulR`)#

Full proof (by induction on m).

Base m = 0:

mulR n (S 0) = add(n)(mulR n 0) by definition = add n 0 = n.

Also n*m + n = n*0 + n = 0 + n = n.
Step assume mulR n (S m) = mulR n m + n.

Then:

mulR n (S (S m)) = add(n)(mulR n (S m)) by definition = add(n)(mulR n m + n) by IH = (mulR n m + n) + n.

This is exactly mulR n (S m) + n, completing the step.

Thus mulR satisfies the Peano recursion.

# Executable illustration for Theorem 4 (prints the base/step identities)

def proof_peano_mulR(n_val=3, m_val=2):
    N = from_int(n_val)
    M = from_int(m_val)

    print("Base m=0:")
    left = mulR(N)(succ(zero))
    right = add(N)(mulR(N)(zero))
    print("  mulR n (S 0) =", to_int(left))
    print("  add n (mulR n 0) =", to_int(right))

    print("Step (sample m):")
    left = mulR(N)(succ(succ(M)))
    mid = add(N)(mulR(N)(succ(M)))
    print("  mulR n (S (S m)) =", to_int(left))
    print("  add n (mulR n (S m)) =", to_int(mid))

proof_peano_mulR()

Base m=0:
  mulR n (S 0) = 3
  add n (mulR n 0) = 3
Step (sample m):
  mulR n (S (S m)) = 12
  add n (mulR n (S m)) = 12

Connecting `mulR` with Church `mul`#

Both mulR and mul represent multiplication of Church numerals. A full formal proof of their extensional equality can be given by induction on the right argument (using Lemma 1 and Theorem 1). The code below performs a sanity check for small numerals.

Theorem 5: `mulR n m = mul n m` (for all `n, m`)#

Proof sketch (induction on m).

We show that the right-recursive multiplication mulR agrees extensionally with Church mul.

Base m = 0:

mulR n 0 = 0 by definition of mulR.

mul n 0 = 0 by Theorem 3.

Hence mulR n 0 = mul n 0.
Step assume mulR n m = mul n m.

Then

mulR n (S m) = add n (mulR n m) by definition of mulR = add n (mul n m) by IH.

To conclude = mul n (S m), we use the multiplication successor law for Church numerals.

So the theorem is justified by induction plus the multiplication step law; the code below gives symbolic trace + finite sanity checks.

# Executable documentation for Theorem 5
# We show the base and step equalities symbolically and numerically.

# Base: mulR n 0 = mul n 0
N = from_int(3)
base_left = mulR(N)(zero)
base_right = mul(N)(zero)
print("Base: mulR n 0 =", to_int(base_left), ", mul n 0 =", to_int(base_right))

# Step: mulR n (S m) = add n (mulR n m) and equals mul n (S m)
M = from_int(2)
step_left = mulR(N)(succ(M))
step_mid = add(N)(mulR(N)(M))
step_right = mul(N)(succ(M))
print("Step left :", to_int(step_left))
print("Step mid  :", to_int(step_mid))
print("Step right:", to_int(step_right))

Base: mulR n 0 = 0 , mul n 0 = 0
Step left : 9
Step mid  : 9
Step right: 9

Symbolic rewrite trace (structural proof)

We now show the step equation purely in lambda‑calculus terms: mulR n (S m) = add n (mulR n m) = mul n (S m).

We represent mulR as a symbolic constant and encode the step as a rewrite chain. This is a symbolic proof sketch in the same calculus, independent of numeric evaluation.

# Symbolic trace for Theorem 5 (step equation)
# We treat mulR as a symbolic constant M (since its definition uses recursion).

M = Var("mulR")
n = Var("n")
m = Var("m")

# Notation: mulR n m  is  ((mulR n) m)
mulR_nm = App(App(M, n), m)
mulR_nSm = App(App(M, n), App(succ_l, m))

# Step equation: mulR n (S m) = add n (mulR n m)
step_rhs = add_term(n, mulR_nm)

print("LHS:", show(mulR_nSm))
print("RHS:", show(step_rhs))
print("This is the definitional equation of mulR (by primitive recursion on m).")

# Use IH: mulR n m = mul n m
mul_nm = mul_term(n, m)
step_rhs_ih = rewrite(step_rhs, mulR_nm, mul_nm)
print("After IH rewrite:", show(step_rhs_ih))

# Final target form for the step
step_final = mul_term(n, App(succ_l, m))
print("Target:", show(step_final))
print("This final equality is extensional; see arithmetic proof text above.")

LHS: ((mulR n) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) m))
RHS: (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) ((mulR n) m))
This is the definitional equation of mulR (by primitive recursion on m).
After IH rewrite: (((lambda m. (lambda n. (lambda f. (lambda x. ((m f) ((n f) x)))))) n) (((lambda m. (lambda n. (lambda f. (m (n f))))) n) m))
Target: (((lambda m. (lambda n. (lambda f. (m (n f))))) n) ((lambda n. (lambda f. (lambda x. (f ((n f) x))))) m))
This final equality is extensional; see arithmetic proof text above.

Visual: Animated Step-Law Trace#

mulR n (S m)

add n (mulR n m)

add n (mul n m)

mul n (S m)

This animation is a structural guide; the chapter text still provides the induction proof obligations.

# Sanity check: mulR equals mul for a small range
for a in range(5):
    for b in range(5):
        A = from_int(a)
        B = from_int(b)
        if to_int(mulR(A)(B)) != to_int(mul(A)(B)):
            raise ValueError("mulR != mul at", a, b)
print("mulR == mul for a,b < 5 (sanity check)")

mulR == mul for a,b < 5 (sanity check)

Remark

Most proofs above are formal beta-reduction/induction derivations. The mulR = mul section is presented as an induction proof sketch with symbolic rewrite trace and finite sanity checks.

Exercise

Prove add n m = add m n by induction on n, using Lemma 1. Then verify with code for a small range.
Prove associativity of addition: add (add n m) k = add n (add m k) by induction on n. Then verify with code for a small range.
Use the symbolic reducer (trace_reduce) to print a beta-reduction trace of add_term (succ_term zero_l) (succ_term zero_l) down to normal form.
Prove mul n one = n by induction on n, using Lemma 2 and the addition identities. Then verify with code for a small range. See solutions: Exercise 8 (Induction)

Summary#

A Church numeral n is an iterator, which can be read as an induction principle: apply a step n times to a base case.
Step laws like add (S n) m = S(add n m) and mul (S n) m = add m (mul n m) are the computational backbone of induction proofs.
A symbolic AST lets us document beta-reduction traces explicitly, which is useful for proof-like explanations.
A finite check is a sanity test, not a proof; the proof lives in the base/step argument and the rewrite trace.
These induction patterns are reused in Chapter 9 to build witness-producing arithmetic certificates.

8. Mathematical Induction in the Lambda Calculus

Contents