[Haskell-cafe] Induction (help!)

[Dan Weston]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
>