Induction (help!)

[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 the least obfuscated definition
I've found so far but I would still like more clarity.
The idea is to move onto inductive proof in Haskell. First, however,
I need to understand the general mathematical concept.

Top marks for clarity and explanation of technical terms.
         Thanks
Paul

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

[Achim Schneider]

PR Stanley <prstanley@...> 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 article offers perhaps the least obfuscated
> definition I've found so far but I would still like more clarity.
> The idea is to move onto inductive proof in Haskell. First, however,
> I need to understand the general mathematical concept.
>
> Top marks for clarity and explanation of technical terms.
> Thanks
> Paul
>

Induction -> from the small picture, extrapolate the big
Deduction -> from the big picture, extrapolate the small

Thus, in traditional logic, if you induce "all apples are red", simple
observation of a single non-red apple quickly reduces your result to
"at least one apple is not red on one side, all others may be red",
i.e, you can't deduce "all apples are red" with your samples anymore.

As used in mathematical induction, deductionaly sound:

1) Let "apple" be defined as being of continuous colour.
2) All "apples" are of the same colour
3) One observed "apple" is red
Ergo: All "apples" are red

Q.E.D.


The question that is left is what the heck an "apple" is, and how it
differs from these things you see at a supermarket. It could, from the
above proof, be a symbol for "red rubberband". The samples are defined
by the logic.

Proposition 2 should be of course inferable from looking at one single
apple, or you're going to look quite silly. It only works in
mathematics, where you can have exact, either complete or part-wise,
"copies" of something. If you can think of a real-world example where
this works, please speak up.

That's it. Aristotlean logic sucks.

--
(c) this sig last receiving data processing entity. Inspect headers for
past copyright information. All rights reserved. Unauthorised copying,
hiring, renting, public performance and/or broadcasting of this
signature prohibited.

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

[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 the least obfuscated
> > definition I've found so far but I would still like more clarity.
> > The idea is to move onto inductive proof in Haskell. First, however,
> > I need to understand the general mathematical concept.
> >
> > Top marks for clarity and explanation of technical terms.
> >       Thanks
> > Paul
> >
>Induction -> from the small picture, extrapolate the big
>Deduction -> from the big picture, extrapolate the small
>
>Thus, in traditional logic, if you induce "all apples are red", simple
>observation of a single non-red apple quickly reduces your result to
>"at least one apple is not red on one side, all others may be red",
>i.e, you can't deduce "all apples are red" with your samples anymore.

         Paul: surely, you wouldn't come up with an incorrect premise
like "all apples are red" in the first place.
Sorry, still none the wiser
Cheers,
Paul

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

[Daniel Fischer-4]

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 the least obfuscated definition
> I've found so far but I would still like more clarity.
> The idea is to move onto inductive proof in Haskell. First, however,
> I need to understand the general mathematical concept.
>
> Top marks for clarity and explanation of technical terms.
> Thanks
> Paul
>

Mathematical induction is a method to prove that some proposition P holds for
all natural numbers.

The principle of mathematical induction says that if
1) P(0) holds and
2) for every natural number n, if P(n) holds, then also P(n+1) holds,
then P holds for all natural numbers.

If you choose another base case, say k instead of 0, so use
1') P(k) holds,
then you can deduce that P holds for all natural numbers greater than or equal
to k.

You can convince yourself of the validity of the principle the following ways:
Direct:
By 1), P(0) is true.
Specialising n to 0 in 2), since we already know that P(0) holds, we deduce
that P(1) holds, too.
Now specialising n to 1 in 2), since we already know that P(1) is true, we
deduce that P(2) is also true.
And so on ... after k such specialisations we have found that P(k) is true.

Indirect:
Suppose there is an n1 such that P(n1) is false.
Let n0 be the smallest number for which P doesn't hold (there is one because
there are only finitely many natural numbers less than or equal to n1.
Technical term: the set of natural numbers is well-ordered, which means that
every non-empty subset contains a smallest element).
If n0 = 0, 1) doesn't hold, otherwise there is a natural number n (namely
n0-1), for which P(n) holds but not P(n+1), so 2) doesn't hold.


Example:
The sum of the first n odd numbers is n^2, or
1 + 3 + ... + 2*n-1 = n^2.

1) Base case:
a) n = 0: the sum of the first 0 odd numbers is 0 and 0^2 = 0.
b) n = 1: the sum of the first 1 odd numbers is 1 and 1^2 = 1.

2) Let n be an arbitrary natural number. We prove that if the induction
hypothesis - 1 + 3 + ... + 2*n-1 = n^2 - holds, then
1 + 3 + ... + 2*(n+1)-1 = (n+1)^2 holds, too.

1 + 3 + ... + 2*(n+1)-1
        = (1 + 3 + ... + 2*n-1) + 2*(n+1)-1
        = n^2 + 2*(n+1) -1       -- by the induction hypothesis
        = n^2 + 2*n + 1
        = (n+1)^2
cqfd.

Hope this helps,
Daniel


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

[Achim Schneider]

PR Stanley <prstanley@...> 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 article offers perhaps the least obfuscated
> > > definition I've found so far but I would still like more clarity.
> > > The idea is to move onto inductive proof in Haskell. First,
> > > however, I need to understand the general mathematical concept.
> > >
> > > Top marks for clarity and explanation of technical terms.
> > >       Thanks
> > > Paul
> > >
> >Induction -> from the small picture, extrapolate the big
> >Deduction -> from the big picture, extrapolate the small
> >
> >Thus, in traditional logic, if you induce "all apples are red",
> >simple observation of a single non-red apple quickly reduces your
> >result to "at least one apple is not red on one side, all others may
> >be red", i.e, you can't deduce "all apples are red" with your
> >samples anymore.
>
>          Paul: surely, you wouldn't come up with an incorrect premise
> like "all apples are red" in the first place.
> Sorry, still none the wiser
> Cheers,
> Paul

well, "all 'apples' are 'red'" is the proof you want to make. And it can
be correctly induced, if and only if you can prove that

a) all 'apples' share the same behaviour regarding the property 'colour'
b) one 'apple''s colour property is 'red'

which leads you directly to
c) every 'apple' (that is, potentially infinite many) 'apples' are
'red'.

if b) concludes that one 'apples''s colour property is not 'red', of
course, you can't say "all 'apples' are 'red'" and still write QED
beneath your proof without having to admit that that wasn't what you
wanted to demonstrate.

As an example, you might construct a proof that every faculty of any
number is positive:


fac 0 = 1
fac n | n > 0 = n * (fac (n-1))
fac _ = undefined

You don't have to go on to proving an infinite number of possible
inputs, you only have to prove

1) that 1 is positive (by definition)
2) that any number greater than 0 is positive (by definition)
3) that multiplication of two positive numbers results in a positive
number (by definition)
4) that only positive numbers get multiplicated (by analysing
haskell's semantics, read: data flow).

So, as soon as you have proved the properties of the fixed point, the
whole, infinite set is proven.

--
(c) this sig last receiving data processing entity. Inspect headers for
past copyright information. All rights reserved. Unauthorised copying,
hiring, renting, public performance and/or broadcasting of this
signature prohibited.

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

[Brandon S. Allbery KF8NH]

On 2008 May 6, at 8:37, PR Stanley wrote:

>> Thus, in traditional logic, if you induce "all apples are red",  
>> simple
>> observation of a single non-red apple quickly reduces your result to
>> "at least one apple is not red on one side, all others may be red",
>> i.e, you can't deduce "all apples are red" with your samples anymore.
>
>        Paul: surely, you wouldn't come up with an incorrect premise  
> like "all apples are red" in the first place.

You could come up with it as a hypothesis, if you've never seen a  
green or golden apple.  This is all that's needed; induction starts  
with "*if* P".

However, the real world is a really lousy way to understand inductive  
logic:  you can come up with hypotheses (base cases), but figuring out  
*what* the inductive step is is difficult at best --- never mind the  
impossibility of *proving* such.  Here's what we're trying to assert:

   IF... you have a red apple
   AND YOU CAN PROVE... that another related apple is also red
   THE YOU CAN CONCLUDE... that all such related apples are red

 From a mathematical perspective this is impossible; we haven't  
defined "apple", much less "related apple".  In other words, we can't  
assert either a hypothesis or an inductive case!  So much for the real  
world.

This only provides a way to construct if-thens, btw; it's easy to  
construct such that are false.  In mathematics you can sometimes  
resolve this by constructing a new set for which the hypothesis does  
hold:  for example, if you start with a proposition `P(n) : n is a  
natural number' and use the inductive case `P(n-1) : n-1 is a natural  
number', you run into trouble with n=0.  If you add the concept of  
negative numbers, you come up with a new proposition:  `P(n): n is an  
integer'.  This is more or less how the mathematical notion of integer  
came about, as naturals came from whole numbers (add 0) and complex  
numbers came from reals (add sqrt(-1)).

--
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@...
system administrator [openafs,heimdal,too many hats] allbery@...
electrical and computer engineering, carnegie mellon university    KF8NH


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

[Luke Palmer-2]

On Tue, May 6, 2008 at 4:53 AM, Achim Schneider <barsoap@...> wrote:

> PR Stanley <prstanley@...> 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 article offers perhaps the least obfuscated
>  > definition I've found so far but I would still like more clarity.
>  > The idea is to move onto inductive proof in Haskell. First, however,
>  > I need to understand the general mathematical concept.
>  >
>  > Top marks for clarity and explanation of technical terms.
>  >        Thanks
>  > Paul
>  >
>  Induction -> from the small picture, extrapolate the big
>  Deduction -> from the big picture, extrapolate the small

Induction has two meanings in mathematics, and I don't believe this is
the type of induction the OP was asking about.

See Daniel Fischer's response for the type you are asking about, and
try not to be confused by the irrelevant discussion about inductive
logic.

Luke

>  Thus, in traditional logic, if you induce "all apples are red", simple
>  observation of a single non-red apple quickly reduces your result to
>  "at least one apple is not red on one side, all others may be red",
>  i.e, you can't deduce "all apples are red" with your samples anymore.
>
>  As used in mathematical induction, deductionaly sound:
>
>  1) Let "apple" be defined as being of continuous colour.
>  2) All "apples" are of the same colour
>  3) One observed "apple" is red
>  Ergo: All "apples" are red
>
>  Q.E.D.
>
>
>  The question that is left is what the heck an "apple" is, and how it
>  differs from these things you see at a supermarket. It could, from the
>  above proof, be a symbol for "red rubberband". The samples are defined
>  by the logic.
>
>  Proposition 2 should be of course inferable from looking at one single
>  apple, or you're going to look quite silly. It only works in
>  mathematics, where you can have exact, either complete or part-wise,
>  "copies" of something. If you can think of a real-world example where
>  this works, please speak up.
>
>  That's it. Aristotlean logic sucks.
>
>  --
>  (c) this sig last receiving data processing entity. Inspect headers for
>  past copyright information. All rights reserved. Unauthorised copying,
>  hiring, renting, public performance and/or broadcasting of this
>  signature prohibited.
>
>
>
>  _______________________________________________
>  Haskell-Cafe mailing list
>  Haskell-Cafe@...
>  http://www.haskell.org/mailman/listinfo/haskell-cafe
>

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

[Brent Yorgey]

On Tue, May 6, 2008 at 5:34 AM, PR Stanley <prstanley@...> 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 article offers perhaps the least obfuscated definition I've found so far but I would still like more clarity.
The idea is to move onto inductive proof in Haskell. First, however, I need to understand the general mathematical concept.

Top marks for clarity and explanation of technical terms.
        Thanks
Paul

For a more intuitive view, mathematical induction (at least, induction over the integers) is like knocking over a chain of dominoes.  To knock over the whole (possibly infinite!) chain, you need two things:

1.  You need to make sure that each domino is close enough to knock over the next.
2.  You need to actually knock over the first domino.

Relating this to proving a proposition P for all nonnegative integers, step 1 is like proving that P(k) implies P(k+1) -- IF the kth domino gets knocked over (i.e. if P(k) is true), then it will also knock over the next one (P(k) implies P(k+1)).  Step 2 is like proving the base case -- P(0) is true.

Hopefully this helps you get a more intuitive view of what induction is all about; you can use some of the other responses to fill in more details.

-Brent

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

[Luke Palmer-2]

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 started as a programmer and then
became a mathematician, so I thought in terms of data structures).

So let's say you have a tree, and we want to count the number of
leaves in the tree.

    data Tree = Leaf Int | Branch Tree Tree

    countLeaves :: Tree -> Int
    countLeaves (Leaf _) = 1
    countLeaves (Branch l r) = countLeaves l + countLeaves r

We want to prove that countLeaves is correct.   So P(x) means
"countLeaves x == the number of leaves in x".

First we prove P(Leaf i), since leaves are the trees that have no
subtrees.  This is analogous to proving P(0) over the naturals.

    countLeaves (Leaf i) = 1, by definition of countLeaves.
    "Leaf i"  has exactly one leaf, obviously.
    So countLeaves (Leaf i) is correct.

Now to prove P(Branch l r), we get to assume that P holds for all of
its subtrees, namely we get to assume P(l) and P(r).  You can think of
this as constructing an algorithm to prove P for any tree, and we have
"already proved" it for l and r in our algorithm.  This is analogous
to proving P(n) => P(n+1) in the case of naturals. So:

   Assume P(l) and P(r).
   P(l) means "countLeaves l == the number of leaves in l"
   P(r) means "countLeaves r == the number of leaves in r"
   countLeaves (Branch l r) = countLeaves l + countLeaves r, by definition.
   And that is the number of leaves in "Branch l r", the sum of the
number of leaves in its two subtress.
   Therefore P(Branch l r).

Now that we have those two cases, we are done; P holds for any Tree whatsoever.

In general you will have to do one such proof for each case of your
data structure in order to prove a property for the whole thing.  At
each case you get to assume the property holds for all substructures.

Generally not so many steps are written down.  In fact in this
example, most people who do this kind of thing a lot would write
"straightforward induction", and that would be the whole proof :-)

The analogy between structural induction and induction over the
naturals is very strong; in fact induction over the naturals is just
induction over this data structure:

    data Nat = Zero | Succ Nat

Hope this helps.

Luke

On Tue, May 6, 2008 at 7:15 AM, Daniel Fischer <daniel.is.fischer@...> wrote:

> 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 the least obfuscated definition
>  > I've found so far but I would still like more clarity.
>  > The idea is to move onto inductive proof in Haskell. First, however,
>  > I need to understand the general mathematical concept.
>  >
>  > Top marks for clarity and explanation of technical terms.
>  >        Thanks
>  > Paul
>  >
>
>  Mathematical induction is a method to prove that some proposition P holds for
>  all natural numbers.
>
>  The principle of mathematical induction says that if
>  1) P(0) holds and
>  2) for every natural number n, if P(n) holds, then also P(n+1) holds,
>  then P holds for all natural numbers.
>
>  If you choose another base case, say k instead of 0, so use
>  1') P(k) holds,
>  then you can deduce that P holds for all natural numbers greater than or equal
>  to k.
>
>  You can convince yourself of the validity of the principle the following ways:
>  Direct:
>  By 1), P(0) is true.
>  Specialising n to 0 in 2), since we already know that P(0) holds, we deduce
>  that P(1) holds, too.
>  Now specialising n to 1 in 2), since we already know that P(1) is true, we
>  deduce that P(2) is also true.
>  And so on ... after k such specialisations we have found that P(k) is true.
>
>  Indirect:
>  Suppose there is an n1 such that P(n1) is false.
>  Let n0 be the smallest number for which P doesn't hold (there is one because
>  there are only finitely many natural numbers less than or equal to n1.
>  Technical term: the set of natural numbers is well-ordered, which means that
>  every non-empty subset contains a smallest element).
>  If n0 = 0, 1) doesn't hold, otherwise there is a natural number n (namely
>  n0-1), for which P(n) holds but not P(n+1), so 2) doesn't hold.
>
>
>  Example:
>  The sum of the first n odd numbers is n^2, or
>  1 + 3 + ... + 2*n-1 = n^2.
>
>  1) Base case:
>  a) n = 0: the sum of the first 0 odd numbers is 0 and 0^2 = 0.
>  b) n = 1: the sum of the first 1 odd numbers is 1 and 1^2 = 1.
>
>  2) Let n be an arbitrary natural number. We prove that if the induction
>  hypothesis - 1 + 3 + ... + 2*n-1 = n^2 - holds, then
>  1 + 3 + ... + 2*(n+1)-1 = (n+1)^2 holds, too.
>
>  1 + 3 + ... + 2*(n+1)-1
>         = (1 + 3 + ... + 2*n-1) + 2*(n+1)-1
>         = n^2 + 2*(n+1) -1       -- by the induction hypothesis
>         = n^2 + 2*n + 1
>         = (n+1)^2
>  cqfd.
>
>  Hope this helps,
>  Daniel
>
>
>
>
>  _______________________________________________
>  Haskell-Cafe mailing list
>  Haskell-Cafe@...
>  http://www.haskell.org/mailman/listinfo/haskell-cafe
>

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

[Achim Schneider]

"Luke Palmer" <lrpalmer@...> wrote:

> On Tue, May 6, 2008 at 4:53 AM, Achim Schneider <barsoap@...>
> wrote:
> > PR Stanley <prstanley@...> 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 article offers perhaps the least
> >  > obfuscated definition I've found so far but I would still like
> >  > more clarity. The idea is to move onto inductive proof in
> >  > Haskell. First, however, I need to understand the general
> >  > mathematical concept.
> >  >
> >  > Top marks for clarity and explanation of technical terms.
> >  >        Thanks
> >  > Paul
> >  >
> >  Induction -> from the small picture, extrapolate the big
> >  Deduction -> from the big picture, extrapolate the small
>
> Induction has two meanings in mathematics, and I don't believe this is
> the type of induction the OP was asking about.
>
> See Daniel Fischer's response for the type you are asking about, and
> try not to be confused by the irrelevant discussion about inductive
> logic.
>

I was referring to traditional logic in the aristotlean sense, I should
have been more explicit there. The key difference is really whether you
define (or proof) the big picture by the small picture, or try to make
deductions about some already-existant big thing by the small picture
you already have.

The method is the same, but the intent and awareness of the model
characteristic of your reasoning differ, thus leading to results that
are either valid or invalid.

--
(c) this sig last receiving data processing entity. Inspect headers for
past copyright information. All rights reserved. Unauthorised copying,
hiring, renting, public performance and/or broadcasting of this
signature prohibited.

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

[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 actually made more sense to
me when I was learning, because I started as a programmer and then
became a mathematician, so I thought in terms of data structures).
        Paul: I was hoping that understanding the classic mathematical
concept would help me appreciate the structural computer science)
variation better. I don't know what it is about induction that I'm
not seeing. It's so frustrating! Deduction in spite of the complexity
in some parts makes perfect sense. This, however, is a different beast!

So let's say you have a tree, and we want to count the number of
leaves in the tree.

     data Tree = Leaf Int | Branch Tree Tree

     countLeaves :: Tree -> Int
     countLeaves (Leaf _) = 1
     countLeaves (Branch l r) = countLeaves l + countLeaves r

We want to prove that countLeaves is correct.   So P(x) means
"countLeaves x == the number of leaves in x".
        Paul: By 'correct' presumably you mean sound.

First we prove P(Leaf i), since leaves are the trees that have no
subtrees.  This is analogous to proving P(0) over the naturals.
        Paul: I'd presume 'proof' here means applying the function to one
leaf to see if it returns 1. If I'm not mistaken this is establishing
the base case.

     countLeaves (Leaf i) = 1, by definition of countLeaves.
     "Leaf i"  has exactly one leaf, obviously.
     So countLeaves (Leaf i) is correct.

Now to prove P(Branch l r), we get to assume that P holds for all of
its subtrees, namely we get to assume P(l) and P(r).
        Paul: How did you arrive at this decision? Why can we assume that P
holds fr all its subtrees?

        You can think of this as constructing an algorithm to prove P for
any tree, and we have
"already proved" it for l and r in our algorithm.
        Paul: Is this the function definition for countLeaves?
       
        This is analogous to proving P(n) => P(n+1) in the case of naturals.
                Paul:I thought P(n) was the induction hypothesis and P(n+1) was the
proof that the formula/property holds for the subsequent element in
the sequence if P(n) is true. I don't see how countLeaves l and
countLeaves r are analogous to P(n) and P(n+1).
               
                So:

    Assume P(l) and P(r).
    P(l) means "countLeaves l == the number of leaves in l"
    P(r) means "countLeaves r == the number of leaves in r"
    countLeaves (Branch l r) = countLeaves l + countLeaves r, by definition.
    And that is the number of leaves in "Branch l r", the sum of the
number of leaves in its two subtress.
    Therefore P(Branch l r).

Now that we have those two cases, we are done; P holds for any Tree whatsoever.

In general you will have to do one such proof for each case of your
data structure in order to prove a property for the whole thing.  At
each case you get to assume the property holds for all substructures.

Generally not so many steps are written down.  In fact in this
example, most people who do this kind of thing a lot would write
"straightforward induction", and that would be the whole proof :-)

The analogy between structural induction and induction over the
naturals is very strong; in fact induction over the naturals is just
induction over this data structure:

     data Nat = Zero | Succ Nat

Hope this helps.

Luke

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

[Daniel Fischer-4]

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 actually made more sense to
> me when I was learning, because I started as a programmer and then
> became a mathematician, so I thought in terms of data structures).
> Paul: I was hoping that understanding the classic mathematical
> concept would help me appreciate the structural computer science)
> variation better.

Understanding either will help understanding the other, they're the same idea
in different guise.

> I don't know what it is about induction that I'm
> not seeing. It's so frustrating! Deduction in spite of the complexity
> in some parts makes perfect sense. This, however, is a different beast!
>
> So let's say you have a tree, and we want to count the number of
> leaves in the tree.
>
>      data Tree = Leaf Int | Branch Tree Tree
>
>      countLeaves :: Tree -> Int
>      countLeaves (Leaf _) = 1
>      countLeaves (Branch l r) = countLeaves l + countLeaves r
>
> We want to prove that countLeaves is correct.   So P(x) means
> "countLeaves x == the number of leaves in x".
> Paul: By 'correct' presumably you mean sound.
>
> First we prove P(Leaf i), since leaves are the trees that have no
> subtrees.  This is analogous to proving P(0) over the naturals.
> Paul: I'd presume 'proof' here means applying the function to one
> leaf to see if it returns 1. If I'm not mistaken this is establishing
> the base case.

Yes, right.

>
>      countLeaves (Leaf i) = 1, by definition of countLeaves.
>      "Leaf i"  has exactly one leaf, obviously.
>      So countLeaves (Leaf i) is correct.
>
> Now to prove P(Branch l r), we get to assume that P holds for all of
> its subtrees, namely we get to assume P(l) and P(r).
> Paul: How did you arrive at this decision? Why can we assume that P
> holds fr all its subtrees?

It's the induction hypothesis.
We could paraphrase the induction step as "If P holds for all cases of lesser
complexity than x, then P also holds for x".
In this example, the subtrees have lesser complexity than the entire tree (you
could define complexity as depth).
The induction step says "assuming P(l) and P(r), we can deduce P(Branch l r)",
or, as a formula,
forall l, r. ([P(l) and P(r)] ==> P(Branch l r)).

>
> You can think of this as constructing an algorithm to prove P for
> any tree, and we have
> "already proved" it for l and r in our algorithm.
> Paul: Is this the function definition for countLeaves?
>
> This is analogous to proving P(n) => P(n+1) in the case of naturals.
> Paul:I thought P(n) was the induction hypothesis and P(n+1) was the
> proof that the formula/property holds for the subsequent element in
> the sequence if P(n) is true. I don't see how countLeaves l and
> countLeaves r are analogous to P(n) and P(n+1).

(countLeaves l == number of leaves in l) and (countLeaves r == number of
leaves in r) together are analogous to P(n).
Proving
forall l, r. ([P(l) and P(r)] ==> P(Branch l r))
is analogous to proving
forall n. [P(n) ==> P(n+1)].

Let me phrase mathematical induction differently.
To prove
forall natural numbers n. P(n)
, it is sufficient to prove
1) P(0)
and
2) forall n. [P(n) implies P(n+1)]
. And structural induction for lists:
To prove
forall (finite) lists l . P(l)
, you prove
1L) P([ ])   -- the base case is the empty list
2L) forall x, l. [P(l) ==> P(x:l)]
and for trees:
to prove
forall trees t. P(t)
, you prove
1T) forall i. P(Leaf i)
2T) forall l, r. ([P(l) and P(r)] ==> P(Branch l r)).

In all three cases, the pattern is the same. The key thing is number 2, which
says if P holds for one level of complexity, then it also holds for the next
level of complexity. In the domino analogy, 2) says that the dominos are
placed close enough, so that a falling domino will tip its neighbour over.
Then 1) is tipping the first domino over.

>
> So:
>
>     Assume P(l) and P(r).
>     P(l) means "countLeaves l == the number of leaves in l"
>     P(r) means "countLeaves r == the number of leaves in r"
>     countLeaves (Branch l r) = countLeaves l + countLeaves r, by
> definition. And that is the number of leaves in "Branch l r", the sum of
> the number of leaves in its two subtress.
>     Therefore P(Branch l r).
>
> Now that we have those two cases, we are done; P holds for any Tree
> whatsoever.
>
> In general you will have to do one such proof for each case of your
> data structure in order to prove a property for the whole thing.  At
> each case you get to assume the property holds for all substructures.
>
> Generally not so many steps are written down.  In fact in this
> example, most people who do this kind of thing a lot would write
> "straightforward induction", and that would be the whole proof :-)
>
> The analogy between structural induction and induction over the
> naturals is very strong; in fact induction over the naturals is just
> induction over this data structure:
>
>      data Nat = Zero | Succ Nat
>
> Hope this helps.
>
> Luke
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@...
> http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[Ryan Ingram]

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 proof of P(0) here>
<insert proof of P(0) => P(1) here>
P(1). -- from P(0) and P(0) => P(1)
<proof of P(1) => P(2)>
P(2). -- from P(1) and P(1) => P(2)
...
P(n-1). -- from P(n-2) and P(n-2) => P(n-1).
<proof of P(n-1) => P(n)>
P(n). -- from P(n-1) and P(n-1) => P(n)

The magic thing about induction is that it gives you a unifying
principle that allows you to skip these steps and prove an -infinite-
number of hypotheses; even though the natural numbers is an infinite
set, each number is still finite and therefore is subject to the same
logic above.

One point to remember is that structural induction fails to hold on
infinite data structures:

data Nat = Zero | Succ Nat deriving (Eq, Show)

Take P(x) to be (x /= Succ x).

P(0):
Zero /= Succ Zero. (trivial)

P(x) => P(Succ x)

So, given P(x) which is: (x /= Succ x),
we have to prove P(Succ x): (Succ x /= Succ (Succ x))

In the derived Eq typeclass:
   Succ a /= Succ b = a /= b
Taking "x" for a and "Succ x" for b:
   Succ x /= Succ (Succ x) = x /= Succ x
which is P(x).

Now, consider the following definition:
infinity :: Nat
infinity = Succ infinity

infinity /= Succ infinity == _|_; and if you go by definitional
equality, infinity = Succ infinity, so even though P(x) holds on all
natural numbers due to structural induction, it doesn't hold on this
infinite number.

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

[Dan Weston]

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

We have to prove that:
P(_|_)  holds
if P(X) holds then P(F(X)) holds

Here, we see that for P(x) = (x /= Succ x), since

infinity = Succ infinity = _|_

then P(_|_) does not hold (since _|_ = Succ _|_ = _|_)

As a counterexample, we can prove e.g. that

length (L ++ M) = length L + length M

See [2] for details, except that they neglect the base case P(_|_) and
start instead with the F^1 case of P([]), so their proof is valid only
for finite lists. We can include the base case too:

length (_|_ ++ M) = length _|_ + length M
length (_|_     ) = _|_        + length M
_|_               = _|_

and similarly for M = _|_ and both _|_.

So this law holds even for infinite lists.

[1] Richard Bird, "Introduction to Functional Programming using
Haskell", p. 67

[2] http://en.wikipedia.org/wiki/Structural_induction

Also note that

>
> data Nat = Zero | Succ Nat deriving (Eq, Show)
>
> Take P(x) to be (x /= Succ x).
>
> P(0):
> Zero /= Succ Zero. (trivial)
>
> P(x) => P(Succ x)
>
> So, given P(x) which is: (x /= Succ x),
> we have to prove P(Succ x): (Succ x /= Succ (Succ x))
>
> In the derived Eq typeclass:
>    Succ a /= Succ b = a /= b
> Taking "x" for a and "Succ x" for b:
>    Succ x /= Succ (Succ x) = x /= Succ x
> which is P(x).
>
> Now, consider the following definition:
> infinity :: Nat
> infinity = Succ infinity
>
> infinity /= Succ infinity == _|_; and if you go by definitional
> equality, infinity = Succ infinity, so even though P(x) holds on all
> natural numbers due to structural induction, it doesn't hold on this
> infinite number.
>
>   -- ryan
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@...
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>

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