# On induction and recursive functions, with an application to binary search

To make sense of recursive functions, you can use a way of thinking closely related to mathematical induction.

- Mathematical induction
- Sum of an arithmetic series (basic example)
- The same sum in code
- Binary search correctness proof

## Mathematical induction

Mathematical induction is a proof method often used to prove statements about integers.

We’ll use the notation P(*n*), where *n* ≥ 0,
to denote such a statement.
To prove P(*n*) with induction is a two-step procedure.

**Base case:**Show that P(0) is true.**Inductive step:**Show that P(*k*) is true**if**P(*i*) is true for all*i*<*k*.

The statement ”P(*i*) is true for all *i* < *k*”
is often called the **induction hypothesis**.

If we manage to prove both of these statements,
we can in fact be sure that P(*n*) is true for all *n* ≥ 0.

- The base case shows that P(0) is true.
- To see that P(1) holds, we use both steps in the proof.
The base case shows that P(0) holds. The inductive step says,
among other things, that P(1) is true
**if**P(0) is true. These two facts taken together imply that P(1) must be true. - Now we can repeat this argument to show P(2).
Since we already know that P(0) and P(1) are true,
we can use the inductive step to prove P(2).
In fact, when
*k*= 2 the inductive step says that ”P(2) is true if P(*i*) is true for all*i*< 2”. - Using the same argument we can show P(3), P(4), P(5), and so on.

## Sum of an arithmetic series

Let’s start with a statement P(*n*) from mathematics.

1 + 2 + 3 + ... +n=n(n+ 1)/2

We’ll use induction to prove P(*n*)
for all *n* ≥ 1.
(If we define the empty sum to be zero, P(0) is true as well.)

### Proof

#### Base case

Since we want to prove the statement for all integers *n* ≥ 1,
we’ll start the induction at 1 instead of 0.
When *n* = 1, the left-hand side is 1 and
the right-hand side is 1(1 + 1)/2 = 1.
Hence, P(1) is true.

#### Inductive step

We need to show that P(*k*) is true
**if** P(*i*) is true for all *i* < *k*.
Our induction hypothesis is

1 + 2 + ... +i=i(i+ 1)/2 for alli<k,

and we must prove that

1 + 2 + ... +k=k(k+ 1)/2.

The computation looks like this.

1 + 2 + ... +k= (1 + 2 + ... + (k- 1)) +k= [*] = ((k- 1)(k- 1 + 1)/2) +k= (k- 1)k/2 + 2k/2 = (k^{2}+ k)/2 =k(k+ 1)/2

* This is where we use the induction hypothesis.

Now that we’ve shown both the base case and the induction step,
we can deduce that P(*n*) must be true for all positive integers *n*.
**Q.E.D.**

## The same sum in code

Induction works beautifully for proving statements about recursive functions, and for thinking about recursion in general.

```
// Sum returns the sum 1 + 2 + ... + n, where n >= 1.
func Sum(n int) int {
if n == 1 {
return 1
}
return n + Sum(n-1)
}
```

The statement P(*n*) to prove can be stated:

The function call`Sum(n)`

returns the value 1 + 2 + ... +n.

### Proof

#### Base case

P(1) is true since the function returns 1 when *n* = 1.

#### Induction step

We make the hypothesis “P(*i*) is true for all *i* < *k*”,
i.e. the call `sum(i)`

returns
1 + 2 + … + *i*
when *i* < *k*.
Using this hypothesis, we need to prove P(*k*).

If *k* ≥ 2, the call `sum(k)`

returns `k + sum(k-1)`

.
But we know, according to the induction hypothesis,
that the call `sum(k-1)`

returns
1 + 2 + … + (*k*-1).
Ergo, `sum(k)`

will return

k+ (1 + 2 + ... + (k-1)) = 1 + 2 + ... +k.

Using induction, we can conclude that the call `sum(n)`

returns the value
1 + 2 + … + *n*
whenever *n* ≥ 1.
**Q.E.D.**

## Binary search correctness proof

Binary search is known as ”the simplest algorithm than no one can implement”. This seems to be true: the top ten search results when I looked for binary search implementations exposed some dubious pieces of code. We’d better use both test code and a correctness proof.

```
// Find returns the smallest index i at which x <= a[i].
// If there is no such index, it returns len(a).
// The slice must be sorted in ascending order.
func Find(a []int, x int) int {
switch len(a) {
case 0:
return 0
case 1:
if x <= a[0] {
return 0
}
return 1
}
mid := 1 + (len(a)-1)/2
if x <= a[mid-1] {
return Find(a[:mid], x)
}
return mid + Find(a[mid:], x)
}
```

The statement P(*n*) to prove:

For a sorted slice`a`

of lengthn, the function call`Find(a, x)`

will return the smallest index`i`

at which`x`

≤`a[i]`

. If there is no such index, it returnsn.

### Proof

#### Base case

If the slice has length at most `1`

,
the correct answer is returned by the switch statement.

#### Induction step

The induction hypothesis states that P(*i*) is true for all
*i* < *k*, i.e. the method returns the correct
answer if the slice has fewer than *k* element.

Our job is to prove P(*k*).
We have already checked P(0) and P(1), so we can assume that *k*
is at least 2.
In that case the program will execute the statement

`mid := 1 + (len(a)-1)/2`

A careful study of this statement leads us to the conclusion that
1 ≤ mid < *k*.

There are two cases. If `x ≤ a[mid-1]`

,
the index we’re looking for must be in the slice `a[:mid]`

.
Since the number of elements in this slice is less than `k`

and at least one, the induction hypothesis states that
`Find(a[:mid], x)`

will return the correct answer.

In the other case, `x > a[mid-1]`

and
the index we’re looking for must be in the slice `a[mid:]`

.
Since the number of elements in this slice is less than `k`

and at least one, the induction hypothesis states that
`mid + Find(a[mid:], x)`

will return the correct answer.

Using induction, we can conclude that the function `Find`

is correct with respect to its specification when
0 ≤ *n* ≤ *M*, where
*M* is the maximum value of an `int`

.
Since the length of an array can always be represented
by an `int`

in Go,
we have proved this code to be correct. **Q.E.D.**

### Test code

Beware of bugs in the above code; I have only proved it correct, not tried it.

*Donald Knuth*

The Table driven unit tests article has test code for this function.

## Further reading

See Loop invariants can give you coding superpowers for a simple yet powerful tool to help understand iterative code.