   Go up to 5 Induction and RecursionGo forward to 5.2 Induction as a Proof Technique ## 5.1 Inductive Definitions

We have introduced in Section 4.1 multiplication over N by the following recursive definition (with termination function r(x, y) := y)

 *: N x N -> N x * y := if y = 0 then 0 else x+(x*y-)

from which we can infer the following knowledge (Proposition Natural Number Operations)

 x * 0 = 0, x * y' = x+(x*y).

or in another form

 x * 0 = 0, x * (y+1) = x+(x*y).

Actually also the inverse is true: this pair of equations uniquely determines the function *: the first Peano law implies that the left hand side of only one equation "matches" a particular application a*b (because b is either 0 or y+1 for some y but not both) and the second Peano law implies that argument b determines the value of parameter y uniquely.

We can therefore write the definition also in the form

 *: N x N -> N x * 0 := 0, x * (y+1) := x+(x*y).

The syntactic properties of these equations guarantee that the corresponding function is well defined.

Definition 65 (Inductive Function Definition) An  inductive definition (induktive Definition) over N of an n-ary function f is a pair of equations
 f(x0, ..., 0, ..., xn-1) := Tb, f(x0, ..., xi+1, ..., xn-1) := Tr
where Tb (whose free variables are among x0, ..., xi-1, xi+1, ..., xn-1) is the  base term in which f does not occur and where every application of f in the  recursion term Tr (whose free variables are among x0, ..., xn-1) has the form
f(T0, ..., xi, ..., Tn-1)
for some terms T0, ..., Tn-1. We say that the induction runs over xi.

If there exist A0, ..., Ai-1, Ai+1, ..., An-1, B with

 forall x0 in A0, ..., xi-1 in Ai-1, xi in N, xi+1 in Ai+1, ..., xn-1 in An-1: Tb in B /\  Tr in B
then above definition introduces a function
f: A0 x ... x Ai-1 x N x Ai+1 x ... x An-1 -> B
such that the following holds:
 forall x0 in A0, ..., xi-1 in Ai-1, xi in N, xi+1 in Ai+1, ..., xn-1 in An-1: f(x0, ..., 0, ..., xn-1) = Tb /\ f(x0, ..., xi+1, ..., xn-1) = Tr.

A function introduced by an inductive definition is uniquely defined.

One can generalize inductive definitions in various ways. For instance, it is not necessary that the induction term is decreased by exactly 1. We may use any non-zero decrement value as long as every possible case is covered by a corresponding equation. For instance, in the definition of the  Fibonacci Numbers (Fibonacci-Zahlen)

 fib(0) := 1, fib(1) := 1, fib(x+2) := fib(x)+fib(x+1)
we have two base equations because in the last equation the induction term x is decreased by 2.

Furthermore, we may let the induction not just run over a single parameter but over a combination of parameters as in

 f(0, 0) := 0, f(x+1, 0) := 1+f(x, 0), f(x, y+1) := 1+f(x, y).

which defines a function that computes (in an artificially complex way) the sum of both arguments x and y. In this case, the induction is guarded by the  termination term x+y whose value is decreased by one in every recursive application of f.

If the induction runs over multiple arguments, we have to take special care that every possible argument pattern is covered by an equation. For instance, the definition

 f(0, 0) := 0, f(x+1, 0) := 1+f(x, 0), f(0, y+1) := 1+f(0, y), f(x+1, y+1) := 2+f(x, y),
uses four equations to cover all possible cases.

The more complicated the recursive structure of a function definition is, the more important it becomes to show that a set of equations indeed defines a total function. This can be done by giving a termination term or, more general, by constructing a well-founded ordering.

Example   Ackerman's function is defined as follows:
 A(0, y) := y+1, A(x+1, 0) := A(x, 1), A(x+1, y+1) := A(x, A(x+1, y)).
We have A: N×N -> N because we can construct the well-founded  lexicographic ordering (lexikographische Ordnung) on the function arguments
 x < y : <=> x0 < y0 \/ (x0 = x0 /\  x1 < y1)
(e.g. <0, 0> < <0, 1> and <0, 1> < <1, 0>) and show that the arguments decrease in every recursive application with respect to this ordering, i.e., for the three recursive applications in the equations above:
1. <x, 1> < <x+1, 0>,
2. <x+1, y> < <x+1, y+1>,
3. <x, A(x+1, y)> < <x+1, y+1>.
All three statements are true by definition of < .

Also predicates can be defined inductively.

Definition 66 (Inductive Predicate Definition) An inductive definition (Induktive Definition) over N of an n-ary predicate p is a pair of equivalences
 p(x0, ..., 0, ..., xn-1) : <=> Fb, p(x0, ..., xi+1, ..., xn-1) : <=> Fr
where Fb (whose free variables are among x0, ..., xi-1, xi+1, ..., xn-1) is the  base formula in which f does not occur and where every application of f in the  recursion formula Fr (whose free variables are among x0, ..., xn-1) has the form
p(T0, ..., xi, ..., Tn-1)
for some terms T0, ..., Tn-1. We say that the induction runs over xi.

Above definition defines a predicate

p subset A0 x ... x Ai-1 x N x Ai+1 x ... x An-1.
such that the following holds:
 forall x0 in A0, ..., xi-1 in Ai-1, xi in N, xi+1 in Ai+1, ..., xn-1 in An-1: (p(x0, ..., 0, ..., xn-1) <=> Fb) /\ (p(x0, ..., xi+1, ..., xn-1) <=> Fr).

A predicate introduced by an inductive definition is uniquely defined.

Example  We can introduce the predicate iseven(x) : <=> 2 | x also by the following recursive definition:
 iseven(0) : <=> T, iseven(x+1) : <=> ~iseven(x).
We can define the same predicate also in the following way with two base cases and an induction term x that is decreased by 2:
 iseven(0) : <=> T, iseven(1) : <=> F, iseven(x+2) : <=> iseven(x).

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   