Howdy. I'm working my way through
Concrete Abstractions, and I'm trying to understand this proof by induction thing. Here is the exercise (note, this is not homework, this is just self-study):
Consider the following procedure foo:
(define foo
(lambda (x n)
(if (= n 0)
1
(+ (expt x n) (foo x (- n 1))))))
Use induction to prove that (foo x n) terminates with the value
x^(n+1) - 1
-----------
x - 1
for all values of x =/ 1 and for all integers n >= 0. You may assume that expt works correctly, (i.e., (expt b m) returns bm). Hint: The inductive step will involve some algebra.
The base case is n = 0, which is 1, which works. I think I understand the inductive hypothesis step, which is to assume that
(foo x k) = ((x^k+1) - 1 / (x - 1)) for all values of k where x =/ 1 and 0 <= k < n. Not sure if that's right.
As far as the inductive step.. I don't know how to do it. I kind of understand the example in the book where the author does an inductive proof of the square procedure, but in trying to apply that same process to this foo procedure isn't working for me. Any help would be appreciated!
Edit: Another example, this one I think is easier, but I don't understand how it proves anything:
Prove by induction that for every nonnegative integer n the following procedure
computes 2n:
(define f
(lambda (n)
(if (= n 0)
0
(+ 2 (f (- n 1))))))
So, the Base case (n = 0) checks out, and if I assume that f(k) = 2k where 0 <= k < n, then f(n-1) = 2 + 2(n-1) = 2 + 2n - 2 = 2n. So, didn't I just prove that this function works by assuming that it does? Huh?
[Edited by - bodchook on December 23, 2008 12:32:41 PM]
