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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe