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

[David Menendez]

Benjamin Franksen writes:

> On Wednesday 04 May 2005 01:32, Ben Rudiak-Gould wrote:
> > This doesn't work in Haskell because Haskell types aren't
> > constructed in this way. It's harder to prove properties of types
> > in Haskell (and fewer properties actually hold).
> 
> Could you explain why this is so? Or rather, what the appropriate
> technique is in Haskell? I assume it has to do with laziness but I
> have no idea how it enters the picture.

I suspect it's because Haskell types are non-strict by default.

Given

data Nat = Zero | Succ Nat

in a strict language, Succ _|_ == _|_. This is not the case in Haskell.

This isn't the case in Haskell, which is why we can do things like:

infinity = Succ infinity

Haskell lets you treat infinity mostly as though it were a normal value
of Nat. You can do arithmetic and compare it to finite values without
ever hitting bottom.
-- 
David Menendez <[EMAIL PROTECTED]> 
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Benjamin Franksen]

On Wednesday 04 May 2005 01:32, Ben Rudiak-Gould wrote:
> This doesn't work in Haskell because Haskell types aren't constructed in
> this way. It's harder to prove properties of types in Haskell (and fewer
> properties actually hold).

Could you explain why this is so? Or rather, what the appropriate technique is 
in Haskell? I assume it has to do with laziness but I have no idea how it 
enters the picture.

Ben
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Ben Rudiak-Gould]

Echo Nolan wrote:
My copy of HS: The Craft Of FP just arrived and I was reading
section 8.5 about induction. On page 141, Simon Thompson gives a
method of proving properties of functions on lists:
1) Prove that the property holds for the null list
2) Prove that the property holds for (x:xs) under the assumption
that the property holds for xs.
My question is this: what is the proof of
> (P([]) and ( P(xs) => P(x:xs))) => P(xs)?
Forget all the other replies. :-) The *real* reason that induction is a 
valid method of proving properties of lists is that *lists are themselves 
defined inductively*. (Except they aren't in Haskell--but let's pretend 
we're talking about ML for the moment.)

In ML (with Haskell syntax), when you write
data Nat = Zero | Succ Nat
what it means is something like this:
  1. Zero is in Nat.
  2. If x is in Nat, then Succ x is in Nat.
  3. Nat contains only such elements as can be proven to belong to it by
 rules 1 and 2.
For example, Succ Zero is in Nat. Proof: Zero is in Nat (1); if Zero is in 
Nat, then Succ Zero is in Nat (instantiation of (2)); Succ Zero is in Nat 
(modus ponens). Note that this mirrors the way the value is actually 
constructed in program code (the Curry-Howard isomorphism).

Now, suppose you've proven
  A. P(Zero).
  B. P(x) => P(Succ x).
Let n be any element of Nat. By rule 3, there is a proof that n belongs to 
Nat. Take that proof, and replace every occurrence of "x is in Nat" with 
"P(x)". The result will be a proof of P(n).

In other words, the inductive structure of the type ensures that we can 
construct a proof of P(n) for any n in the type by gluing together a finite 
number of primitive pieces (one for each data constructor). This is why it's 
sufficient to prove just A and B, and why they have this particular form.

This doesn't work in Haskell because Haskell types aren't constructed in 
this way. It's harder to prove properties of types in Haskell (and fewer 
properties actually hold).

-- Ben
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Daniel Fischer]

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

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

[David Menendez]

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.
-- 
David Menendez <[EMAIL PROTECTED]> | "In this house, we obey the laws
  |of thermodynamics!"
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Clive Brettingham-Moore]

Although the answer to the original question was sort of embedded in the 
discussion, a quick read of the replies suggested that no one had made 
the simple clarification.

2) Prove that the property holds for (x:xs) under the assumption
that the property holds for xs.
It's not a general property it is a specific one, this is more clearly 
stated thus:

2) Prove that the property holds for (x:xs) given that it holds for a 
list xs.
Now, from 1 you already have a list xs =[], and then you have (x:[]) = 
[x], then (x2:[x]) = [x2,x] ... I think that you can see where this is 
going.
This is an example of a useful type of proof called proof by induction, 
which are related to natural numbers and counting. Induction gets a 
little uncertain with infinities which is what most of the posts where 
about, in summary: Haskell has infinite lists, infinite lists must be 
handled seperately in the proof.
Wikipedia has a fairly conventional explanation of induction 
http://en.wikipedia.org/wiki/Mathematical_induction

C
Echo Nolan wrote:
Hello all,
My copy of HS: The Craft Of FP just arrived and I was reading
section 8.5 about induction. On page 141, Simon Thompson gives a
method of proving properties of functions on lists:
1) Prove that the property holds for the null list
My question is this: what is the proof of (P([]) and ( P(xs) => P(x:xs))) 
=> P(xs)?
In other words, how does proof of the property on empty lists and proof
that the property holds on (x:xs) under the assumption that it holds on
xs give proof that it holds on all lists? Isn't there a recursive
dependency here? You are defining the proof for lists with at least one
element based on the assumption that it holds for all lists, right? How
does this get you a proof of the general property if it depends on the
assumption of the general property?
Regards and thanks,
Echo Nolan.
 

 

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Cale Gibbard]

On 5/2/05, Cale Gibbard <[EMAIL PROTECTED]> wrote:
> On 5/2/05, robert dockins <[EMAIL PROTECTED]> wrote:
> > > Well, yes, but I'd argue that ordinary (transfinite) mathematical
> > > induction will work just fine here. It's just that the set we're doing
> > > mathematical induction over is one larger (in the ordinal sense) than
> > > usual. Let S = N union {w}, where N is the usual set of naturals and w
> > > is an additional new element. Adopt the usual well-ordering <= on N,
> > > and extend it to a new well-ordering by defining x <= w for every x.
> > >
> > > Assign finite completely defined lists their usual lengths, and every
> > > _|_ terminated or infinite list, length w.
> >
> > So every infinite object has a special length denoted "w".  I assume we
> > wish to make the following statements about "w"
> >
> > w = w
> > ~(w < w)
> >
> > Without which "=" and "<" fail to have their intended meaning.
> >
> > > Suppose that if the statement P(x) holds for every x < y then it holds
> > > for y as well. Then P(y) holds by mathematical induction.
> >
> > Then this induction hypothesis cannot apply to infinite lists.  Suppose
> > xs is infinite.  Then we assign it length "w".  Now, (x:xs) is also
> > infinite, and has length "w".  But, ~(w < w), so we cannot conclude that
> > P(x:xs) given P(xs).
> >
> I didn't claim that this what we need to prove in this case. We need
> to prove that P holds on lists of length w given that it holds on
> lists of every finite length.
> 
> > One simply cannot reason based on the "size" of an infinite object in
> > this way.  You require a form of structural reasoning, and that means
> > coinduction.

As an added note before I take a nap, if you find that the proof
requirement given this definition of length is too difficult, you
could also use the definition that [] and _|_ both have length zero,
(x:xs) has length one more than the length of xs, for finite and
finitely defined lists, and infinite lists have length w. This will
probably make the proof come out more easily (but both ways are
equally valid, provided that you meet the proof requirements for
mathematical induction). This way means that we will be allowed to
make use of the fact that P holds for all finite and finitely defined
lists in order to prove that it holds for infinite lists. As a
tradeoff, there's more work in the induction step and base case, but
it's likely the same kind of work we were already doing.
 - Cale
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Conor McBride]

Stefan Holdermans wrote:
Daniel,
Interestingly, we can also use induction to reason about infinite list. 
To this end, we use _|_ (`bottom' or `undefined') as a base case.

To prove something for both finite and infinite lists, one uses two base 
cases (_|_, and []) and takes the inductive step.
Are you sure this makes sense for a lazy language?
Conor
--
http://www.cs.nott.ac.uk/~ctm
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Cale Gibbard]

On 5/2/05, robert dockins <[EMAIL PROTECTED]> wrote:
> > Well, yes, but I'd argue that ordinary (transfinite) mathematical
> > induction will work just fine here. It's just that the set we're doing
> > mathematical induction over is one larger (in the ordinal sense) than
> > usual. Let S = N union {w}, where N is the usual set of naturals and w
> > is an additional new element. Adopt the usual well-ordering <= on N,
> > and extend it to a new well-ordering by defining x <= w for every x.
> >
> > Assign finite completely defined lists their usual lengths, and every
> > _|_ terminated or infinite list, length w.
> 
> So every infinite object has a special length denoted "w".  I assume we
> wish to make the following statements about "w"
> 
> w = w
> ~(w < w)
> 
> Without which "=" and "<" fail to have their intended meaning.
> 
> > Suppose that if the statement P(x) holds for every x < y then it holds
> > for y as well. Then P(y) holds by mathematical induction.
> 
> Then this induction hypothesis cannot apply to infinite lists.  Suppose
> xs is infinite.  Then we assign it length "w".  Now, (x:xs) is also
> infinite, and has length "w".  But, ~(w < w), so we cannot conclude that
> P(x:xs) given P(xs).
> 
I didn't claim that this what we need to prove in this case. We need
to prove that P holds on lists of length w given that it holds on
lists of every finite length.

> One simply cannot reason based on the "size" of an infinite object in
> this way.  You require a form of structural reasoning, and that means
> coinduction.
> 
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Jerzy Karczmarczuk]

robert dockins wrote:
Assign finite completely defined lists their usual lengths, and every
_|_ terminated or infinite list, length w.

So every infinite object has a special length denoted "w".  I assume 
we wish to make the following statements about "w"

w = w
~(w < w)
Without which "=" and "<" fail to have their intended meaning.
I don't know what's 'your' intended meaning of the length of an infinite
list, but I don't think you can prove or assume that ~(w
5 < 6
6 < 7
... go to aleph0.
Jerzy Karczmarczuk
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[robert dockins]

Well, yes, but I'd argue that ordinary (transfinite) mathematical
induction will work just fine here. It's just that the set we're doing
mathematical induction over is one larger (in the ordinal sense) than
usual. Let S = N union {w}, where N is the usual set of naturals and w
is an additional new element. Adopt the usual well-ordering <= on N,
and extend it to a new well-ordering by defining x <= w for every x.
Assign finite completely defined lists their usual lengths, and every
_|_ terminated or infinite list, length w.
So every infinite object has a special length denoted "w".  I assume we 
wish to make the following statements about "w"

w = w
~(w < w)
Without which "=" and "<" fail to have their intended meaning.
Suppose that if the statement P(x) holds for every x < y then it holds
for y as well. Then P(y) holds by mathematical induction.
Then this induction hypothesis cannot apply to infinite lists.  Suppose
xs is infinite.  Then we assign it length "w".  Now, (x:xs) is also 
infinite, and has length "w".  But, ~(w < w), so we cannot conclude that 
P(x:xs) given P(xs).

One simply cannot reason based on the "size" of an infinite object in 
this way.  You require a form of structural reasoning, and that means 
coinduction.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Cale Gibbard]

On 5/2/05, robert dockins <[EMAIL PROTECTED]> 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.
> 
> The problem here is that the haskell [] type is not actually an
> inductive type, but a coinductive type (which means one can construct
> infinite objects of that type).  The proof tools available to work with
> coinductive types differ somewhat from the tools used on inductive
> types.  In "Craft of FP", the author works with scheme, which has eager
> evaluation and thus cannot construct objects with coinductive type: thus
> the usual, familiar induction principles just work.  Haskell has lazy
> evaluation which allows the construction and manipulation of
> coinductive-typed objects.
> 
> Short story: when working with finite objects, regular induction works.
>   When working with infinite objects, be careful and read up on coinduction.
> 

Well, yes, but I'd argue that ordinary (transfinite) mathematical
induction will work just fine here. It's just that the set we're doing
mathematical induction over is one larger (in the ordinal sense) than
usual. Let S = N union {w}, where N is the usual set of naturals and w
is an additional new element. Adopt the usual well-ordering <= on N,
and extend it to a new well-ordering by defining x <= w for every x.

Assign finite completely defined lists their usual lengths, and every
_|_ terminated or infinite list, length w.

Suppose that if the statement P(x) holds for every x < y then it holds
for y as well. Then P(y) holds by mathematical induction.

This does indeed add an additional case to check relative to induction
over just the naturals, that is that if P(x) holds for every x in N,
then we must check that P(w) holds.

In general, this may or may not be a special case, though in the case
of lists, it almost certainly will be.
 - Cale
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[robert dockins]

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.
The problem here is that the haskell [] type is not actually an 
inductive type, but a coinductive type (which means one can construct 
infinite objects of that type).  The proof tools available to work with 
coinductive types differ somewhat from the tools used on inductive 
types.  In "Craft of FP", the author works with scheme, which has eager 
evaluation and thus cannot construct objects with coinductive type: thus 
the usual, familiar induction principles just work.  Haskell has lazy 
evaluation which allows the construction and manipulation of 
coinductive-typed objects.

Short story: when working with finite objects, regular induction works. 
 When working with infinite objects, be careful and read up on coinduction.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Jan-Willem Maessen]

On May 2, 2005, at 8:29 AM, Henning Thielemann wrote:
On Mon, 2 May 2005, Echo Nolan wrote:
Hello all,
My copy of HS: The Craft Of FP just arrived and I was reading
section 8.5 about induction. On page 141, Simon Thompson gives a
method of proving properties of functions on lists:
1) Prove that the property holds for the null list
2) Prove that the property holds for (x:xs) under the assumption
that the property holds for xs.
	My question is this: what is the proof of (P([]) and ( P(xs) => 
P(x:xs))) => P(xs)?
In other words, how does proof of the property on empty lists and 
proof
that the property holds on (x:xs) under the assumption that it holds 
on
xs give proof that it holds on all lists?
There must be some warranty that the resolution with respect to (:) 
stops somewhere. If you are sure that xs is shorter than x then the 
induction will stop sometimes. But if (x:xs) is infinite the induction 
won't work. I think you need some notion of the length of a list or 
some relation "one list is shorter than the other one" in order to 
explain induction.
Yes, to prove properties of an infinite (or a cyclic) list, 
co-recursion is indicated.  Briefly, we must *assume* that the property 
holds for xs, and show that it holds for (x:xs).  We must still show 
that it holds for [] if the property is to hold for finite lists as 
well.

I'll leave it to others better qualified than myself to flesh this 
picture out.  If induction leaves you dubious, you will find 
co-induction quite unconvincing. :-)

-Jan-Willem Maessen
___
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

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

[Stefan Holdermans]

Daniel,
Interestingly, we can also use induction to reason about infinite list. 
To this end, we use _|_ (`bottom' or `undefined') as a base case.

To prove something for both finite and infinite lists, one uses two 
base cases (_|_, and []) and takes the inductive step.

HTH,
Stefan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Cale Gibbard]

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

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

[Daniel Fischer]

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.

> >
> > 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

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

[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 :-)
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?
What does 'repeat' do?
Cheers,
Daniel.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Cale Gibbard]

This is, as others pointed out, an example of mathematical induction
at work. This is actually a slightly nontrivial instance of it, as
there is one more case than usual to be treated: lists can be
infinite. What happens to our proof when our list is infinite? Have we
really shown that the function works for all lists?

The answer is yes, the proof does work. Mathematical induction works
on what are called well-ordered sets. The naturals are just one
example. A set S with a relation <= is called well-ordered by <= if
the following hold:
1) <= is a partial order, that is:
 a) a <= a for every a in S (reflexivity)
 b) If a <= b and b <= a for any a,b in S, then a = b (antisymmetry)
 c) If a <= b and b <= c then a <= c for any a,b,c in S. (transitivity)
2) <= is additionally a total order, that is for any a and b in S,
we have a <= b or b <= a. (comparability)
3) Every nonempty subset T of S has a least element with respect to
<=. That is, there is some x in T such that for any a in T, we have x
<= a.

Note that the natural numbers are well-ordered by the usual <= under
this definition. Also, the lengths of lists, with the single infinity,
which I'll call w, under the ordering inherited from the naturals, and
x <= w for every x is still well ordered. (You might want to check
this) As an example, the set of integers with the usual ordering is
not well ordered.

Now suppose that F is some logical formula with a single free
variable, and that S is a well ordered set under the relation <=. Let
0 be the least element of S under this relation.

Additionally, suppose that F(0) is true (this is actually implied by
the following), and that if F(x) is true for all x < y in S,  then
F(y) is true as well. (x < y means that x <= y, and x /= y)

We will show that F(x) is true for all x in S by way of contradiction.

Suppose that there is some x such that F(x) is false. Consider the set
of all such x in S, that is {x | not F(x)}. This set is nonempty by
assumption, so it has a least element, say c.

Then for any x < c, F(x) must hold, because otherwise c would not be
the least element where F fails to be true. So, for every x < c, F(x)
is true, and by assumption F(c) must be true as well. But F(c) was
supposed to be false, which is a contradiction.

So our extra assumption that there was an x for which F(x) was false
must be wrong. So F(x) must be true for all x in S.

So, that's induction for sets of any size. It's possible to go a
little farther with it, but I think this is more than enough.

So there you have it, a proof that mathematical induction works. You
might want to check that the lengths of lists (including the infinite
length w) are well ordered.

I hope this helps.
 - Cale Gibbard

On 5/2/05, Echo Nolan <[EMAIL PROTECTED]> wrote:
> Hello all,
> My copy of HS: The Craft Of FP just arrived and I was reading
> section 8.5 about induction. On page 141, Simon Thompson gives a
> method of proving properties of functions on lists:
> 1) Prove that the property holds for the null list
> 2) Prove that the property holds for (x:xs) under the assumption
> that the property holds for xs.
> 
> My question is this: what is the proof of (P([]) and ( P(xs) => 
> P(x:xs))) => P(xs)?
> In other words, how does proof of the property on empty lists and proof
> that the property holds on (x:xs) under the assumption that it holds on
> xs give proof that it holds on all lists? Isn't there a recursive
> dependency here? You are defining the proof for lists with at least one
> element based on the assumption that it holds for all lists, right? How
> does this get you a proof of the general property if it depends on the
> assumption of the general property?
> 
> Regards and thanks,
> Echo Nolan.
> 
> 
> ___
> 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

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

[Henning Thielemann]

On Mon, 2 May 2005, Daniel Carrera wrote:
Daniel Fischer wrote:
Both do, but in Explanation 2, you omitted 'finite' a couple of times.
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 :-)
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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Daniel Carrera]

Daniel Fischer wrote:
Both do, but in Explanation 2, you omitted 'finite' a couple of times.
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 :-)

Cheers,
Daniel.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Daniel Fischer]

Am Montag, 2. Mai 2005 14:20 schrieb Daniel Carrera:
> Hi Echo,
>
> I'm totally new at Haskell btw. But I'll comment a bit. :-)
>
> > My copy of HS: The Craft Of FP just arrived
>
> Is it good? Do you recommend it? Should I get a copy too?

It is good. Best would be to have an extensive look and decide for yourself. 
But if that's not possible, I'd say, though rather expensive, it's worth the 
money. BTW, I don't know it, but the 'Haskell School of Expression' (by Paul 
Hudak, if I remember correctly) is said to be good, too, so you might want to 
take a look at both and compare.

>
> > and I was reading section 8.5 about induction. On page 141, Simon
> > Thompson gives a method of proving properties of functions on lists:
> > 1) Prove that the property holds for the null list
> > 2) Prove that the property holds for (x:xs) under the assumption
> > that the property holds for xs.
>
> Cool. Mathematical induction. I can see how that would be a sueful skil
> for an FP programmer.

Quite!
>
> > In other words, how does proof of the property on empty lists and proof
> > that the property holds on (x:xs) under the assumption that it holds on
> > xs give proof that it holds on all lists? Isn't there a recursive
> > dependency here?
>
> I'll offer two explanations. Hopefully one will make sense. :-)

Both do, but in Explanation 2, you omitted 'finite' a couple of times.

Let me rephrase it:
You prove P([]) and
(forall finite lists xs) (forall x) (P(xs) => P(x:xs)).

Then you can deduce P(ys) for all finite lists ys because all such are reached 
in a finite number of steps. (I tacitly assumed that all lists and elements 
are defined, the case of partially defined lists is treated later in the 
book.)
>
> Explanation 1:
>
> Fact (*): You proved P(xs) => P(x:xs).
>
> step 0: prove for the empty list.
> step 1: given (*) and step 0, you get the result for a 1-item list.
> step 2: given (*) and step 1, you get the result for a 2-item list.
> ...
> step n: given (*) and step n-1, you get the result for a n-item list.
>
> Explanation 2:
>
> Start with any list xs, it can be written in the form (y:ys). So if you
> prove the property for ys you're done, right? Continue this recursively,
> removing one entry on each round. Eventually you'll hit an empty list.
> But you proved the property for the empty. So, recursively, you've
> proven it for all lists.
>
> Hope that helps.
>
> This is called mathematical iduction. It is one of the most popular
> methods of proving theorems in mathematics.
>
>
> Cheers,
> Daniel.

Cheers back,
Daniel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Henning Thielemann]

On Mon, 2 May 2005, Echo Nolan wrote:
Hello all,
My copy of HS: The Craft Of FP just arrived and I was reading
section 8.5 about induction. On page 141, Simon Thompson gives a
method of proving properties of functions on lists:
1) Prove that the property holds for the null list
2) Prove that the property holds for (x:xs) under the assumption
that the property holds for xs.
My question is this: what is the proof of (P([]) and ( P(xs) => P(x:xs))) 
=> P(xs)?
In other words, how does proof of the property on empty lists and proof
that the property holds on (x:xs) under the assumption that it holds on
xs give proof that it holds on all lists?
There must be some warranty that the resolution with respect to (:) stops 
somewhere. If you are sure that xs is shorter than x then the induction 
will stop sometimes. But if (x:xs) is infinite the induction won't work. I 
think you need some notion of the length of a list or some relation "one 
list is shorter than the other one" in order to explain induction.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Daniel Carrera]

Hi Echo,
I'm totally new at Haskell btw. But I'll comment a bit. :-)
My copy of HS: The Craft Of FP just arrived
Is it good? Do you recommend it? Should I get a copy too?
and I was reading section 8.5 about induction. On page 141, Simon Thompson
gives a method of proving properties of functions on lists:
1) Prove that the property holds for the null list
2) Prove that the property holds for (x:xs) under the assumption
that the property holds for xs.
Cool. Mathematical induction. I can see how that would be a sueful skil 
for an FP programmer.

In other words, how does proof of the property on empty lists and proof
that the property holds on (x:xs) under the assumption that it holds on
xs give proof that it holds on all lists? Isn't there a recursive
dependency here?
I'll offer two explanations. Hopefully one will make sense. :-)
Explanation 1:
Fact (*): You proved P(xs) => P(x:xs).
step 0: prove for the empty list.
step 1: given (*) and step 0, you get the result for a 1-item list.
step 2: given (*) and step 1, you get the result for a 2-item list.
...
step n: given (*) and step n-1, you get the result for a n-item list.
Explanation 2:
Start with any list xs, it can be written in the form (y:ys). So if you 
prove the property for ys you're done, right? Continue this recursively, 
removing one entry on each round. Eventually you'll hit an empty list. 
But you proved the property for the empty. So, recursively, you've 
proven it for all lists.

Hope that helps.
This is called mathematical iduction. It is one of the most popular 
methods of proving theorems in mathematics.

Cheers,
Daniel.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe