Go backward to 5.2 Induction as a Proof TechniqueGo up to 5 Induction and RecursionGo forward to 5.4 Induction on Sets

## 5.3 Properties of Recursive Definitions

The close relationship between inductive definitions and induction as a proof strategy makes it natural that the same method can be applied to  verify (verifizieren) the correctness of inductively/recursively defined functions. Given the definition of a function

f: A -> B
we would like to show that the formula
forall x in A: O(x, f(x))
holds where O is a binary predicate which expresses the desired relationship between input x and output f(x). A more general statement of the problem is given below.

Definition 67 (Specification) For every function f: A -> B, a relation I subset A and a relation O subset A x B, we call the formula
forall x: I(x) => O(x, f(x))
a  specification (Spezifikation) of function f with  input condition (Eingabebedingung) I and  output condition (Ausgabebedingung) O.

If the domain of a function parameter is N, then the verification may proceed by induction over this parameter.

Example  Take the exponentiation function:
 x0 := 1, xn+1 := x * xn.
We want to verify that the expected relationship
forall x, n in N: xn = (prod1 <= i <= n x).
is indeed true for above definition.

Take arbitrary x; we proceed by induction over n.

We have x0 = 1 = (prod1 <= i <= 0 x) and thus the induction base holds.

We take arbitrary n in N and assume

(1) xn = (prod1 <= i <= n x).
We have to prove
(2) xn+1 = (prod1 <= i <= n+1 x).
We know
 xn+1 = (definition exponentiation) x * xn = (1) x * (prod1 <= i <= n x) = (definition (prod )) (prod1 <= i <= n+1 x)
which implies (2).

The usual purpose of verification is to show that a particular definition of a function matches a specification that is defined in a more abstract away; the function definition can be thus considered as an  implementation of the specification. While the specification may be inconstructive (i.e., it does not directly yield an algorithm that can be implemented on a computer) or constructive but algorithmically inefficient, the implementation is more concrete and/or more efficient.

The proof that an implementation matches the specification typically requires the derivation of additional mathematical knowledge; more knowledge yields better algorithms.

Example  We have defined the greatest common divisor as
gcd(x, y) := such z in N: z | x /\  z | y /\  (forall w: (w | x /\  w | y) => w <= z).
The corresponding implementation in the Logic Evaluator
```fun gcd(x, y) =
let(m = if(=(x, N0), y, x):
such(z in nat(N0, m):
and(divides(z, x), divides(z, y),
forall(w in nat(+N(z, N1), m):
or(not(divides(w, x)), not(divides(w, y))))),
z));
```

is very inefficient because it tests every z in Nm (for some m) whether it is a divisor of the arguments and if it is the greatest such divisor.

Now we may realize (as the Greek mathematician Euclid did) that the following property holds:

(0) forall m in N, n <= m: gcd(m, n) = gcd(m-n, n).

Based on this knowledge, we may define the following function

 Euclid(m, n) := if m = 0 then n else if n = 0 then m else if n <= m then Euclid(m-n, n) else Euclid(m, n-m).
which we claim to satisfy the specification
forall m in N, n in N: (m != 0 \/ n != 0) => Euclid(m, n) = gcd(m, n).

First we check that above equation defines a function

Euclid: Nat x Nat -> N
by constructing a termination term m+n (and check that it is appropriately decreased in every recursive application).

Second we verify that this function meets the specification by complete induction on the term m+n: we take arbitrary m in N and n in N and assume

 (1) forall x in N, y in N: x+y < m+n => (x != 0 \/ y != 0) => Euclid(x, y) = gcd(x, y).
We have to prove
 (2) (m != 0 \/ n != 0) => Euclid(m, n) = gcd(m, n).
We assume (3) (m != 0 \/ n != 0) and prove (4) Euclid(m, n) = gcd(m, n).

We have, according to the definition of `Euclid', four cases

1. m = 0.

By (3), we have n != 0 and, by definition of `gcd' and `Euclid',

gcd(m, n) = n = Euclid(m, n)
which implies (4).
2. m != 0 /\  n = 0.

We have, by definition of `gcd' and `Euclid',

gcd(m, n) = m = Euclid(m, n)
which implies (4).
3. m != 0 /\  n != 0 /\  n <= m.

We know

 gcd(m, n) = (0) gcd(m-n, n) = (1) Euclid(m-n, n) = (definition Euclid) Euclid(m, n)
which implies (4).
4. m != 0 /\  n != 0 /\  n not  <= m.

The proof is analogous to the previous case.

Thus we have shown that `Euclid' indeed computes the `gcd' (in an algorithmically much more efficient way than suggested by the definition of `gcd').

From (0) we can derive the even more powerful property

(0') forall m in N, n != 0: gcd(m, n) = gcd(m, m mod n)
which triggers the following recursive function definition
 Euclid'(m, n) := if m = 0 then n else if n = 0 then m else if n <= m then Euclid'(m mod n, n) else Euclid'(m, n mod m)
with induction term m+n.

The proof that this (algorithmically even more efficient) function also meets the specification

forall m in N, n in N: (m != 0 \/ n != 0) => Euclid'(m, n) = gcd(m, n).
is similar to the proof given above.

One can give an algorithmically (essentially) equivalent but shorter definition

 Euclid"(m, n) := if n = 0 then m else Euclid"(n, m mod n)
which however requires the construction of an well-founded ordering of the arguments to show termination (please try).

A definition of  Euclid's algorithm (Euklidscher Algorithmus) in the Logic Evaluator is given above. With larger input values, one soon notices the difference to the efficiency of the naive implementation of the gcd.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999