[Haskell-cafe] Clarification on proof section of HS: The Craft of FP

[Cale Gibbard]

On 5/2/05, Daniel Fischer <daniel.is.fischer at web.de> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>