Paul: okay, da capo: We prove/test through case analysis
that the predicate p holds true for the first/starting case/element
in the sequence. When dealing with natural numbers this could be 0 or
1. We try the formula with 0 and if it returns the desired result we
move onto the next
Am Freitag, 9. Mai 2008 13:50 schrieb PR Stanley:
Paul: okay, da capo: We prove/test through case analysis
that the predicate p holds true for the first/starting case/element
in the sequence. When dealing with natural numbers this could be 0 or
1. We try the formula with 0 and if it
On 5/9/08, Daniel Fischer [EMAIL PROTECTED] wrote:
Right. I only wanted to say that we might have chosen the wrong base case for
the proposition. If p(0) doesn't hold, then obviously [for all n. p(n)]
doesn't hold. But [for all n. p(n) implies p(n+1)] could still be true, and
in that case, if
On Wed, May 7, 2008 at 8:01 PM, PR Stanley [EMAIL PROTECTED] wrote:
So, when you apply the function to the first element in the set - e.g. Zero
or Nil in the case of lists - you're actually testing to see the function
works. Then in the inductive step you base everything on the assumption that
You've got the right idea.
Paul: At long last! :-)
I should point out that it doesn't make sense to say p(Succ n) =
Succ(p(n)), p(x) represents some statement that is either true or
false, so it doesn't make sense to say Succ(p(n)). .
Paul: okay, da capo: We prove/test
Am Freitag, 9. Mai 2008 00:04 schrieb PR Stanley:
You've got the right idea.
Paul: At long last! :-)
I should point out that it doesn't make sense to say p(Succ n) =
Succ(p(n)), p(x) represents some statement that is either true or
false, so it doesn't make sense to say
On 5/8/08, Daniel Fischer [EMAIL PROTECTED] wrote:
No. In the induction step, we prove that
IF p(j) holds, THEN p(j+1) holds, too.
p(j) is the assumption, and we prove that *given that assumption*, p(j+1)
follows.
Then we have proved
(*) p(j) implies p(j+1), for all j.
To formalize this,
Hi
One of you chaps mentioned the Nat data type
data Nat = Zero | Succ Nat
Let's have
add :: Nat - Nat - Nat
add Zero n = n
add (Succ m)n = Succ (add m n)
Prove
add m Zero = m
I'm on the verge of giving up on this. :-(
Cheers
Paul
___
Haskell-Cafe
PR Stanley wrote:
add Zero n = n
So this function takes the left argument, and replaces Zero with n. Well
if n = Zero, this clearly leaves the left argument unchanged...
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
On Wed, May 7, 2008 at 9:27 PM, PR Stanley [EMAIL PROTECTED] wrote:
Hi
One of you chaps mentioned the Nat data type
data Nat = Zero | Succ Nat
Let's have
add :: Nat - Nat - Nat
add Zero n = n
add (Succ m)n = Succ (add m n)
Prove
add m Zero = m
To prove this by induction on m,
Paul,
Sometimes it helps to go exhaustively through every detail to be sure
there is no magic going on. Proceed only if you want exhaustive detail...
If it seems that people are skipping some steps in their argument, it is
because they are! They already understand it so well that they forgot
So, when you apply the function to the first element in the set -
e.g. Zero or Nil in the case of lists - you're actually testing to
see the function works. Then in the inductive step you base
everything on the assumption that p holds for some n and of course if
that's true then p must hold
Hi
I don't know what it is that I'm not getting where mathematical
induction is concerned. This is relevant to Haskell so I wonder if
any of you gents could explain in unambiguous terms the concept please.
The wikipedia article offers perhaps the least obfuscated definition
I've found so far
Am Dienstag, 6. Mai 2008 11:34 schrieb PR Stanley:
Hi
I don't know what it is that I'm not getting where mathematical
induction is concerned. This is relevant to Haskell so I wonder if
any of you gents could explain in unambiguous terms the concept please.
The wikipedia article offers perhaps
On Tue, May 6, 2008 at 5:34 AM, PR Stanley [EMAIL PROTECTED] wrote:
Hi
I don't know what it is that I'm not getting where mathematical induction
is concerned. This is relevant to Haskell so I wonder if any of you gents
could explain in unambiguous terms the concept please.
The wikipedia
After you grok induction over the naturals, you can start to think
about structural induction, which is usually what we use in
programming. They are related, and understanding one will help you
understand the other (structural induction actually made more sense to
me when I was learning, because
After you grok induction over the naturals, you can start to think
about structural induction, which is usually what we use in
programming. They are related, and understanding one will help you
understand the other (structural induction actually made more sense to
me when I was learning, because
Am Dienstag, 6. Mai 2008 23:34 schrieb PR Stanley:
After you grok induction over the naturals, you can start to think
about structural induction, which is usually what we use in
programming. They are related, and understanding one will help you
understand the other (structural induction
Another way to look at it is that induction is just a way to abbreviate proofs.
Lets say you have a proposition over the natural numbers that may or
may not be true; P(x).
If you can prove P(0), and given P(x) you can prove P(x+1), then for
any given natural number n, you can prove P(n):
insert
Ryan Ingram wrote:
One point to remember is that structural induction fails to hold on
infinite data structures:
As I understand it, structural induction works even for infinite data
structures if you remember that the base case is always _|_. [1]
Let the initial algebra functor F = const
20 matches
Mail list logo
