CSC/MAT 208 (Spring 2024)

Reading: Inductive Reasoning

Review of Recursive Design

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.

A Review of Lists

In Racket, we typically perform recursion over lists. 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.

List Functions

The primary functions over lists map cleanly onto our recursive definition:

We can create a list using the (list ...) function, which creates a list from the specified elements. We can also use quotation syntax, e.g., '(1 2 3), to create a list. Finally, we can use (cons v l) that constructs a list from head element v and tail list l.

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

  1. (car '(1 2 3))
  2. (cdr '(1 2 3))
  3. (car (cdr (cdr '(1 2 3))))
  4. (null? (cdr (cdr (cdr '(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 pattern matching or the null? predicate. For some simple operations, this is enough to get by, e.g., a function that retrieves the second element of a list:

;;; (second l) -> T?
;;; l : listof T?
;;; Returns the second element of `l`. Raises an error if
;;; no such element exists.
(define second
  (lambda (l)
    (cond [(null? l)       (error "List is empty.")]
          [(null? (cdr l)) (error "List only contains one element.")]
          [else            (car (cdr 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 Racket using our list functions:

(define length
  (lambda (l)
    (if (null? l)
        0
        (+ 1 (length (cdr 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.

Pattern Matching with Lists

Recall that one of our design goals is to write programs that are correct from inspection. In particular, when we have a recursive design, we want our code to look like that design. Let’s see how our recursive definition of length fares in this respect. Below, we have replicated the definition of length with the recursive design in-lined in comments:

(define length
  (lambda (lst)
    (if (null? lst)                   ; A list is either empty or non-empty.
        0                             ; + The empty list has zero length.
        (let ([head (car lst)]        ; + A non-empty list has a head and tail
              [tail (cdr lst)])       ; element.
             (+ 1 (length tail))))))  ;   The length of a non-empty list is one
                                      ;   plus the length of the tail.

In this version of the code, we explicitly bind the head and tail of l to be clear where these components of l are manipulated.

Overall, this isn’t too bad! Like our design, the code is clearly conditioned on whether lst is empty or non-empty. Furthermore, the results of the cases clearly implement the cases of our design, so we can believe our implementation is correct as long as we believe our design is correct.

Is there anything we can improve here? Yes—some subtle, yet important things, in fact:

To fix these issues, we’ll use the pattern matching facilities of Racket to express our recursive design directly without the need for a guard expression or let-binding. Note that when we talk about pattern matching here, we don’t mean regular expression matching but instead a separate library of Racket for writing code that looks at the shape of a data type.

First, we’ll revise our list definition slightly based on the functions we use to construct lists.

A list is either: + '(), the empty list (null is a more readable alternative to '()). + (cons v l), a non-empty list constructed with cons that consists of a head element v and a list l.

Remember that a list is ultimately composed of repeated cons calls ending in '(). For example:

> (list 1 2 3 4 5)
'(1 2 3 4 5)
> (cons 1 (cons 2 (cons 3 (cons 4 (cons 5 '())))))
'(1 2 3 4 5)

Because of this, we know that our constructive definition of a list covers all possible lists. Now, we’ll use pattern matching to directly express length in terms of this constructive definition:

(require racket/match)

(define length
  (lambda (l)
    (match l
      ['() 0]
      [(cons head tail) (+ 1 (length tail))])))

This version of length behaves identically to the previous version of the code but is more concise, directly reflecting our constructive definition of a list. By doing so, we no longer need a let-expression to bind names to the components of the non-empty list—the match construct of Racket does this for us automatically!

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

Inductive Reasoning

In the previous reading, we reviewed recursive design. Now, we’ll develop our primary technique for reasoning about recursive structures, structural induction.

Reasoning About Recursive Functions

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, (+ (length l1) (length l2))(length (append l1 l2)).

To prove this claim, we need the definitions of both length and append.

Exercise (Append): Try to design and implement (append l1 l2), which returns the result of appending l1 onto the front of l2 without peeking below!

(define length
  (lambda (l)
    (match l
      ['() 0]
      [(cons _ tail) (+ 1 (length tail))])))

(define append
  (lambda (l1 l2)
    (match l1
      ['() l2]
      [(cons head tail) (cons head (append tail 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:

    (+ (length l1) (length l2))
    (+ (match l1
         ['() 0]
         [(cons _ tail) (+ 1 (length tail))])
       (length l2))

The right-hand side of the equivalence evaluates to:

    (length (append l1 l2))
--> (length (match l1
              ['() l2]
              [(cons head tail) (cons head (append tail 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:

    ...
    --> (+ (match '()
            ['() 0]
            [(cons _ tail) (+ 1 (length tail))])
    --> (+ 0 (length l2))
    --> (length l2)

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

    ...
    --> (length (match '()
                  ['() l2]
                  [(cons head tail) (cons head (append tail l2))]))
    --> (length l2)

    Both sides evaluate to (length l2), so they are equivalent!

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

  • l1 is non-empty. Since l1 is non-empty, l1 is (cons head tail) for some value head and list tail, so on the left-hand side of the equivalence, we have:

    ...
    --> (+ (match l1
            ['() 0]
            [(cons _ tail) (+ 1 (length tail))])
    --> (+ (+ 1 (length tail)) (length l2))
    --> (+ 1 (+ (length tail) (length l2)))

    The final step of evaluation comes from the commutative property of addition: \((1 + x) + y = 1 + (x + y)\).

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

    ...
    --> (length (match '()
                  ['() l2]
                  [(cons head tail) (cons head (append tail l2))]))
    --> (length (cons head (append tail l2))
    --> (match (cons head (append tail l2))
          ['() 0]
          [(cons _ ttail) (+ 1 (length ttail))])
    --> (+ 1 (length (append tail l2)))

Note that this evaluation is a bit trickier than the previous ones that we have seen. In particular, we have to observe that the tail of (cons x y) is simply y! Nevertheless, if we push through accurately, we can persevere!

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

(+ 1 (+ (length tail) (length l2))) ≡ (+ 1 (length (append tail l2)))

tail is still abstract, so we can’t proceed further. One way to proceed is to note that tail itself is a list. Therefore, we can perform case analysis on it—is tail empty or non-empty?

(Still in the case where l1 is non-empty.)

tail is either empty or non-empty.

  • tail is empty. The left-hand side of the equivalence evaluates to:

    ...
    --> (+ 1 (+ (length tail) (length l2)))
    --> (+ 1 (+ (match tail
                  ['() 0]
                  [(cons _ tail2) (+ 1 (length tail2))])
                (length l2)))
    --> (+ 1 (+ 0 (length l2)))
    --> (+ 1 (length l2))

    The right-hand side of the equivalence evaluates to:

    ...
    --> (+ 1 (length (append tail l2)))
    --> (+ 1 (length (match tail
                       ['() l2]
                       [(cons head2 tail2) (cons head2 (append tail2 l2))])))
    
    --> (+ 1 (length l2))

    Both sides of the equivalence are (+ 1 (length l2)), completing this case.

Note that when tail 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 (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 is non-empty. The left-hand side of the equivalence evaluates to:

    ...
    --> (+ 1 (+ (length tail) (length l2)))
    --> (+ 1 (+ (match tail
                  ['() 0]
                  [(cons head2 tail2) (+ 1 (length tail2))])
                (length l2)))
    --> (+ 1 (+ (+ 1 (length tail2)) (length l2)))
    --> (+ 1 (+ 1 (+ (length tail2) (length l2))))

tail2 here is the tail of tail, i.e., (cdr (cdr l1)) or (cddr l1)!

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

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

We could now proceed with case analysis on tail2. 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 is non-empty. You should arrive at the point where the right-hand side evaluates to:

(+ 1 (+ 1 (length (append tail2 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, (+ (length l1) (length l2)) ≡ (length (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: (+ (length (cdr l1)) (length l2)) ≡ (length (append (cdr 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 (+ (length tail) (length l2))) ≡ (+ 1 (length (append tail l2)))

Compare this goal equivalence with our induction hypothesis above. We see that the left-hand side of the induction hypothesis equivalence, (+ (length tail) (length l2)), is contained in the left-hand side of the goal equivalence. Because our induction hypothesis states that this expression is equivalent to (length (append tail 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:

    `(+ (length tail)) ≡ (length (append tail))`

    Since l1 is non-empty, evaluation simplifies the goal equivalence to:

    (+ 1 (+ (length tail) (length l2))) ≡ (+ 1 (length (append tail l2)))

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

    (+ 1 (length (append tail l2)) ≡ (+ 1 (length (append tail 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 length or append directly to the branch of the match 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, (+ (length l1) (length l2))(length (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:

        (+ (length '()) (length l2))
    --> (+ 0 (length l2))
    --> (length l2)

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

        (length (append '() l2))
    --> (length l2)
  • l1 is non-empty. Let head and tail be the head element and tail of l1, respectively. Our induction hypothesis is:

    Inductive hypothesis: (+ (length tail) (length l2))(length (append tail l2)).

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

    --> (+ (length l1) (length l2))
    --> (+ (+ 1 (length tail)) (length l2))
    --> (+ 1 (+ (length tail) (length l2)))

    The final step of evaluation comes from the commutative property of addition: \((1 + x) + y = 1 + (x + y)\).

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

    --> (length (append l1 l2))
    --> (length (cons head (append tail l2)))
    --> (+ 1 (length (append tail l2)))

    In summary, we now have:

    (+ 1 (+ (length tail) (length l2))) ≡ (+ 1 (length (append tail l2)))

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

    (+ 1 (length (append tail l2))) ≡ (+ 1 (length (append tail 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.