Mathematical Induction

It seems to me that MathematicalInduction is simply what you get when you apply RefactorMercilessly to mathematics itself, in a loose mental concept sort of way. Here's how it goes:

1) Mathematics contains many constructive definitions of sets, which (e.g.) define the set of Foo in two parts:

2) Mathematics contains many constructive definitions of predicates (boolean functions) which (e.g.) discuss the predicate Burble in two parts:

Noticing the common behavior between these two methods leads us to conclude that Burble must be true for any Foo.

True Mathematicians will notice that I cheated in the first point above. There is usually a third clause, which says "Foo contains ONLY those elements that result from one of the two preceding rules." This allows the possibility that Burble is true for some things that are not in Foo, unless we can add a corresponding "but nothing else" clause to the definition of Burble, in which case we have shown that the predicate Burble selects exactly the elements of Foo.

As an application of this idea, consider that the NaturalNumbers are defined by the original PeanoPostulates? this way:

Similarly, we can show that 2m+1 is odd for all NaturalNumbers m by showing:

Having a soft spot for correctness arguments, I immediately see this as a way to show that a loop does what I intend, based on some fact that is invariant across the loop. (Pardon the fact that the example is in Perl... I don't know Smalltalk well enough to compose at the keyboard with confidence.)

 @somenums = (3, 4, 1, 7, 2, 9, 6);
 # I need to total the above numbers (yeah, trivial example!)

$total = 0; @temp = @somenums; # after 0 times thru the loop, $total + sum @temp = sum @somenums

while (@temp) { $total += shift @temp; # this preserves my invariant that $total + sum @temp = sum @somenums }

# on exit, @temp is empty, therefore sum @temp = 0 ... # therefore $total = sum @somenums
Now, of course, no practicing programmer would write it this way. This is exactly analogous to the fact that we begin in junior high algebra by writing each tiny step in detail, skipping the detailed steps only once we have satisfied ourselves (and our teacher) that we have mastered them. (And we can still make occasional mistakes trying to do too much at once!) Just as the experienced algebraist could have stated 2k+1 + 2 = 2(k+1) + 1 without needing the intermediate step above, the experienced programmer could have stated

 $total = 0;
 foreach (@somenums) {$total += $_}
without needing the explicit intermediate reasoning about @temp (assuming, of course that foreach is guaranteed to visit each element exactly once!)

-- JoelNeely


CategoryMath


EditText of this page (last edited May 25, 2008) or FindPage with title or text search