21.1 Induction and Coinduction

---

21.1 Induction and Coinduction

Assume we have fixed some universal set U as the domain of discourse for our inductive and coinductive definitions. U represents the set of "everything in the world," and the role of an inductive or coinductive definition will be to pick out some subset of U. (Later on, we are going to choose U to be the set of all pairs of types, so that subsets of U are relations on types. For the present discussion, an arbitrary set U will do.)

21.1.1 Definition

A function F Î P(U) → P(U) is monotone if X ⊆ Y implies F(X) ⊆ F(Y). (Recall that P(U) is the set of all subsets of U.)

In the following, we assume that F is some monotone function on P(U). We often refer to F as a generating function.

21.1.2 Definition

Let X be a subset of U.

1. X is F-closed if F(X) ⊆ X

2. X is F-consistent if X ⊆ F(X).

3. X is a fixed point of F if F(X) = X.

A useful intuition for these definitions is to think of the elements of U as some sort of statements or assertions, and of F as representing a "justification" relation that, given some set of statements (premises), tells us what new statements (conclusions) follow from them. An F-closed set, then, is one that cannot be made any bigger by adding elements justified by F-it already contains all the conclusions that are justified by its members. An F-consistent set, on the other hand, is one that is "self-justifying": every assertion in it is justified by other assertions that are also in it. A fixed point of F is a set that is both closed and consistent: it includes all the justifications required by its members, all the conclusions that follow from its members, and nothing else.

21.1.3 Example

Consider the following generating function on the three-element universe U = {a, b, c}:

•  

  E1(ø)	=	{c}	E1({a,b})	=	{c}
  E1 ({a})	=	{c}	E1({a,c})	=	{b,c}
  E1({b})	=	{c}	E1({b,c})	=	{a,b,c}
  E1({c})	=	{b,c}	E1({a,b,c})	=	{a,b,c}

There is just one E₁-closed set-{a,b,c}-and four E₁-consistent sets-ø, {c}, {b, c}, {a, b, c}.

E₁ can be represented compactly by a collection of inference rules:

Each rule states that if all of the elements above the bar are in the input set, then the element below is in the output set.

21.1.4 Theorem [Knaster-Tarski (Tarski, 1955)]

1. The intersection of all F-closed sets is the least fixed point of F.

2. The union of all F-consistent sets is the greatest fixed point of F.

Proof: We consider only part (2); the proof of part (1) is symmetric. Let C = {X | X ⊆ F(X)} be the collection of all F-consistent sets, and let P be the union of all these sets. Taking into account the fact that F is monotone and that, for any X Î C, we know both that X is F-consistent and that X ⊆ P, we obtain X ⊆ F(X) ⊆ F(P). Consequently, P = È_XÎC X ⊆ F(P), i.e. P is F-consistent. Moreover, by its definition, P is the largest F-consistent set. Using the monotonicity of F again, we obtain F(P) ⊆ F(F(P)). This means, by the definition of C, that F(P) Î C. Hence, as for any member of C, we have F(P) ⊆ P, i.e. P is F-closed. Now we have established both that P is the largest F-consistent set and that P is a fixed point of F, so P is the largest fixed point.

21.1.5 Definition

The least fixed point of F is written μF. The greatest fixed point of F is written vF.

21.1.6 Example

For the sample generating function E₁ shown above, we have μE₁ = vE₁ = {a, b, c}.

21.1.7 Exercise [⋆]

Suppose a generating function E₂ on the universe {a, b, c} is defined by the following inference rules:

Write out the set of pairs in the relation E₂ explicitly, as we did for E₁ above. List all the E₂-closed and E₂-consistent sets. What are μE₂ and vE₂?

Note that μF itself is F-closed (hence, it is the smallest F-closed set) and that vF is F-consistent (hence, it is the largest F-consistent set). This observation gives us a pair of fundamental reasoning tools:

21.1.8 Corollary [of 21.1.4]

1. Principle of induction: If X is F-closed, then μF ⊆ X.

2. Principle of coinduction: If X is F-consistent, then X ⊆ vF.

The intuition behind these principles comes from thinking of the set X as a predicate, represented as its characteristic set-the subset of U for which the predicate is true; showing that property X holds of an element x is the same as showing that x is in the set X. Now, the induction principle says that any property whose characteristic set is closed under F (i.e., the property is preserved by F) is true of all the elements of the inductively defined set μF.

The coinduction principle, on the other hand, gives us a method for establishing that an element x is in the coinductively defined set vF. To show x Î vF, it suffices to find a set X such that x Î X and X is F-consistent. Although it is a little less familiar than induction, the principle of coinduction is central to many areas of computer science; for example, it is the main proof technique in theories of concurrency based on bisimulation, and it lies at the heart of many model checking algorithms.

The principles of induction and coinduction are used heavily throughout the chapter. We do not write out every inductive argument in terms of generating functions and predicates; instead, in the interest of brevity, we often rely on familiar abbreviations such as structural induction. Coinductive arguments are presented more explicitly.

21.1.9 Exercise [Recommended, ⋆⋆⋆]

Show that the principles of ordinary induction on natural numbers (2.4.1) and lexicographic induction on pairs of numbers (2.4.4) follow from the principle of induction in 21.1.8.

---