Go backward to 5.3 Properties of Recursive DefinitionsGo 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.

Definition 68 (Inductive Set Definition) An inductive definition of a set S is a collection of formulas
 (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)
with object constant S and function constants f1, ..., fc which denote the  constructors (Konstruktoren) of 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

fi(T1, ..., Tmi, S1, ..., Sni)
for some terms T1, ..., Tmi, S1, ..., Sni where the S1, ..., Sni are also such constructor terms.

Example
• 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(e0, ..., cons(en-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(n0, node(n11, ...), node(n21, ...)),
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.
in the syntax of  BNF ( Backus Naur Form) that is used to describe  grammars (Grammatiken) of formal languages.

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

Definition 69 (Term Algebra) An inductively defined set is a  term algebra (Term Algebra) if we have for every constructor f of this set
 forall x, y: f(x) = f(y) => x = y
i.e., f is injective (injektiv). Furthermore, for all constructors f and g
 forall x, y: f(x) != g(y)
i.e., different constructors yield different results.

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

fi(T1, ..., Tmi, S1, ..., Sni)
for some terms T1, ..., Tmi, S1, ..., Sni where the S1, ..., Sni are also constructor terms. The name term algebra stems from this one to one correspondence between set elements and the terms that denote these elements.

Example  Because of the first two Peano axioms, N is a term algebra with constructors 0 and '.

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.

Example
• 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.

Proposition 67 (Structural Induction) In order to prove a property
forall x in S: F
for an inductively defined set S, it suffices to prove
 forall x1,...,xmi, y1 in S, ..., yni in S: (F[x := y1] /\  ... /\  F[x := yni]) => F[x := fi(x1,...,xmi, y1, ..., yni)]
for every constructor fi of S.

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

fi(x1,...,xmi, y1, ..., yni).
denoting some element x in S. We assume that F holds for every "S-component" yj of x and show that F is propagated to x itself.

Example  Take the set "List(T)" defined inductively as
 nil in List(T), forall e in T, l in List(T): cons(e, l) in List(T).
We define
 append: List(T) x List(T) -> List(T) append(nil, y) := y append(cons(e, x), y) := cons(e, append(x, y))
and claim that (for the function "length" defined in the previous example) the following holds:
 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).

Several formal concepts in computer science, e.g. datatypes and formal languages, can be reduced to inductively defined sets; the principle of structural induction is therefore of great importance.
Author: Wolfgang Schreiner
Last Modification: October 4, 1999