As you learned in CSC 151, the workhorse of functional programming is
*recursion*. Recursion allows us to perform repetitive behavior
by defining an operation in terms of a smaller version of itself.
However, recursion is not just something you learn in Racket and
summarily forget about for the rest of your career. Recursion is
pervasive everywhere in computer science, especially in algorithmic
design.

Because of this, we must know how to reason about recursive programs.
Our model of computation is robust enough to trace the execution of
recursive programs. However, our formal reasoning tools fall short in
letting us prove properties of these programs. We introduce
*induction* one of the foundational reasoning principles in
mathematics and computer science, to account for this disparity.

# Lists in Python

In Scheme/Racket, we typically perform recursion over lists. It is
*un-Pythonic*, *i.e.*, not idiomatic Python, to do this.
Instead, we favor other techniques, *e.g.*, list comprehensions
and for-loops. However, we’ll use list recursion now as a bridge between
our knowledge of Scheme and Python. Later in the course, we’ll
demonstrate how we can verify programs involving lists manipulated in
Pythonic ways.

For now, let’s review what lists are all about. Like numbers, there
are an infinite number of possible lists, *e.g.*,

`[]`

`[3, 5, 8]`

`['Hi', 'goodbye', '!']`

`[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]`

.

However, our *recursive* definition of a list categorizes
these infinite possibilities into a *finite* set of cases.

**Definition (List)**: A *list* is either:

- Empty, or
- Non-empty, consisting of a
*head*element and the remainder of the list, its*tail*.

This definition is similar to that of a boolean, where we define a
boolean as one of two possible values: `#t`

or
`#f`

. However, the definition of a list is recursive because
the non-empty case includes an element that is also a list.

## Queries Over Lists

From our recursive definition, we see we need to perform three
operations over lists. In Scheme, there exists
functions—`null?`

, `car`

, and `cdr`

—to
perform these operations directly. To achieve the same effect in Python,
we have to take advantage of a few different features of lists:

- To test if a list
`l`

is**empty**, we can simply test for equality against the empty list:`l == []`

. - To retrieve the
**head**of the list, we use list indexing:`l[0]`

. - To retrieve the
**tail**of the list, we use list slicing:`l[1:len(l)]`

. As short-hand, Python allows us to omit the end index of the slice if it is the end of the list. So the above expression is equivalent to the shorter`l[1:]`

.

List literal syntax in Python, *e.g.*,
`[1, 2, 3, 4, 5]`

, allows us to create a list from the
specified elements. Finally, to achieve the effect of `cons`

which constructs a new list given a head and tail, we combine list
literal syntax and list concatenation with `+`

:
`[head] + tail`

.

Rather than remembering these patterns, it is helpful to create helper functions that perform like the equivalent Scheme functions:

```
def is_null(l):
return l == []
def head(l):
return l[0]
def tail(l):
return l[1:]
def cons(x, xs):
return [x] + xs
```

Note that these are *not* library functions but functions that
we provide ourselves. We’ll use these helpers throughout the remainder
of our discussion.

**Exercise**: Predict the results of each of the
following expressions:

`head([1, 2, 3])`

`tail([1 2 3])`

`head(tail(tail([1 2 3])))`

`is_null(tail(tail(tail([1 2 3]))))`

## Recursive Design with Lists

Because lists are defined via a finite set of cases, we define
operations over lists using *case analysis* with the
`is_null`

predicate. For some simple operations, this is
enough to get by, *e.g.*, a function that retrieves the second
element of a list:

```
def second(l):
if is_null(l):
raise Exception('list is empty')
else if (is_null(tail(l))):
raise Exception('list only contains one element')
else:
return head(tail(l))
```

We can translate this code to a high-level description:

- If the list is empty, throw an error.
- If the list contains one element, throw an error.
- If the list has at least two elements, retrieve the second element.

However, mere case analysis doesn’t allow us to write more complex
behavior. Consider the prototypical example of a recursive function:
computing the length of a list. Let’s first consider a high-level
*recursive design* of the operation of this function. Because a
list is either empty or non-empty, this leads to straightforward case
analysis. The empty case is straightforward:

- If the list is empty, its length is
`0`

.

However, in the non-empty case, it isn’t immediately clear how we
should proceed. We can draw the non-empty case of a list `l`

with head element `v`

and tail `tl`

as
follows:

`l = [v][ ?? tl ?? ]`

Besides knowing that `tl`

is a list, we don’t know
anything about it—it is an *arbitrary list*. So how can we
compute the length of `l`

in this case? We proceed by
*decomposing* the length according to the parts of the lists we
can access:

```
length = 1 + length(t)
l = [h][ ?? t ?? ]
```

We know that the head element `h`

contributes
`1`

to the overall length of `l`

. How much does
the tail of the list `t`

contribute? Since `t`

is,
itself, a list, `t`

contributes whatever
`length(t)`

produces. But this is a call to the same function
that we are defining, albeit with a smaller list than the original
input!

Critically, as long as the call to `length(t)`

works, the
overall design of `length`

is correct. This assumption that
we make—that the recursive call “just works” as long as it is passed a
“smaller” input—is called the *recursive assumption*, and it is
the distinguishing feature of recursion compared to simple case
analysis.

In summary, we define `length`

recursively as follows:

The length of a list

`l`

is:

`0`

if`l`

is empty.`1`

plus the length of the tail of`l`

if`l`

is non-empty.

In the recursive case of the definition, our recursive assumption
allows us to conclude that the “length of the tail of `l`

” is
well-defined.

Finally, our high-level recursive design of `length`

admits a direct translation into Python using our list functions:

```
def list_length(l):
if is_null(l):
return 0
else:
return 1 + list_length(tail(l))
```

Because the translation is immediate from the high-level recursive design, we can be confident our function is correct provided that the design is correct.

## A Recursive Skeleton for Lists

Ultimately, the recursive design of a function contains two parts:

- Case analysis over a recursively-defined structure.
- A recursive assumption allowing us to use the function recursively on a smaller object than the input.

When we fix the structure, *e.g.*, lists, we arrive at a
*skeleton* or template for defining recursive functions that
operate on that structure. This skeleton serves as a starting point for
our recursive designs. The skeleton always mimics the recursive
definition of the structure:

For an input list `l`

:

- What do we do when
`l`

is empty (the*base case*)? - What do we do when
`l`

is non-empty (the*recursive case*)? When`l`

is non-empty, we have access to the head of`l`

and the tail of`l`

with pattern matching. Furthermore, when`l`

is non-empty, we can use our recursive assumption to recursively call our function on the tail of`l`

.

Note that this skeleton is only a starting point in our recursive
design. We may need to generalize or expand the skeleton, *e.g.*,
by adding additional base cases depending on the problem.

**Exercise (Intersperse)**: write a high-level recursive
design for the `list_intersperse`

function.
`list_intersperse(v, l)`

returns `l`

but with
`v`

placed between every element of `l`

. For
example:

```
0, [1, 2, 3, 4, 5])
list_intersperse(> [1, 0, 2, 0, 3, 0, 4, 0, 5]
0, [])
list_intersperse(> []
list-intersperse(0, [1])
> [1]
```

(*Hint*: this is an example of a function where its most
elegant implementation comes from having *multiple base cases*.
Consider an additional base case in your recursive design.)

# Reasoning About Recursive Functions

Now, we’ll develop our primary technique for reasoning about
recursive structures, *structural induction*. Let’s come back to
the proposition about `append`

that we used to start our
discussion of program correctness:

**Claim**: for all lists `l1`

and
`l2`

, `list_length(l1) + list_length(l2)`

≡
`list_length(list_append(l1, l2))`

.

To prove this claim, we need the definitions of both
`list_length`

and `list_append`

.

**Exercise (Append)**: Try to design and implement
`list_append(l1, l2)`

, which returns the result of appending
`l1`

onto the front of `l2`

without peeking
below!

```
def list_length(l):
if is_null(l):
return 0
else:
return 1 + list_length(tail(l))
def list_append(l1, l2):
if is_null(l1):
return l2
else:
return cons(head(l1), list_append(tail(l1), l2))
```

The proof proceeds similarly to all of our symbolic proofs so far: assume arbitrary values for the universally quantified variables and attempt to use symbolic evaluation.

*Proof*. Let `l1`

and `l2`

be arbitrary
lists. The left-hand side of the equivalence evaluates to:

```
+ list_length(l2)
list_length(l1) --> [[ if is_null(l1):
return 0
else:
return 1 + list_length(tail(l1)) ]] + list_length(l2)
```

The right-hand side of the equivalence evaluates to:

```
list_length(list_append(l1, l2))--> list_length([[
if is_null(l1):
return l2
else:
return cons(head(l1), list_append(tail(l1), l2))
]])
```

At this point, both sides of the equivalence are stuck. However, we
know that because `l1`

is a list, it is either empty or
non-empty. Therefore, we can proceed with a case analysis of this
fact!

Either `l1`

is empty or non-empty.

`l1`

is empty,*i.e.*,`l1`

is`[]`

. The left-hand side of the equivalence evaluates as follows:`...--> [[ if is_null([]): return 0 else: return 1 + list_length(tail([])) ]] + list_length(l2) -->* 0 + list_length(l2) --> list_length(l2)`

On the right-hand side of the equivalence, we have:

`... [[ --> list_length(if is_null([]): return l2 else:cons(head(l1), list_append(tail(l1), l2)) return ]]) -->* list_length(l2)`

Both sides evaluate to

`list_length(l2)`

, so they are equivalent!

So the empty case works out just fine. What about the non-empty case?

`l1`

is non-empty. On the left-side of the equivalence, we have:`...--> [[ if is_null(l1): return 0 else: return 1 + list_length(tail(l1)) ]] + list_length(l2) -->* 1 + list_length(tail(l1)) + list_length(l2)`

On the right-hand side of the equivalence, we have:

`...--> list_length([[ if is_null(l1): return l2 else: return cons(head(l1), list_append(tail(l1), l2)) ]])-->* list_length(cons(head(l1), list_append(tail(l1), l2))) --> 1 + list_length(list_append(tail(l1), l2))`

Note that this evaluation is a bit trickier than the previous ones
that we have seen. In particular, we have to observe that in the final
step that the outer call to `list_length`

can partially
evaluate because `is_null(cons(x, xs))`

returns
`False`

, *i.e.*, a `cons`

is, by
definition, a non-empty list! Nevertheless, if we push through
accurately, we can persevere!

At this point, our equivalence in the non-empty case is:

`1 + list_length(tail(l1)) + list_length(l2) ≡ 1 + list_length(list_append(tail(l1), l2))`

`l1`

is still abstract, so we can’t proceed further. One
way to proceed is to note that `tail(l1)`

itself is a list.
Therefore, we can perform case analysis on it—is `tail(l1)`

empty or non-empty?

(Still in the case where `l1`

is non-empty.)

`tail(l1)`

is either empty or non-empty.

`tail`

is empty. The left-hand side of the equivalence evaluates to:`...--> 1 + list_length(tail(l1)) + list_length(l2) -->* 1 + 0 + list_length(l2) --> 1 + list_length(l2)`

The right-hand side of the equivalence evaluates to:

`...--> 1 + list_length(list_append(tail(l1), l2)) -->* 1 + list_length(l2)`

Both sides of the equivalence are

`1 + list_length(l2)`

, completing this case.

Note that when `tail(l1)`

is empty, the original list
`l1`

only contained a single element. Therefore, it should
not be surprising that the equivalence boils down to demonstrating that
both sides evaluates to `1 + list_length (l2)`

.

Again, while the empty case works out, the non-empty case runs into problems.

(Still in the case where `l1`

is non-empty.)

`tail(l1)`

is non-empty. The left-hand side of the equivalence evaluates to:`...--> 1 + list_length(tail(l1)) + list_length(l2) --> 1 + [[ if is_null(tail(l1)): return 0 else: return 1 + list_length(tail(tail(l1))) + list_length(l2) ]] --> 1 + [[ if False: return 0 else: return 1 + list_length(tail(tail(l1))) + list_length(l2) ]] -->* 1 + 1 + list_length(tail(tail(l1))) + list_length(l2)`

Notice a pattern yet? Here is where our case analyses have taken the left-hand side of the equivalence so far:

```
+ list_length(l2)
list_length(l1) + (length l1) (length l2))
(-->* <... l1 is non-empty ...>
-->* 1 + list_length(tail(l1)) + list_length(l2)
-->* <... tail(l1) is non-empty ...>
-->* 1 + 1 + list_length(tail(tail(l1))) + list_length(l2)
```

We could now proceed with case analysis on
`tail(tail(l1))`

. We’ll find that the base/empty case is
provable because there we assume that `l1`

has exactly two
elements. But then, we’ll end up in the same situation we are in, but
with one additional `1 + ...`

at the front of expression!
Because the inductive structure is defined in terms of itself and we are
proving this property over *all* possible lists, we don’t know
when to stop our case analysis!

**Exercise (The Other Side)**: we demonstrated that case
analysis and evaluation of the equivalence’s left-hand side seemingly
has no end. Perform a similar analysis of the equivalence’s right-hand
side, starting when `tail(l1)`

is non-empty. You should
arrive at the point where the right-hand side evaluates to:

`1 + 1 + list_length(list_append(tail(tail(l1)), l2))`

# Inductive Reasoning

How do we break this seemingly infinite chain of reasoning? We employ
an *inductive assumption* similar to the recursive assumption we
use to design recursive functions. The recursive assumption is that our
function “just works” for the tail of the list. Our inductive assumption
states that our original claim holds for the tail of the list!

Recall that our original claim stated:

**Claim**: for all lists `l1`

and
`l2`

,
`list_length(l1) + list_length(l2) ≡ list_length(list_append(l1, l2))`

.

Our *inductive assumption* is precisely the original claim but
specialized to the tail of the list that we perform case analysis over.
We also call this inductive assumption our *inductive
hypothesis*.

**Inductive hypothesis**:
`list_length(tail(l1)) + list_length(tail(l2)) ≡ list_length(list_append(tail(l1), l2))`

While we are trying to prove the claim, the inductive hypothesis is
an *assumption* we can use in our proof.

Let’s unwind our proof back to the case analysis of `l1`

.
The case where `l1`

was empty was provable without this
inductive hypothesis, so let’s focus on the non-empty case. Recall that
before we performed case analysis, we arrived at a proof state where our
goal equivalence to prove was:

`1 + list_length(tail(l1)) + list_length(l2) ≡ 1 + list_length(list_append(tail(l1), l2))`

Compare this goal equivalence with our induction hypothesis above. We
see that the left-hand side of the induction hypothesis equivalence,
`list_length(tail(l1)) + list_length(l2)`

, is contained in
the left-hand side of the goal equivalence. Because our induction
hypothesis states that this expression is equivalent to
`list_length(list_append(tail(l1), l2))`

, we can
*rewrite* the former expression to the latter expression in our
goal! This fact allows us to finish the proof as follows:

`l1`

is non-empty. Our induction hypothesis states that:`+ list_length(tail(l2)) ≡ list_length(list_append(tail(l1), l2)) list_length(tail(l1))`

Since

`l1`

is non-empty, evaluation simplifies the goal equivalence to:`1 + list_length(tail(l1)) + list_length(l2) ≡ 1 + list_length(list_append(tail(l1), l2))`

By our induction hypothesis, we can rewrite this goal to:

`1 + list_length(list_append(tail(l1), l2)) ≡ 1 + list_length(list_append(tail(l1), l2))`

Which completes the proof.

We call a proof that uses an induction hypothesis a *proof by
induction* or *inductive proof*. Like recursion in
programming, inductive proofs are pervasive in mathematics.

In summary, here is a complete inductive proof of the
`append`

claim. In this proof, we’ll step directly from a
call to `list_length`

or `list_append`

directly to
the branch of the `if`

that we would have selected. We’ll
take this evaluation shortcut moving forward to avoid cluttering our
proof.

Note in our proof that we declare that we “proceed by induction on
`l1`

” and then move into a case analysis. This exemplifies
how we should think of inductive proof moving forward:

An inductive proof is a

case analysisover arecursively-defined structurewith the additional benefit of aninduction hypothesisto avoid infinite reasoning.

**Claim**: for all lists `l1`

and
`l2`

, `list_length(l1) + list_length(l2)`

≡
`list_length(list_append(l1, l2))`

.

*Proof*. We proceed by induction on `l1`

.

`l1`

is empty, thus`l1`

is`[]`

. The left-hand side of the equivalence evaluates as follows:`+ list_length(l2) list_length([]) -->* 0 + list_length(l2) --> list_length(l2)`

On the right-hand side of the equivalence, we have:

`list_length(list_append([], l2))-->* list_length(l2)`

`l1`

is non-empty. Our induction hypothesis is:**Inductive hypothesis**:`list_length(tail(l1)) + list_length(tail(l2)) ≡ list_length(list_append(tail(l1), l2))`

On the left-hand side of the equivalence, we have:

`+ list_length(l2) list_length(l1) -->* 1 + list_length(tail(l1)) + list_length(l2)`

On the right-hand side of the equivalence, we have:

`list_length(list_append(l1, l2))-->* list_length(cons(head(l1), list_append(tail(l1), l2))) -->* 1 + list_length(list_append(tail(l1), l2))`

In summary, we now have:

`1 + list_length(tail(l1)) + list_length(l2) ≡ 1 + list_length(list_append(tail(l1), l2))`

We can use our induction hypothesis to rewrite the left-hand side of the equivalence to the right-hand side:

`1 + list_length(list_append(tail(l1), l2)) ≡ 1 + list_length(list_append(tail(l1), l2))`

Completing the proof.

**Exercise (Switcharoo, ‡)**: in our proof of the
correctness of `append`

, we performed induction on
`l1`

. Could we have instead performed induction on
`l2`

? Try it out! And based on your findings, explain why or
why not in a few sentences.