[Haskell-cafe] Induction (help!)
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
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
>
>
More information about the Haskell-Cafe
mailing list