Recursive Definitions and Structural Induction

What This Concept Is

A recursive (or inductive) definition of a set $S$ gives:

1. A basis clause. One or more explicit elements belong to $S$.
2. One or more constructor clauses. Rules of the form "if $x_1, \ldots, x_k \in S$ (and possibly some external data), then $f(x_1, \ldots, x_k) \in S$."
3. An exclusion clause. Nothing else belongs to $S$.

Every element of $S$ is therefore obtained by finitely many applications of the constructors starting from the base, and every element has an (often unique) derivation tree witnessing its construction.

Structural induction is the proof principle matched to such definitions. To prove $\forall x \in S,\ P(x)$:

1. Base cases. Prove $P(b)$ for every explicit base element $b$.
2. Constructor cases. For each constructor $f$, assume $P(x_1), \ldots, P(x_k)$ (the structural IH) and prove $P(f(x_1, \ldots, x_k))$.

If all cases are discharged, $\forall x \in S,\ P(x)$ is proved.

Relationship to ordinary/strong induction. Structural induction generalises ordinary induction on $\mathbb{N}$: ordinary induction is structural induction on the recursive definition of $\mathbb{N}$ (base $0$, successor $n \mapsto n + 1$). It is also a form of well-founded induction over the relation "$x$ is a substructure of $y$." Thus it requires no new axioms on top of those already in play.

Typical recursively defined sets you will meet:

• Natural numbers: base $0$; constructor $\mathrm{succ}(n)$.
• Strings over $\Sigma$: base $\varepsilon$ (empty); constructor $a :: s$ for $a \in \Sigma$.
• Lists over $A$: base $\mathsf{nil}$; constructor $\mathsf{cons}(a, l)$.
• Binary trees: base $\mathsf{leaf}$; constructor $\mathsf{node}(l, r)$.
• Arithmetic expressions: base numerals and variables; constructors $+, \times, \ldots$.
• Propositional formulas: base atoms; constructors $\lnot, \land, \lor, \to$.

Why It Matters Here

Structural induction follows the constructors of finite inductive data. It is well suited to functions whose recursive calls follow immediate substructures. More general recursion and mutable or cyclic runtime objects require separate measures and representation assumptions.

More broadly, all of computer-science theory -- operational semantics, type systems, compilers, verification -- is written over recursively defined abstract syntax and reasoned about with structural induction. It is not a "nice to have"; it is the working lingua franca of the field.

Structural induction organizes obligations by constructor. Numerical induction on a suitable size measure is also sound; either method must cover every case and justify its hypothesis.

Concrete Example

Strings and concatenation. Define strings over a fixed alphabet $\Sigma$:

• Base: $\varepsilon$ (the empty string) is a string.
• Constructor: if $a \in \Sigma$ and $s$ is a string, then $a :: s$ is a string.

Define length and concatenation by structural recursion:

$$|\varepsilon| = 0, \qquad |a :: s| = 1 + |s|.$$

$$\varepsilon \mathbin{\text{++}} t = t, \qquad (a :: s) \mathbin{\text{++}} t = a :: (s \mathbin{\text{++}} t).$$

Theorem. For all strings $s, t$, $|s \mathbin{\text{++}} t| = |s| + |t|$.

Proof (by structural induction on $s$).

Base ($s = \varepsilon$). $|\varepsilon \mathbin{\text{++}} t| = |t| = 0 + |t| = |\varepsilon| + |t|$.

Step ($s = a :: s'$). Assume the structural IH: $|s' \mathbin{\text{++}} t| = |s'| + |t|$. Then $$|(a :: s') \mathbin{\text{++}} t| = |a :: (s' \mathbin{\text{++}} t)| = 1 + |s' \mathbin{\text{++}} t| \stackrel{IH}= 1 + |s'| + |t| = |a :: s'| + |t|.$$

By structural induction, the theorem holds for all strings $s$. $\blacksquare$

Every step used only the recursive definition of the function and the IH on the one immediate substructure of $s$. That is the template.

Binary trees and nodes. Define:

• Base: $\mathsf{leaf}$ is a tree; $\mathrm{nodes}(\mathsf{leaf}) = 0$; $\mathrm{leaves}(\mathsf{leaf}) = 1$.
• Constructor: $\mathsf{node}(l, r)$ is a tree with $\mathrm{nodes}(\mathsf{node}(l,r)) = 1 + \mathrm{nodes}(l) + \mathrm{nodes}(r)$ and $\mathrm{leaves}(\mathsf{node}(l,r)) = \mathrm{leaves}(l) + \mathrm{leaves}(r)$.

Counting convention for this example: nodes counts internal nodes only; the lab calls this I and uses N for all nodes.

Theorem. For every tree $t$, $\mathrm{leaves}(t) = \mathrm{nodes}(t) + 1$.

Base: $\mathrm{leaves}(\mathsf{leaf}) = 1 = 0 + 1 = \mathrm{nodes}(\mathsf{leaf}) + 1$. Step: assume IH for $l$ and $r$. Then $\mathrm{leaves}(\mathsf{node}(l,r)) = \mathrm{leaves}(l) + \mathrm{leaves}(r) \stackrel{IH}= (\mathrm{nodes}(l)+1) + (\mathrm{nodes}(r)+1) = \mathrm{nodes}(l) + \mathrm{nodes}(r) + 2 = \mathrm{nodes}(\mathsf{node}(l,r)) + 1$. $\blacksquare$

Common Confusion / Misconception

1. "Just induct on the length / size." For many proofs this works, but it is indirect: you translate structure into a numerical measure, prove a measure-indexed fact, then translate back. Structural induction skips the translation. Finite syntax, including finite lambda terms up to renaming bound variables, still admits size measures; structural induction is often the clearer presentation.
2. Missing constructor cases. Every constructor must produce a proof obligation. A classic mistake in propositional-formula proofs is treating $\land$ and $\lor$ but forgetting $\to$ or $\lnot$. The exclusion clause of the definition tells you which constructors exist; the proof must cover all of them.
3. Wrong IH scope. The structural IH applies to the immediate substructures that the constructor consumes, not to arbitrary smaller objects. For $\mathsf{node}(l, r)$ the IH gives you $P(l)$ and $P(r)$ -- nothing about grandchildren except via $P(l)$ and $P(r)$'s consequences.
4. Recursive definitions need justification. For a free finite grammar, total constructor clauses using child results define a unique function. For ambiguous or quotient representations, additionally establish agreement between representations.
5. Induction and recursion are different obligations. Induction on finite derivations does not require each element to have a unique derivation. A recursively proposed function on represented elements must give the same result through every applicable derivation.

How To Use It

Structural induction checklist:

1. Write the recursive definition of the set explicitly. Base cases. Constructors. Exclusion clause.
2. Identify the generation rules and their finite derivations. For a function on represented elements, separately check representative independence.
3. State $P(x)$ as a property of elements of $S$.
4. Prove $P$ for each base case.
5. For each constructor $f$: assume the structural IH on each argument that lies in $S$, then prove $P(f(\ldots))$.
6. Conclude "by structural induction, $\forall x \in S,\ P(x)$."

Definition-by-recursion checklist:

1. Define the function on each base element.
2. For each constructor, define the function in terms of the function on the arguments.
3. Verify the definition type-checks (every branch of every constructor is covered).
4. If defining on a non-free set, prove well-definedness -- independent of derivation.

Check Yourself

1. Why is ordinary induction on $\mathbb{N}$ a special case of structural induction? Identify the base and constructor.
2. Given a recursive definition with three constructors, how many proof obligations does a structural-induction proof have?
3. What is the structural IH for a constructor $\mathsf{node}(l, r)$ over binary trees?
4. Why might a property be provable by structural induction but awkward to prove by numerical induction on tree height?
5. What extra obligation do you have when proving a property of a non-freely-generated recursive set (e.g., rationals as fractions)?

Mini Drill or Application

1. Define $\mathrm{reverse}$ on lists recursively: $\mathrm{reverse}(\mathsf{nil}) = \mathsf{nil}$; $\mathrm{reverse}(\mathsf{cons}(a, l)) = \mathrm{reverse}(l) \mathbin{\text{++}} \mathsf{cons}(a, \mathsf{nil})$. Prove by structural induction that $\mathrm{reverse}(\mathrm{reverse}(l)) = l$. You will need a helper lemma about $\mathrm{reverse}(l_1 \mathbin{\text{++}} l_2)$.
2. Define propositional formulas recursively with atoms $p, q, \ldots$ and constructors $\lnot, \land, \lor$. Prove by structural induction that every formula has an equal number of opening and closing parentheses (under the standard parenthesised notation).
3. Define the height and the number of internal nodes of a binary tree. Prove $n \le 2^{h+1} - 1$ by structural induction on trees.
4. Sketch why a language designer's "match exhaustiveness" checker is essentially enforcing the structural-induction obligation at the type level.

Write out all constructor cases explicitly even when they look trivial.

Transfer to the module project

Use this concept to state, justify or challenge one claim in the workflow project. Name the mathematical model and the execution assumptions separately; software behavior is not established by an analogy alone.

Read This Only If Stuck

Use the bounded reading guide to locate this lesson's topic in MCS or Rosen. These links open book indexes. Find the named topic in your edition, read one relevant explanation, then reconstruct the argument with the book closed.

Closing Note

A matching recursive program and proof can share constructor cases, but a compiler's exhaustiveness check does not prove the desired property or termination. State and discharge the mathematical obligations explicitly.

Induction on derivations versus well-defined recursion

Properties of an inductively generated set can be proved by showing every generation rule preserves the property. Unique derivations are not required: one can induct on finite derivations of its elements. Defining a function by recursion on a non-unique representation is a separate issue; different derivations must agree on the output.

For the free tagged tree grammar, immediate children are unambiguous, so constructor recursion is straightforward. If tuple objects are shared between positions, the structural tree still counts each occurrence. An implementation counting unique object identities computes a different quantity. Finite syntax also has ordinary numerical size measures; structural induction is convenient, not the only sound method.

Transfer attempt: prove L=I+1 using internal-node count I and total count N=I+L. Add a unary constructor and rederive the identities in P16. For the distinction between generation rules and recursive definitions, see Cornell's induction and recursion notes.

Use Practice Solutions and Feedback after your attempt, and Proof and Model Contracts to audit assumptions.