Chapter 3
Reasoning about programs

Aims

• To show how properties of functions and other Miranda objects can be proved using elementary techniques of logic.
• In particular, the chapter introduces proof by induction over the natural numbers; `mathematical induction' in other words.

Issues

Relevance

It is an important fact that functional programs are more amenable to verification than most imperative programs, and it is therefore somewhat simpler to introduce verification in a functional setting. The thread on proof through the book can be treated as optional, but it has been included as an integral part of the text because I see it as central to learning functional programming.

Strategies for teaching proof

Proof is hard to teach; the ground rules for writing proofs are less clearly defined than for a programming language, and induction in particular looks circular to many students. There seems to be no `silver-bullet' explanation, but a number of ideas help:

• Simplification of expressions involving variables works in exactly the same way as calculation. For the direct proofs at the start of the chapter, this is really all that is needed.
• Induction is like recursion. A familiarity with recursive definitions, and the conviction that they work, can help in convincing students that induction is not circular. The view of the proof as a machine turning proofs into proofs can also help.
• Proving the induction step involves making an assumption; examining particular examples of chains of reasoning involving real world assumptions can convince that they are different than proofs without assumptions.
• To tighten up on the mechanics of proof, three points are important:
  • Keeping the variables in the definition and the proof different makes it clearer when substitutions in the definition take place.
  • Providing a template for proofs forces students to be clear about the sub-goals that induction produces; in particular this is helpful when a formula contains more than one variable.
  • If the (sub-)goal is to prove an equation, a sensible strategy is to simplify (like calculation, as above) both sides, and try to get a common result. It is important to check whether the induction hypothesis has been used, when appropriate.

Next Up