Am Dienstag, 3. Mai 2005 03:48 schrieben Sie:
Daniel Fischer writes:
Due to lazyness, we can have infinite lists (and other infinite structures) in Haskell (of course, in finite time, only a finite portion of those can be evaluated), e.g. ns = [1 .. ] :: [Integer] is an infinite list which is often used. And now consider the property P that there exists a natural number n so that the list l has length n.
Obviously P holds for all finite lists, but not for the infinite list ns.
You can avoid some problems like that by using lazy naturals, e.g.:
data Nat = Zero | Succ Nat
instance Eq Nat where m == n = compare m n == EQ
instance Ord Nat where compare Zero Zero = EQ compare Zero (Succ _) = LT compare (Succ _) Zero = GT compare (Succ m) (Succ n) = compare m n
infinity = Succ infinity
length [] = Zero length (x:xs) = Succ (length xs)
Everything terminates, as long as you don't try to compare two infinite values.
Mea culpa, I probably should have stated it quite explicitly: this example was intended to illustrate the difference between finite and infinite lists with respect to inductive proofs. The proof scheme (1) P([]) (2) (forall xs) (forall x) (P(xs) => P(x:xs)) yields an induction over the natural numbers: let Q(n) = for all lists xs of length n, P(xs) holds. Then (1) --> (i) Q(0), (2) --> (ii) (forall n) (Q(n) => Q(n+1)). But by step (ii) we only reach successor ordinals, so, as Cale Gibbard pointed out, to handle infinite lists we must take the step to transfinite induction, for 'w' (closest Ascii character to omega) is a limit ordinal. The scheme for transfinite induction is (i) Q(0) (iia) [(forall n) (n < m => Q(n))] => Q(m) as stated by Cale. This reaches all ordinals. My example has the property that (ii) holds, but (iia) doesn't. Conclusion: to handle infinite lists, we must extend our toolkit - replacing (ii) by (iia) isn't the only possibility, of course. Cheers, Daniel