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 th
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 appropria
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
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 l
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
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
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 lar
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.
Ar
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
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 "<"
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
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. Un
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
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
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
__
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, a
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
> >> dis
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
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
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
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 distincti
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 de
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
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
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 f
25 matches
Mail list logo
