Making induction meaningful

Question

I've been teaching inductive proofs of code correctness to high school students for three years now, and the instruction has steadily improved. Many of the students come in not having done inductive proofs in math yet, so it takes some time to teach this.

As of this year, the large majority of my students are writing virtually 100% correct proofs for algorithms that they have never seen before. However, this takes a large amount of class time (many weeks), and it has become a box-ticking exercise that the students are not excited by. This is certainly not what I want.

Here are a list of some of my personal favorite takeaways from this unit:

• You are proving an infinite number of things using a finite amount of ink.
• We normally conceptualize our variables as just that: variable. But really, they are a cascading series of constants, and the reality is that the runtime program goes sliding through these constants. We can designate these constants using subscripts. If you have a for loop in which i increments from 0 to 50, $i_0$ is always 0, and $i_1$ is always 1. They're not truly variable. It's a subtle distinction, but I find it beautiful, and I also believe that it is a nice lead-in to that aspect of functional programming.
• We can make real guarantees about code in the first place.

This list has been thus-far unconvincing to my students. I need to make this unit more exciting. How do I demonstrate to my students that this is both interesting and beautiful?

Answer 1

Since you are doing this in the context of code correctness, one incentive is to tell student that in some cases, you have to prove code, not test it. Anything critical (pick up your example, nuclear plant command system, plane autopilot, …) requires the highest level of confidence. Tests are always going to be partial. They will test 1, 10, 1000 possible inputs but that's it. You need to show that your program behaves well for all possible input.

Since many programs work by splitting their large input into smaller cases, proofs by induction are a good fit. It also gives a high degree of confidence since often, the structure of the proof will follow the program step by step (while a proof by contradiction would only be remotely related to the code).

You can also show that often, a proof by induction will give you an actual program. The basic toy example is the one of the Tower of Hanoi (where you have three pegs and N discs). The proof of the theorem stating "it takes 2^N moves" is actually the recursive algorithm that implements the moves (and you can make an animated version of the algorithm in JS or something to make it visual).

Another example is quicksort. Give the code of quicksort. The (strong) induction proof of correctness has the exact same structure has the code. You can use several divide and conquer algorithms for this (Binary search also works very well AND is really cool because you can also show another issue with proof of code : Most 'student' implementation of binary search are buggy, since they tend to write middle = (left + right)/2 which will overflow for large arrays (where left+right > max_int). This bug was present in the Java standard library. So you also have to talk about the mathematical model of the program (used for proofs, where you have potentially infinite memory, Natural numbers) and the program (fixed size integer, limited, memory, …).

Answer 2

I try to introduce induction not only as method for proving an algorithm, but as a method for developing algorithms as well. The idea is from Introduction to Algorithms by Udi Manber.

Sometimes the way of thinking

• solve the problem for n=1
• think about how you can calculate (n+1) once you know n

helps them to develop solutions on their own. And it helps with understanding recursion as well ;-).

Fun fact: Around Christmas I given them the following assignment: Why does this inductive "proof" not work in real life:

Hypothesis: I need only one match to light all candles in a very large christmas tree. Proof:

• n = 1; I can light one candle using the match.
• n --> (n+1): I move the match to the next candle and light this candle

Answer 3

This isn't really an answer, but I hope will provide a bit of insight for the OP into thinking about and presenting the problem.

I think that recursion (in computing) and induction (in mathematics) are complementary, not identical ideas. The interplay between the two can give insight.

In mathematical induction, we normally work outward from the base case. For example, in an inductive definition, you first establish (for example) that 1 is a Natural Number. You then define the inductive case(s) based on that. So, the general case is valid because you can work forward, through a finite number of steps, until you reach the case for, say 42.

In programming recursion, we work and think in the other direction. While we may state or prove the base case first, the program written for the general case(s) work inward toward that base. We write a solution of a more complex case in terms of known or assumed solutions for the simpler case(s).

I hope I'm not being overly subtle here, and admit that it may be just a personal way of thinking, but I find it helpful. In induction, we start at the base and work outward until we are stopped by a more complex case (42). In recursion we start with the complex case and work backwards until we are stopped by the base case. In both we need an argument of finiteness, of course, but they seem subtly different to me.

Since this is just an insight, not an answer, I've marked it as community owned.