List Induction
Contents
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
;We show that the length of the null list is zero
;1. (length null) ; Premise
;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
;Conclusion: The return value is zero, which is the length of the null list
Next, we need an inductive hypothesis. This is more difficult for lists. The concept is the same, but we need to more variables and 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 a set of lists where our property holds. Then prove that this set implies other lists. 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 set of lists called Q
;The lists in this set contain between 0 and k (inclusive) items
;For any list L in Q, the function (length L) will return x
;where x is the length of the list.
This inductive hypothesis creates a range where the function works correctly. We can use it during the inductive case. The longest list in the set \(Q\) has \(k\) elements. We can make a longer list by just using cons to add a new element to the list.
;Inductive Case
;Let A in Q such that (length A) = k
;Let x be any racket object
;We show that (length (cons x A)) = (+ 1 k)
;1. (length (cons x A)) ; Premise
;2. (if (null? (cons x A)) 0 ... ) ;Apply Definition of Length
;3. (if #f 0 ...) ;Evaluate Null?
;4. (+ 1 (length (rest (cons x A)))) ; Evaluate If
;5. (+ 1 (length A)) ;Evaluate Rest
;6. (+ 1 k) ;By IH
;Conclusion: The length is computed as (+ 1 k) if the IH holds.
;By Induction, we have shown our length function works correctly.
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
;Let B be a valid Racket List
;Let (length B) = n where n is an integer
;We show that (length (append null B)) = (length B)
;1. (length (append null B)) ;Premise
;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
;Conclusion: If A is null, it's length is 0.
;The return value is the length of list B
;Inductive Hypothesis
;Let there be a set of lists Q with between 0 and k elements (inclusive)
;such that if we select two lists A and B
;with (length A) = n
;and (length B) = m
;we have (length (append A B)) = (+ n m)
;Inductive Case
;Let x be some element in Racket
;1. (length (append (cons x A) B)) ;Premise
;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)) ;By IH
;Conclusion: Adding one new element to the first list
;increased the total size increased by 1
;By induction we have show that for any two value Racket Lists, the length of the appended list
;is the sum of the lengths of the two original 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:
;The length of the null list is zero before and after
;reversing
;1. (length (reverse null)) ; Premise
;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
;Conclusion: The initial and reversed list both have length 0
;Inductive Hypothesis
;Let us assume there exists a set of lists Q
;with between 0 and k elements (inclusive)
;For any value B in Q where (length B) = n
;we will have (length (reverse B)) = n
;Inductive Case
;1. (length (reverse (cons x B))) ; Premise
;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
;Concluded: The reverse increases by 1 when the list gets 1 extra element.
;By induction the length of a reversed list is always the as as its initial
;length.
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:
;The smallest whole number is 0
;which should return the null list.
;1. (intToBinary 0) ; Premise
;2. (cond [(= 0 0) null] ...) ;Apply Func Def.
;3. (cond [#t null] ...) ;Evaluate Equals
;4. null ; Evaluate If
;Conclusion: The result list is null for zero
;Inductive Hypothesis
;Let us assume for any whole number m in range
; 0 <= m <= k for some constant whole number k
; We have the following:
; (intToBinary m) = X where X is the correct binary representation
;Inductive Case 1
;Let us assume that k is an odd number
;We show the inductive hypothesis cases (intToBinary (+ k 1)
;to return (cons 0 X)
;1. (intToBinary (+ k 1)) ;Premise
;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
;Conclusion: (+ k 1) was an even number and an zero was added to the end
;of the list correctly
;Inductive Case 1
;Let us assume that k is an even number
;We show the inductive hypothesis cases (intToBinary (+ k 1)
;to return (cons 1 X)
;1. (intToBinary (+ k 1)) ;Premise
;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
;Conclusion: (+ k 1) was an odd number and an one was added to the end
;of the list correctly
;By induction we have show the function correctly computes
;the binary value of a number. Odd numbers already end in 1
;and even numbers always end in 0
;this pattern repeated for the entire number
;until 0