List Induction

General List Properties

Even if we don’t know the values in a list, sometimes we can still make claims about how the list will work.

Let \(x\) be any number. Let \(A\) be any valid list. There are some things we can predict knowing only these two things.

We have no idea what the result of (null? A) will be. Maybe it is null, maybe it is not. We don’t have enough information. We can say for certain that (null? (cons x A)) will return false. That list has at least one element. We can also be sure that (cons? (cons x A)) will return true.

We can also make predications about first and rest. We know first takes the first value out of the list. We can predict (first (cons x A)) will return x. We can also predict that (rest (cons x A)) will evaluate to A.

Putting these concepts together, we can predict that (null? (rest (cons x (cons y A)))) will return false.

Using this kind of reasoning, we can verify list functions using proofs by Induction.

Length Proof

The length function defines the length of a list. We want to verify it actually computes the correct value. The definition of length is given below.

(define (length N)
  (if (null? N) 
    0 
    (+ 1 (length (rest N)))
  )
)

We want to show that the length is computed correctly. The base case is the null list.

; Base Case
; Anchor at null list (length of 0)
; LHS
; 1. (length null) ; Premise of Base Case LHS
; 2. (if (null? null) 0 (+ 1 (length (rest null)))) ;Apply Def Length
; 3. (if #t 0 (+ 1 (length (rest null)))) ;Evaluate Null
; 4. 0 ;Evaluate If
; RHS
; 1. 0 ;Premise of Base Case RHS
;
; Since the LHS = RHS, the Base Case is established.

Next, we need an inductive hypothesis. This is more difficult for lists. The concept is the same, but we may need to more variables and/or assumptions to describe the situation. We cannot rely on the fact that anyone reading our proof knows what an integer is.

The basic plan is the same. We need to create lists where our property holds. Then prove that this implies other lists also hold. The implies statement can still create an infinite sequence. We still need to fall back on concepts from counting. We need a smaller set that can imply a larger set. With lists, we can use the number of elements in the list.

Imagine the set of all lists with at most \(5\) items in them. This is an infinite set, since we don’t define what items might appear. There is still a limit. You can only have at most \(5\) items in the list. A bigger set would be the set with at most \(6\) elements. This set is larger. This is the kind of implication we will need to create for lists.

We assume there is a set of lists that all have at most \(k\) elements. Then we use this assumption to prove properties of larger lists.

;Inductive Hypothesis
; Let us assume there exists a list L which 
; will cause (length L) to return x.
; Let x be the correct length of the list L.

This inductive hypothesis creates a lists where the function works. We can use it during the inductive case. We can make a longer list by just using cons to add a new element to the list.

; Leap Case
; Let k be any racket value.
; LHS
; 1. (length (cons k L)) ; Premise of Leap Case LHS
; 2. (if (null? (cons k L)) 0 ... ) ;Apply Definition of Length
; 3. (if #f 0 ...) ;Evaluate Null?
; 4. (+ 1 (length (rest (cons k L)))) ; Evaluate If
; 5. (+ 1 (length L)) ;Evaluate Rest
; 6. (+ 1 x) ; invoke IH
; RHS
; 7. (+ 1 x) ; Premise of Leap Case RHS
; Since LHS = RHS, the Leap Case is established.

; Both the Leap Case and Base Case are established,
; therefore, by POSI, we know the length function
; works correctly.

This time we can use POSI instead of POMI. This is short for Proof of Structural Induction. We did the proof on a data structure.

Append Proof

The append function takes two lists and merges all the elements into one longer list. The definition of append is given below.

(define (append A B)
    (if (null? A) 
        B 
        (cons (first A) (append (rest A) B))
    )
)

We want to prove that the length of the appended list is correct. If you append two lists, the resulting list should have a length equal to the sum of the two original lists. This means we correctly added all the elements from both lists.

;We Prove that the length of two appended lists is
; the sum of the lengths

; Base Case
; Anchored at first list is null.
; Let B be a valid Racket List
; Let (length B) = n where n is an integer
; LHS
; 1. (length (append null B)) ;Premise of Base Case LHS
; 2. (length (if (null? null) B ...)) ;Apply Def of Append
; 3. (length (if #t B ...)) ;Evaluate Null
; 4. (length B) ; Evaluate If
; 5. n ;by definition
; RHS
; 1. (length B) ;Premise of Base Case RHS
; 2. n ;by definition
; Since LHS=RHS we have established the Base Case.

; Inductive Hypothesis
; Let us assume there are two lists A and B
; with (length A) = n and (length B) = m
; then we have (length (append A B)) = (+ n m)

; Leap Case
; Let x be some element in Racket
; LHS
; 1. (length (append (cons x A) B)) ;Premise of Leap Case LHS
; 2. (length (if (null? (cons x A)) B ...)) ; Apply Def of Append
; 3. (length (if #f B ...)) ;Evaluate Null
; 4. (length (cons (first (cons x A)) (append (rest (cons x A)) B)) ;Eval If
; 5. (length (cons x (append (rest (cons x A)) B))) ; Evaluate First
; 6. (length (cons x (append A B))) ;Evaluate Rest
; 7. (if (null? (cons x (append A B))) 0 ...) ;Apply Def of Length
; 8. (if #f 0 ...) ;Evaluate Null?
; 9. (+ 1 (length (rest (cons x (append A B))))) ; Evaluate If
; 10. (+ 1 (length (append A B))) ; Evaluate Rest
; 11. (+ 1 (+ n m)) ;invoke IH
; RHS
; 1. (+ (length (cons x A)) (length B)) ; Premise of Leap Case RHS
; 2. (+ (if (null? (cons x A)) 0 (+ 1 (length A))) (length B)) ;Apply Def of Length
; 3. (+ (if #false 0 (+ 1 (length A))) (length B)) ; Evaluate Null?
; 4. (+ (+ 1 (length A)) (length B)) ; Evaluate If
; 5. (+ (+ 1 n) (length B)) ; By Definition of A
; 6. (+ (+ 1 n) m) ; by Definition of B
; 7. (+ 1 (+ n m)) ; Algebraic Reordering (Math)
; Since LHS = RHS, the Leap Case is Established.
;
; Since both the Leap Case and Base Case are established,
; by POSI we have 
; (length (append X) (append Y)) = (+ (length X) (length Y))
; for all Racket Lists.

Reverse Proof

We want to look at what happens to lists when we reverse them. The definition of reverse is given below.

(define (reverse A)
    (if (null? A) 
        null 
        (append (reverse (rest A)) (cons (first A) null))
    )
)

We show that reversing a list does not change it length.

;We show the length of a reversed list is equal to its original length

; Base Case:
; Anchored at null list.
; LHS
; 1. (length (reverse null)) ; Premise of Base Case LHS
; 2. (length (if (null? null) null ...)) ;Apply Func Def.
; 3. (length (if #t null ..)) ;Evaluate Null
; 4. (length null) ; Evaluate If
; 5. (if (null? null) 0 ...) ;Apply Def of Length
; 6. (if #t 0 ...) ; Evaluate Null
; 7. 0 ; Evaluate If
; RHS
; 1. (length null) ; Premise of Base Case RHS
; 2. (if (null? null) 0 ...) ; Apply Def of Length
; 3. (if #t 0 ...) ; Evaluate Null?
; 4. 0 ;Evaluate If
; Since LHS = RHS the Base Case is established.

; Inductive Hypothesis
; Let us assume B is a list with (length B) = n
; then we will have (length (reverse B)) = n

; Leap Case
; Let x be some racket value.
; LHS
; 1. (length (reverse (cons x B))) ; Premise of Leap Case LHS
; 2. (length (if (null? (cons x B)) null ...)) ;Apply Def of Reverse
; 3. (length (if #f null ...)) ;Evaluate Null
; 4. (length (append (reverse (rest (cons x B)))
;           (cons (first (cons x B)) null)) ; Evaluate If
; 5. (length (append (reverse B)
;            (cons (first (cons x B)) null)) ;Evaluate Rest
; 6. (length (append (reverse B) (cons x null))) ; Evaluate First
; 7. (+ (length (reverse B)) (length (cons x null))) ;By previous append proof
; 8. (+ n (length (cons x null))) ; By IH
; 9. (+ n (if (null? (cons x null)) 0 ...)) ; Apply Def of Length
; 10. (+ n (if #f 0 ...)) ;Evaluate Null?
; 11. (+ n (+ 1 (length (rest (cons x null))))) ; Evaluate If
; 12. (+ n (+ 1 (length null))) ;Evaluate Rest
; 13. (+ n (+ 1 (if (null? null) 0 ...))) ;Apply Def of Length
; 14. (+ n (+ 1 (if #t 0 ...))) ;Evaluate Null
; 15. (+ n (+ 1 0)) ; Evaluate If
; 16. (+ n 1) ; Simple Math
; RHS
; 1. (length (cons x B)) ; Premise of RHS
; 2. (if (null? (cons x B)) 0 ...) ;Apply Def of length
; 3. (if #f 0 ...) ;Evaluate Null?
; 4. (+ 1 (length B)) ; Evaluate If
; 5. (+ 1 n) ; By definition
; Since LHS = RHS, the Leap Case is Established.

; Since both the Leap Case and Base Case are established,
; by POSI we have 
; (length (reverse X))= (length X)
; for all Racket Lists.

Multiple Cases

Sometimes we will need to create multiple base cases or inductive cases. Some situations will not have exactly one base case or exactly one inductive case. This is normally determined by the code itself.

The following function converts an integer to a binary number. It makes a list of ones and zeros for the binary number. The list is created in reverse binary.

;input-contract: A integer
;output-contract: A list of 0/1. (Reverse Binary)
(define (intToBinary N)
  (cond
    [(= N 0) null]
    [(= (remainder N 2) 0)
     (cons 0 (intToBinary (quotient N 2)))]
    [(= (remainder N 2) 1)
     (cons 1 (intToBinary (quotient N 2)))]
  )
)

This function definition has three conditions. There is one base case and two recursive cases. This means, if we want to prove something about it we need three cases. We will need one base case, and two inductive cases. Even and odd numbers work differently in this function. We need to make sure they both work correctly. This function creates the minimum binary list, so it has no extra zeros in it.

Since this function has conditions it will not fit on a single line. We need to compress parts that are not related to the condition we are looking at.

We will show that the function correctly computes the binary value of a given whole number.

;We show that intToBinary computes the correct binary number
;for any whole number

;Base Case:
; Anchored at 0
; LHS
; 1. (intToBinary 0) ; Premise of Base Case LHS
; 2. (cond [(= 0 0) null] ...) ;Apply Func Def.
; 3. (cond [#t null] ...) ;Evaluate Equals
; 4. null ; Evaluate If
; RHS
; 1. null ;Premise of Base Case RHS
; Since RHS = LHS the Base Case is established.

; Inductive Hypothesis
; Let us assume for any whole number k
; (intToBinary k) = X where X is the correct binary representation.

; Leap Case 1
; Let us assume that k is an odd number
; We show the inductive hypothesis causes (intToBinary (+ k 1) 
; to return (cons 0 X).
; LHS
; 1. (intToBinary (+ k 1)) ;Premise of Leap Case RHS
; 2. (cond [(= (+ k 1) 0) null] ...) ;Apply Def of Function
; 3. (cond [#f 0] ...) ;Evaluate Equals
; 4. (cond ...  [(= (remainder (+ k 1) 2) 0)
;     (cons 0 (intToBinary (quotient (+ k 1) 2)))] ...) ;Evaluate First Condition
; 5. (cond ...  [(= 0 0) (cons 0 (intToBinary (quotient (+ k 1) 2)))] ...) ;Evaluate Remainder
; 6. (cond ...  [#t (cons 0 (intToBinary (quotient (+ k 1) 2)))] ...) ;Evaluate Equals
; 7. (cons 0 (intToBinary (quotient (+ k 1) 2))) ;Evaluate Second Condition
; 8. (cons 0 X) ;by IH 
; RHS
; 1. (cons 0 X) ; Premise of RHS
; Since LHS = RHS we have established one leap case.

; Leap Case 2
; Let us assume that k is an even number
; We show the inductive hypothesis cases (intToBinary (+ k 1) 
; to return (cons 1 X)
; LHS
; 1. (intToBinary (+ k 1)) ;Premise of Leap Case LHS
; 2. (cond [(= (+ k 1) 0) null] ...) ;Apply Def of Function
; 3. (cond [#f 0] ...) ;Evaluate Equals
; 4. (cond ...  [(= (remainder (+ k 1) 2) 0)
;     (cons 0 (intToBinary (quotient (+ k 1) 2)))] ...) ;Evaluate First Condition
; 5. (cond ...  [(= 1 0) (cons 0 (intToBinary (quotient (+ k 1) 2)))] ...) ;Evaluate Remainder
; 6. (cond ...  [#f (cons 0 (intToBinary (quotient (+ k 1) 2)))] ...) ;Evaluate Equals
; 7. (cond ... [(= (remainder (+ k 1) 2) 1)
;     (cons 1 (intToBinary (quotient (+ k 1) 2)))]) ;Evaluate Second Condition
; 8. (cond ... [(= 1 1))
;     (cons 1 (intToBinary (quotient (+ k 1) 2)))]) ;Evaluate Remainder
; 9. (cond ... [#t (cons 1 (intToBinary (quotient (+ k 1) 2)))]) ;Evaluate Equals
; 10. (cons 1 (intToBinary (quotient (+ k 1) 2))) ;Evaluate Third Condition
; 11. (cons 1 X) ;by IH
; RHS
; 1. (cons 1 X); Premise of RHS
; Since LHS = RHS we have established a second leap case.

;Conclusion: (+ k 1) was an odd number and an one was added to the end 
;of the list correctly

; Since all the Leap Case and Base Case are established,
; by POSI we have (intToBinary k) = X
; for any positive number k and it's correct
; binary representation X.