[Haskell-cafe] Induction (help!)
ryani.spam at gmail.com
Tue May 6 20:21:23 EDT 2008
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
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).
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
More information about the Haskell-Cafe