Go up to 5 Induction and Recursion
Go forward to 5.2 Induction as a Proof Technique
|
Go up to 5 Induction and Recursion Go forward to 5.2 Induction as a Proof Technique |
|
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.
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(x0, ..., 0, ..., xn-1) := Tb, f(x0, ..., xi+1, ..., xn-1) := Tr
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
then above definition introduces a function
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
f: A0 x ... x Ai-1 x N x Ai+1 x ... x An-1 -> Bsuch 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)
we have two base equations because in the last equation the induction term x is decreased by 2.
fib(0) := 1, fib(1) := 1, fib(x+2) := fib(x)+fib(x+1)
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
uses four equations to cover all possible cases.
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),
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.
We have A: N×N -> N because we can construct the well-founded lexicographic ordering (lexikographische Ordnung) on the function arguments
A(0, y) := y+1, A(x+1, 0) := A(x, 1), A(x+1, y+1) := A(x, A(x+1, y)).
(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:
x < y : <=> x0 < y0 \/ (x0 = x0 /\ x1 < y1)
Also predicates can be defined inductively.
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(x0, ..., 0, ..., xn-1) : <=> Fb, p(x0, ..., xi+1, ..., xn-1) : <=> Fr
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).
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(x+1) : <=> ~iseven(x).
iseven(0) : <=> T, iseven(1) : <=> F, iseven(x+2) : <=> iseven(x).