Ryan Ingram wrote:
One point to remember is that structural induction fails to hold on infinite data structures:
As I understand it, structural induction works even for infinite data structures if you remember that the base case is always _|_. [1] Let the initial algebra functor F = const Zero | Succ We have to prove that: P(_|_) holds if P(X) holds then P(F(X)) holds Here, we see that for P(x) = (x /= Succ x), since infinity = Succ infinity = _|_ then P(_|_) does not hold (since _|_ = Succ _|_ = _|_) As a counterexample, we can prove e.g. that length (L ++ M) = length L + length M See [2] for details, except that they neglect the base case P(_|_) and start instead with the F^1 case of P([]), so their proof is valid only for finite lists. We can include the base case too: length (_|_ ++ M) = length _|_ + length M length (_|_ ) = _|_ + length M _|_ = _|_ and similarly for M = _|_ and both _|_. So this law holds even for infinite lists. [1] Richard Bird, "Introduction to Functional Programming using Haskell", p. 67 [2] http://en.wikipedia.org/wiki/Structural_induction Also note that
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