1 - Inductive principles

Summary

Throughout the book we will make extensive use of both induction and coinduction, and their associated proof techniques. Here we give a brief review of these concepts, and an indication of how we intend to use them.

Induction

Figure 1.1 contains a definition of the (abstract) syntax of a simple language of machines. Here a ranges over some set of action labels Act, and intuitively a machine can carry out sequences of these actions, and periodically has a choice of which actions to perform. Let M be the set of all machines defined in Figure 1.1. Formally this is an inductive definition of a set, namely the least set S that satisfies

• stop ∈ S

• M ∈ S implies a.M ∈ S for every action label a in Act

• M₁, M₂ ∈ S implies M₁ + M₂ ∈ S.

The fact that M is the least set that satisfies these conditions gives us a proof technique for defining and proving properties of machines in M; any other set satisfying the conditions is guaranteed to contain M.

As an example consider the following definition of the size of a machine:

• |stop| = 0

• |a.M| = 1 + |M|

• |M₁ + M₂| = |M₁| + |M₂|.

We know by induction that this function is now defined for every machine. Belabouring the point for emphasis let D be the domain of the size function | |, the set of elements for which it is defined.