Go backward to 5.3 Properties of Recursive Definitions Go up to 5 Induction and Recursion

5.4 Induction on Sets

The concept of induction is not limited to N; it can be applied to any set whose construction is based on a corresponding principle.

(forall x1,...,xm1, y1 in S, ..., yn1 in S:

f1(x1, ..., xm1, y1, ..., yn1) in S)

, ... ,

(forall x1,...,xmc, y1 in S, ..., ync in S:

fc(x1, ..., xmc, y1, ..., ync) in S)

By this definition, S denotes the smallest set on which the conjunction of these formulas holds.

The notion "smallest" used in above definition implies that every element of the defined set is denoted by a constructor term

f_i(T₁, ..., T_mi, S₁, ..., S_ni)

• The set N is inductively defined by

  0 in N,

  forall x in N: x' in N

  for some constructors 0 and '. Every element of N is of the form

  0'^...',

  e.g. 0'''' is interpreted as the number 4 in N.
• For every set T, the set "List(T)" is defined by

  nil in List(T),

  forall e in T, l in List(T): cons(e, l) in List(T).

  for some constructors "nil" and "cons". Every element of List(T) is of the form

  cons(e₀, ..., cons(e_n-1, nil)),

  e.g. "cons(2, cons(3, nil))" is interpreted as the list [2, 3] in List(N).
• For every set T, the set "Tree(T)" is defined by

  empty in Tree(T),

  forall e in T, l in Tree(T), r in List(T): node(e, l, r) in Tree(T).

  for some constructors "empty" and "tree". Every element of Tree(T) is of the form

  node(n₀, node(n₁₁, ...), node(n₂₁, ...)),

  e.g. "node(1, node(2, node(3, empty, empty), node(4, empty, empty)), node(5, empty, empty))" is interpreted as the following tree in Tree(N):

  1
  2       5
  3   4          

• The set "Term" is defined by

  0 in Term,

  1 in Term,

  forall x in Term: -x in Term,

  forall x in Term, y in Term: x+y in Term,

  forall x in Term, y in Term: x*y in Term

  for some constructors 0, 1, -, +, *. An element of "Term" is "1+(1+0)*1".
• The set "Formula" is defined by

  T in Formula

  forall x in Formula: not(x) in Formula,

  forall x in Formula, y in Formula: and(x, y) in Formula,

  forall x in Variable, y in Formula: forall(x, y) in Formula

  for some constructors "T", "not", "and", "forall". An element of "Formula" is "forall(X, and(T, or(T, F)))" (assuming X in "Variable").

Inductive set definitions may appear in various notations; e.g., the set "Term" in above example is more conveniently defined as

Term ::= 0 | 1 | -Term | Term+Term | Term*Term.

We now constrain our notion of inductive sets such that the elements preserve "knowledge" about their construction.

forall x, y: f(x) = f(y) => x = y

forall x, y: f(x) != g(y)

Every element of a term algebra is denoted by one and only one constructor term

f_i(T₁, ..., T_mi, S₁, ..., S_ni)

A nice property of a term algebra is that they allow inductive function and predicate definitions in the style of inductive definitions over N; we do not introduce these definitions formally but give some examples.

• Take the set List(T) defined in the previous example and assume that it is a term algebra. We define the length of a list as

  length: List(T) -> N

  length(nil) := 0

  length(cons(e, l)) := 1+length(l).

  Then we have length(cons(1, cons(2, nil))) = 2.
• Take the set List(T) defined in the previous example and assume that it is a term algebra. We define the depth of a tree as

  depth: Tree(T) -> N

  depth(empty) := 0

  depth(node(n, l, r)) := 1+max(depth(l), depth(r)).

  Then we have depth(node(1, empty, node(2, node(3, empty, empty), empty))) = 3.
• Take the set Term defined in the previous example and assume that it is a term algebra. We define the value of a term as

  value: Term -> N

  value(0) := 0N

  value(1) := 1N

  value(-x) := -Nvalue(x)

  value(x+y) := value(x)+Nvalue(y)

  value(x*y) := value(x)*Nvalue(y)

  Then we have value(1+(1+0)*1)=2.

On inductively defined sets (not necessarily term algebras) we have the following induction principle.

forall x in S: F

forall x1,...,xmi, y1 in S, ..., yni in S:

(F[x := y1] /\  ... /\  F[x := yni]) =>

F[x := fi(x1,...,xmi, y1, ..., yni)]

Intuitively, we let the induction run over the "structure" of every term

f_i(x₁,...,x_mi, y₁, ..., y_ni).

nil in List(T),

forall e in T, l in List(T): cons(e, l) in List(T).

append: List(T) x List(T) -> List(T)

append(nil, y) := y

append(cons(e, x), y) := cons(e, append(x, y))

forall x in List(T), y in List(T):

length(append(x, y)) = length(x)+length(y).

We proceed by structural induction on x:

Case x=nil:

We have to show

forall y in List(T):

length(append(nil, y)) = length(nil)+length(y).

Take arbitrary y in List(T). We have

length(append(nil, y))	=	(definition append)
length(y)	=
0+length(y)	=	(definition length)
length(nil)+length(y).

Case x=cons(e, l):

Take arbitrary e in T and l in List(T).

We assume (induction hypothesis)

forall y in List(T):

length(append(l, y)) = length(l)+length(y)

and have to show

forall y in List(T):

length(append(cons(e, l), y)) = length(cons(e, l)) +length(y).

Take arbitrary y in List(T). We have

length(append(cons(e, l), y))	=	(definition append)
length(cons(e, append(l, y)))	=	(definition length)
1 + length(append(l, y))	=	(induction hypothesis)
1 + (length(l) + length(y))	=
(1 + length(l)) + length(y)	=	(definition length)
length(cons(e, l)) + length(y).