[Haskell-cafe] Induction (help!)
PR Stanley
prstanley at ntlworld.com
Fri May 9 07:50:56 EDT 2008
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.
Paul: I don't understand the point you're contending. We've chosen 0
as our base case and if p(0) doesn't hold then nothing else will for
our proof. Granted, you may want to start from 3 or 4 as your base
case but we're not doing that here and for all we know forall n >= 3
p(n) but this isn't relevant to our proof, surely.
>
Paul: 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).
Daniel: 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.
Paul: No, you haven't proved anything! I'm sorry but your assertion
fails to make much sense.
Daniel: 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.
Paul: 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?
Daniel: 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.
Paul: 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?
Cheers,
Paul
More information about the Haskell-Cafe
mailing list