Mathematical Induction

So far, we have applied induction exclusively to lists. However, are there other structures that are inductive? It turns out that the natural numbers are the most common structure to perform induction over in mathematics. Now that we have some experience with inductive proof, let’s explore this foundational application of the technique in detail.

The Natural Numbers

Recall that we can apply induction to any inductively-defined structure, that is, a structure defined in terms of a finite set of (potentially recursively-defined) cases. How can we define the natural numbers, i.e., non-negative integers, in this manner? One natural choice is to start at zero, the smallest natural number, and work our way up.

Since it is the smallest natural number, zero seems to serve as a base case, similar to the empty list. However, how can we characterize a non-zero natural number in terms of another natural number? Consider the number seven, written in unary, i.e., tally marks:

\[ \underbrace{1111111}_{7} \]

Do we see a smaller natural number nested somewhere inside of seven? The unary representation makes this explicit:

\[ 1\underbrace{111111}_{6}. \]

Seven can be thought of as six but with one extra mark! In general, any non-zero natural number \(k\) is one more than \(k - 1\). This fact leads to the following definition of the natural number as an inductive structure:

With lists, we use list functions list to query and break apart the structure:

• null? allows us to test if a list is empty.
• car lets us extract the head of an empty list.
• cdr lets us extract the tail of an empty list.
• cons lets us construct a list from a head and tail.

We do the same thing with natural numbers, albeit with functions that you have seen before but may not have thought of in this context:

• (=) and equal? allows us to test if a natural number is zero. zero? also allows us to test for zero directly.
• (-) allows us to retrieve the smaller natural number from a larger one.
• (+) allows us to build up larger natural numbers from smaller ones.

Induction Over the Natural Numbers

Now that we have an inductive definition of the natural numbers, we can:

1. Perform recursive operations over the natural numbers, and
2. Prove properties involving natural numbers by using inductive reasoning.

Of course, not having a formal inductive definition didn’t stop us from writing recursive functions over the natural numbers. Similarly, with lists, having this definition in-hand can give us more confidence that we are doing the right thing when we begin programming.

With that being said, let us focus on the second activity for the remainder of this section: writing inductive proofs with natural numbers. Induction over the natural numbers is so common that we give it a generic Consider the following canonical recursive function over the natural numbers:

(define factorial
  (lambda (n)
    (if (zero? n)
        1
        (* n (factorial (- n 1))))))

And the following claim about factorial asserts that factorial produces only positive, non-negative, non-zero results.

Claim: for any natural number n, (< 0 (factorial n)).

Note that the definition of factorial reflects the structure of the inductive definition of a natural number. This strongly suggests that we ought to prove this claim using induction. Let’s go ahead and try it, following the same style of proof introduced for lists, but instead invoking the inductive definition of natural numbers.

The case analysis of our inductive is similar to that of lists. The “base case” for a natural number is when that number is zero. The “inductive case” for a natural number is when that number is non-zero. Note that because a natural number cannot be negative and the inductive case number is not zero, this number must be a positive integer. If we call that natural number k, then we know that k-1 is well-defined (since k is at least 1).

The proof of the base case follows from evaluation:

The proof of the recursive case also follows from evaluation, invoking the induction hypothesis, and collecting assumed constraints about the different pieces of the inequality.

Note that in the inductive case, we acquire the following assumptions:

• n is non-zero because we are in the inductive case.
• (< 0 (factorial ( - n 1))) from our induction hypothesis.

These two facts combined with the knowledge that two multiplying two positive numbers produces a positive number tell us that the body of factorial produces a strictly positive result.

(define sum
  (lambda (n)
    (if (zero? n)
        0
        (+ n (sum (- n 1))))))