Dan Weston westondan at imageworks.com
Tue May 6 21:30:08 EDT 2008

```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

[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
> _______________________________________________