In this chapter I will introduce a powerful proof technique based on mathematical induction. With it we will be able to prove complex and important properties of programs that cannot be accomplished with proof-by-calculation alone. The inductive proof method is one of the most powerful and common methods for proving program properties.
Induction and Recursion
Induction is very closely related to recursion. In fact, in certain contexts the terms are used interchangeably; in others, one is preferred over the other primarily for historical reasons. I like to think of them as being duals of each other: Induction is used to describe things starting with something very simple, and building up from there, whereas recursion describes the whole thing first, working backward to the simple case.
For example, although I have previously used the phrase recursive data type, in fact data types are often described inductively, such as a list:
A list is either empty, or it is a pair consisting of a value and another list.
On the other hand, we usually describe functions that manipulate lists, such as map and foldr, as being recursive. This is because when you apply a function such as map, you apply it initially to the whole list, and work backwards toward [ ]. But these differences between induction and recursion run no deeper: They are really just two sides of the same coin.
This chapter is about inductive properties of programs (but based on the above argument could just as rightly be called recursive properties) that are not usually proven via calculation alone. Proving inductive properties usually involves the inductive nature of data types and the recursive nature of functions defined on the data types.
As an example, suppose that P Is an inductixe property of a list. In other words, P(l) for some list l is either true or false (no middle ground here!), To prove this property inductively, we do so based un the length of the list: Starting with length 0, we first prove P([]), (using our standard method of proof-by-calculation).
Review the options below to login to check your access.
Log in with your Cambridge Aspire website account to check access.
If you believe you should have access to this content, please contact your institutional librarian or consult our FAQ page for further information about accessing our content.