Am Freitag, 9. Mai 2008 00:04 schrieb PR Stanley: > You've got the right idea. > Paul: At long last! :-) > I should point out that it doesn't make sense to say p(Succ n) = > Succ(p(n)), p(x) represents some statement that is either true or > false, so it doesn't make sense to say Succ(p(n)). . > Paul: okay, da capo: We prove/test through case analysis > that the predicate p holds true for the first/starting case/element > in the sequence. When dealing with natural numbers this could be 0 or > 1. We try the formula with 0 and if it returns the desired result we > move onto the next stage. If the formula doesn't work with 0 and so > the predicate does not hold true for the base case then we've proved > that it's a nonstarter.
Well, it might hold for all n >= 3. But you're right, if p doesn't hold for the base case, then it doesn't hold for _all_ cases. > > In the inductive step we'll make a couple of assumptions: we'll > imagine that p(j). We'll also assume that p holds true for the > successor of j - p(j+1). No. In the induction step, we prove that IF p(j) holds, THEN p(j+1) holds, too. p(j) is the assumption, and we prove that *given that assumption*, p(j+1) follows. Then we have proved (*) p(j) implies p(j+1), for all j. If we already have established the base case, p(0), we have p(0) and (p(0) implies p(1)) - the latter is a special case of (*) - from that follows p(1). Then we have p(1) and (p(1) implies p(2), again a special case of (*), therefore p(2). Now we have p(2) and (p(2) implies p(3)), hence p(3) and so on. > Then with the help of rules and the protocol available to us we'll > try to establish whether the formula (f) gives us f(j) = f(j+1) - f(1) > So, we know that the predicate holds for 0 or at least one element. > By the way, could we have 3 or 4 or any element other than 0? Sure, anything. Start with proving p(1073) and the induction proves p(n) for all n >= 1073, it does not say anything about n <= 1072. > Anyway, > p(0). Then we set out to find out if p holds for the successor of 0 > followed by the successor of the successor of 0 and so forth. > However, rather than laboriously applying p to every natural number > we innstead try to find out if f(j+1) - f(1) will take us back to > fj). I think this was the bit I wasn't getting. The assumptions in > the inductive step and the algebraic procedures are not to prove the > formula or premise per se. That's sort of been done with the base > case. Rather, they help us to illustrate that f remains consistent > while allowing for any random element to be succeeded or broken down > a successive step at a time until we reach the base/starting element/value. > Okay so far? Not quite, but close. > > Cheers > Paul > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
