Strong induction on the length of a List ======================================== Recall that generative functions must come with a termination argument. To prove things about generative recursive functions, we generally have to express that termination argument as a new induction principle. The reason is that structural induction principles only give us induction hypotheses for recursive calls on the immediate pieces of an input. But generative recursive functions recur on arbitrary smaller problems that are usually generated by a helper function, and so the induction hypotheses of the SIP tend not to help. Think about quicksort. It recurs on an arbitrary but shorter list that is generated from the one it is given. Further, when it receives the empty list, quicksort stops. Thus quicksort terminates because the length of the input decreases at each recursive call, and when it reaches the smallest length, quicksort does not recur anymore. In HtDP, we taught you that generative function design usally involves a "eureka step." Here is a eureka step: that last paragraph sounds an awful lot like strong induction on the natural numbers, except that we're producing the natural numbers by computing the length of a list. Suppose I have a subset S of N. To show S = N, I have to prove: 0 : S all n:N. {k:N | k <= n} <= S -> n+1 : S Let's fiddle with this to try to come up with a plausible induction principle that would work for quicksort. In that case, S is a subset of LoN. So I will replace 0 : S with nil : S because (len nil) = 0. nil : S And let's tinker with the inductive case like so: all n:N {k : LoN | (len k) <= n} <= S -> {(cons x k) | x:N, k:LoN, (len k) <= n} <= S That says that I will assume that every list of length no more than n satisfies that property and then prove that every list of length no more than n+1 satisfies the property too. Lists of length no more than n+1 can be written as (cons x k) when k is a list of length no more than n. This principle would work for quicksort because it allows us to assume that a property holds for every list smaller than the one we are given. Remember, that we're only tinkering and speculating so far. If we want to use this principle, then we must prove that it is correct. To do that, we'll use a technique similar to the one we used to come up with the structural induction principle. Define Q : N -> Set[LoN] Q(n) = {l:LoN | (len l) <= n} For each n:N, Q(n) is the subset of LoN of length at most n. Let Q* = Union n:N Q(n). I claim that Q* = LoN. Lemma 1: Q* <= LoN because all n:N. Q(n) <= LoN, by induction on n. Do it. Lemma 2: Q* is L-closed. Proof: do it yourself. Corollary: Q* = LoN. Proof: Since LoN is the smallest L-closed set, we have LoN <= Q*. Combined with lemma 1 we have Q* = LoN, Q.E.D. Now if we want to show that some subset S of LoN is in fact equal to LoN, we can choose to show S = Q* instead: we just show all n:N.Q(n) <= S. In other words, we reduce the problem to induction on N! So given S, the base case is: - nil : S, because Q(0) = {nil} <= S and the inductive case is: - all n:N. if Q(n), then Q(n+1) Expanding the definition of Q, the inductive case is equivalent to: all n:N.{l:LoN | (len l) <= n} <= S -> {l:LoN | (len l) <= n+1} <= S. But we already have to show nil:S from no assumptions anyway, and so we can simplify the right-hand side by only considering conses: all n:N.{l:LoN | (len l) <= n} <= S -> {(cons x l) | x:N, l:LoN, (len l) <= n} <= S And there's the induction principle that we speculated would work. Eureka! Fortunately, using the new induction principle requires no more insight than using the structural induction principle. Theorem: all xs:LoN. (qsort xs) = (isort xs). Proof: We proceed by induction on the length of xs. Base case: (qsort nil) = nil = (isort nil). Inductive case: We must show (qsort (cons p xs)) = (isort (cons p xs)). IH: Assume (qsort l) = (isort l) whenever (len l) <= (len xs). We calculate: (qsort (cons p xs)) = (append (qsort (select-<= xs p)) (cons p (qsort (select-> xs p)))) *1 Assuming both of: (len (select-<= xs p)) <= (len xs) (len (select-> xs p)) <= (len xs) allows us to use the induction hypothesis on each recursive call to qsort. That leaves us with: = (append (isort (select-<= xs p)) (cons p (isort (select-> xs p)))) *2 We know that p is smaller than all of the members of (select-> xs p). So we can push the (cons p ...) inside the second isort because the isort should just stick p in the front. = (append (isort (select-<= xs p)) (isort (cons p (select-> xs p)))) *3 And we expect that appending two sorted lists yields the same result as sorting the appended lists. Note that we need to take advantage of the fact that all the elements in the first list are no larger than all the elements in the second list. = (isort (append (select-<= xs p) (cons p (select-> xs p)))) *4 Now, if we change the order of the list items inside the argument of isort, the result shouldn't change. So let's pull the (cons p ...) out in front of the append: = (isort (cons p (append (select-<= xs p) (select-> xs p)))) *5 It would be nice if we could claim that (append (select-<= xs p) (select-> xs p)) = xs but of course that's not generally true (you should find a counterexample that falsifies this equation). Instead, we recognize we are calling isort on a cons. We can use the definition of isort to simplify to: = (insert p (isort (append (select-<= xs p) (select-> xs p)))) *6 Now we are in a better position because surely we can prove that (isort (append (select-<= xs p) (select-> xs p))) = (isort xs). If so, then we could simplify to: = (insert p (isort xs)) And then use the definition of isort backwards to conclude = (isort (cons p xs)) Q.E.D., modulo the assumptions marked *1 through *6. We need to turn each assumption into a lemma and prove them in order to finish the proof. Now go read HW #7 ;)