[Haskell-cafe] Clarification on proof section of HS: The Craft of
cgibbard at gmail.com
Mon May 2 11:00:09 EDT 2005
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 ++  == 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe