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

• '()
• '(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.

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:

• (null? l) tests to see if the list is null, i.e., empty.
• (car l) returns the head of a (non-empty) list.
• (cdr l) returns the tail of a (non-empty) list.

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.

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:

• 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 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:

• We need to make sure that the guard of our conditional accurately reflects the cases of our data structure. Here, our list is either empty or non-empty which is captured by a null? check.
• We know that in the recursive case that our non-empty list is made up of a head and tail which we need to manually access using car and cdr, respectively. Let-bindings name these individual pieces so that we don’t interchange car and cdr in our code, but the let-binding adds a significant layer of complexity.

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:

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

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

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:

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

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

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

    (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!

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

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?

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.

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!

(+ 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:

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.

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:

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.