On 5/2/05, Daniel Fischer <[EMAIL PROTECTED]> wrote: > Am Montag, 2. Mai 2005 16:16 schrieb Daniel Carrera: > > Henning Thielemann wrote: > > >> Well, I also omited the word "countable". I figure it's understood > > >> since computers only deal with finite data. And given an infinite > > >> list, any finite "head" of it would meet the criteria, so the > > >> distinction is moot. Unless Haskell has some neat property I am not > > >> aware of :-) > > 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. > This property clearly violates the assumption for mathematical induction that if P(x) is true for all x < y, then P(y) is true.
> > > > > > If you don't take care you may end up "proving" that e.g. > > > repeat 1 ++ [0] == repeat 0 > > > because for the first list you can prove that every reachable element > > > is equal to its neighbour and the "last" element is 0. > > > > Note: I'm totally new at Haskell. > > > > What does ++ do? > > append two lists: [1,2] ++ [3,4] == [1,2,3,4] > > > What does 'repeat' do? > > create an infinite list with one distinct element: > > repeat 1 = [1,1,1,1,1,1,1, ... ad infinitum > > > > > Cheers, > > Daniel. > ditto > > _______________________________________________ > 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