Inductive principles
Matthew Hennessy · Cambridge University Press eBooks · 2007
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 1 , M 2 ∈ S implies M 1 + M 2 ∈ 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 1 + M 2 | = | M 1 | + | M 2 |. 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.