Another way to look at it is that induction is just a way to abbreviate proofs.
Lets say you have a proposition over the natural numbers that may or may not be true; P(x). If you can prove P(0), and given P(x) you can prove P(x+1), then for any given natural number n, you can prove P(n): <insert proof of P(0) here> <insert proof of P(0) => P(1) here> P(1). -- from P(0) and P(0) => P(1) <proof of P(1) => P(2)> P(2). -- from P(1) and P(1) => P(2) ... P(n-1). -- from P(n-2) and P(n-2) => P(n-1). <proof of P(n-1) => P(n)> P(n). -- from P(n-1) and P(n-1) => P(n) The magic thing about induction is that it gives you a unifying principle that allows you to skip these steps and prove an -infinite- number of hypotheses; even though the natural numbers is an infinite set, each number is still finite and therefore is subject to the same logic above. One point to remember is that structural induction fails to hold on infinite data structures: data Nat = Zero | Succ Nat deriving (Eq, Show) Take P(x) to be (x /= Succ x). P(0): Zero /= Succ Zero. (trivial) P(x) => P(Succ x) So, given P(x) which is: (x /= Succ x), we have to prove P(Succ x): (Succ x /= Succ (Succ x)) In the derived Eq typeclass: Succ a /= Succ b = a /= b Taking "x" for a and "Succ x" for b: Succ x /= Succ (Succ x) = x /= Succ x which is P(x). Now, consider the following definition: infinity :: Nat infinity = Succ infinity infinity /= Succ infinity == _|_; and if you go by definitional equality, infinity = Succ infinity, so even though P(x) holds on all natural numbers due to structural induction, it doesn't hold on this infinite number. -- ryan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe