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 bu
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 per
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 wikipedi
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 I
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 ac
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):
P(1)
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 Z
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
Am Mittwoch, 7. Mai 2008 23:27 schrieb PR Stanley:
> 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. :-(
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
http://www.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 i
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 for
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
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 through
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 Succ(
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 t
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
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
21 matches
Mail list logo
