CSC 208-01 (Spring 2023)

Reading: Inductive Reasoning

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.,

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:

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:

  1. head([1, 2, 3])
  2. tail([1 2 3])
  3. head(tail(tail([1 2 3])))
  4. 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:

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:

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:

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:


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:

list_intersperse(0, [1, 2, 3, 4, 5])
> [1, 0, 2, 0, 3, 0, 4, 0, 5]
list_intersperse(0, [])
> []
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(l1) + list_length(l2)
--> [[ 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:
               return cons(head(l1), list_append(tail(l1), l2))
         ]])
    -->* 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(l1) + list_length(l2)
     (+ (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(l1)) + list_length(tail(l2)) ≡ list_length(list_append(tail(l1), l2))

    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 analysis over a recursively-defined structure with the additional benefit of an induction hypothesis to 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([]) + list_length(l2)
    -->* 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(l1) + list_length(l2)
    -->* 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.