previous up next
Go backward to 5.3 Properties of Recursive Definitions
Go up to 5 Induction and Recursion
RISC-Linz logo

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.


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.



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)
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

previous up next