[Haskell-cafe] Induction (help!)
prstanley at ntlworld.com
Thu May 8 18:04:40 EDT 2008
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.
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).
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? 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?
More information about the Haskell-Cafe