Structural Induction Explained

August 31, 2024

Mathematical induction is a fundamental concept in computer science and mathematics, often used to prove properties of structures such as natural numbers and binary trees. This article provides an introduction to induction, focusing on how it applies to natural numbers and binary trees, and demonstrates the process through examples. Unfortunately, most other sources that explain structural induction don’t do a clear enough job explaining why induction works for an inductive set. This blog post outlines the process and relates it to induction over \(\mathbb{N}\).

A Recap of Induction over \(\mathbb{N}\) #

Induction over \(\mathbb{N}\) (often called just induction) is a method for proving propoerties of the natural numbers \(\mathbb{N} = \{0, 1, 2, \ldots\}\) to prove some property \(H(n)\), called the hypothesis for all \(n \in \mathbb{N}\).

It works by allowing you to prove just two cases:

1. base case: \(H(0)\) holds.
2. inductive case: If we know that \(H(n)\) holds for some \(n \in \mathbb{N}\), then \(H(n+1)\) also holds.

The reason why this works is that every natural number can be written in the form

\[ 0+1+1+\cdots+1 \]

for example,

\[ 3 = 0+1+1+1 \]

for a finite¹ number of \(1\)’s, that could be thought of as a tally. Since it is finite, you can always find a smaller number of any non-zero natural by removing one of the \(1\)’s, from the tally representation. This means that every natural is either,

1. Equal to \(0\), or
2. Equal to \(n + 1\) for some smaller natural \(n\).

So knowing that the base case holds tells us that \(H(0)\) holds, and knowing that the inductive case holds and inductive case hold tells us that for any natural \(0+1+\cdots+1\),

\[ H(0) \implies H(0+1) \implies H(0+1+1) \implies \cdots \implies H(0+1+\cdots+1) \]

and therefore, that \(H(n)\) holds for all \(n \in \mathbb{N}\)

Trees and Inductive Sets #

\[ \def\sc#1{\dosc#1\csod} \def\dosc#1#2\csod{{\rm #1{\small #2}}} \]

Structural induction can only be done over a certain kind of set called an inductive set. These are sets that can be represented as different kinds of trees. We start out by defining an inductive set of binary trees \(\sc{BIN}\sc{TREE}\) with construction rules:

\[ \dfrac{}{\text{Leaf}\in\sc{BIN}\sc{TREE}} \]

\[ \dfrac{l\in\sc{BIN}\sc{TREE}\qquad r\in\sc{BIN}\sc{TREE}} {\text{Fork}(l,r)\in\sc{BIN}\sc{TREE}} \]

The statements above the horizontal line are the premises, and the statement below is called the conclusion. \(\sc{BIN}\sc{TREE}\) is the inductive set being defined here. \(\text{Leaf}\), and \(\text{Fork}\) are constructors, and \(l\), \(r\) are variables local to the construction rule.

The \(\text{Leaf}\) rule is analogous to the base case in induction over \(\mathbb{N}\). This is because it has no premises, so it essentially just says,

\[ \text{Leaf}\in\sc{BIN}\sc{TREE} \]

The \(\text{Fork}\) rule is analogous to the inductive case in induction over \(\mathbb{N}\). It says that if for any \(l,r\in\sc{BIN}\sc{TREE}\),

\[ \text{Fork}(l,r)\in\sc{BIN}\sc{TREE} \]

We define \(\sc{BIN}\sc{TREE}\) as the least set that satisfies the construction rules. Like with \(\mathbb{N}\), this ends up having the effect of ensuring that there must be a finite number of construction rules.

As an example, we can construct the tree \[\text{Fork}(\text{Leaf},\text{Fork}(\text{Leaf},\text{Leaf}))\]

by building it ‘upside down’:

\[ \dfrac{\dfrac{}{\text{Leaf}\in\sc{BIN}\sc{TREE}}\qquad\dfrac{\dfrac{}{\text{Leaf}\in\sc{BIN}\sc{TREE}}\qquad\dfrac{}{\text{Leaf}\in\sc{BIN}\sc{TREE}}} {\text{Fork}(\text{Leaf},\text{Leaf})\in\sc{BIN}\sc{TREE}}} {\text{Fork}(\text{Leaf},\text{Fork}(\text{Leaf},\text{Leaf}))\in\sc{BIN}\sc{TREE}} \]

which can be represented grapically as follows:

The Natural Numbers as ‘Unary Trees’ #

Now we’ve got an example to think about, I’d like to take a different view of natural numbers by constructing them as ‘Unary trees’, that is trees where each fork only has one child.

Define \(\sc{U}\sc{TREE}\) as follows:

\[ \dfrac{}{\text{Zero}\in\sc{U}\sc{TREE}} \]

\[ \dfrac{n\in\sc{U}\sc{TREE}} {\text{Succ}(n)\in\sc{U}\sc{TREE}} \]

The intuition here is that \(\text{Succ}\) represents the constructor that creates a new natural number by adding one to a previous natural. For example, we can write the number \(2\) as:

Then we can recursively map from \(\sc{U}\sc{TREE}\) to \(\mathbb{N}\):

\begin{align} &f : \sc{U}\sc{TREE} \rightarrow \mathbb{N} \\ & f(\text{Zero}) = 0 \\ &f(\text{Succ}(t)) = f(t) + 1 \end{align}

This is recursive because in the second case, we are using \(f(t)\) to define \(f(\text{Succ}(t))\). So each step relies on the f’s value for its subtrees.

It turns out that this map from unary trees and the natural numbers associates every natural number with a unique unary tree. ² Intuitively this is because a tally and a unary tree are more or less the same thing. Each starts off with a single value and extends it in a unique way ³.

Structural Induction on Biary Trees #

We will now take a look at an example of induction on binary trees, to demonstrate structural induction.

Consider the hypothesis \(H(t)\) which states that for any binary tree \(t\), the number of leaves is one more than the number of forks. In symbols:

\[ H(t) \iff (\#leaves(t) = \#forks(t) + 1) \]

We then extend this to apply to a set \(S \subset \sc{BIN}\sc{TREE}\) such that,

\[ \mathcal{H} = {t\in \sc{BIN}\sc{TREE}. H(t)} \]

The reason why we have to use this as our hypothesis, rather than just having \(H(t)\) for some t is that in the \(\text{Fork}\) case, we will be combining different trees and need to know that the hypothesis holds for both trees that we are combining. Essentially the process we’re going through is to show that the set \(\mathcal{H}\) satisfies the construction rules for \(\sc{BIN}\sc{TREE}\), and therefore must be equal to \(\sc{BIN}\sc{TREE}\) itself.

To make this more concrete we define \(\#leaves\) and \(\#forks\) inductively on trees.

\begin{align*} &\#leaves(\text{Leaf}) = 1 \\ &\#leaves(\text{Fork}(s, t)) = \#leaves(s) + \#leaves(t) \\ &\#forks(\text{Leaf}) = 0 \\ &\#forks(\text{Fork}(s, t)) = \#forks(s) + \#leaves(t) + 1 \\ \end{align*}

Let’s prove this step by step.

\(\text{Leaf}\) Case #

We already know that \(\#leaves(\text{Leaf}) = 1\) and \(\#forks(\text{Leaf}) = 0\), so clearly

\[ \#leaves(\text{Leaf}) = \#forks(\text{Leaf}) + 1 \]

Thus \(\text{Leaf} \in \mathcal{H}\).

We’ve now shown that H(\text{Leaf}) holds, so we know that at least \(\text{Leaf} \in \mathcal{H}\).

\(\text{Fork}\) Case #

Given \(s,t\in\mathcal{H}\), then we know that

\[ \#leaves(s) = \#forks(s) + 1 \]

\[ \#leaves(t) = \#forks(t) + 1 \]

We want to show that

\[ \#leaves(\text{Fork}(s,t)) = \#forks(\text{Fork}(s,t)) + 1 \]

\begin{align*} \#leaves(\text{Fork}(s,t))) &= \#leaves(s) + \#leaves(t) &\text{(by definition of }\#leaves\text{)} && \\ &= \#forks(s) + 1 + \#forks(t) + 1 &\text{(by IH)} && \\ &= \#forks(\text{Fork}(s,t)) + 1 &\text{(by definition of }\#forks\text{)} && \end{align*}

Hence \(H(\text{Fork}(s,t))\) holds so \(\text{Fork}(s,t)\in\mathcal{H}\).

This completes the \(\text{Fork}\) case proving that \(\mathcal{H} = \sc{BIN}\sc{TREE}\). Hence we can conclude that \(\#leaves(t) = \#forks(t) + 1\) for all \(t \in \sc{BIN}\sc{TREE}\).

Summary #

Structural induction is a powerful tool for proving properties of recursively defined structures like natural numbers and binary trees. By proving that the set of elements satisfying a hypothesis also must satsify every construction rule, we can conclude that this set must be equal to the whole inductive set.

This method is not only foundational in mathematics but also crucial in computer science for reasoning about algorithms and data structures