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.

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.

On 5/2/05, Daniel Fischer 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

On 5/2/05, robert dockins 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

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

On 5/2/05, Cale Gibbard wrote:

On 5/2/05, robert dockins 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

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

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

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

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 http://www.eyrie.org/~zednenem/