Go backward to 5.2 Induction as a Proof Technique
Go up to 5 Induction and Recursion
Go forward to 5.4 Induction on Sets
|
Go backward to 5.2 Induction as a Proof Technique Go up to 5 Induction and Recursion Go forward to 5.4 Induction on Sets |
|
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 -> Bwe 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.
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.
We want to verify that the expected relationship
x0 := 1, xn+1 := x * xn.
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
which implies (2).
xn+1 = (definition exponentiation) x * xn = (1) x * (prod1 <= i <= n x) = (definition (prod )) (prod1 <= i <= n+1 x)
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.
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
which we claim to satisfy the specification
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).
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 -> Nby 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
We have to prove
(1) forall x in N, y in N: x+y < m+n => (x != 0 \/ y != 0) => Euclid(x, y) = gcd(x, y).
We assume (3) (m != 0 \/ n != 0) and prove (4) Euclid(m, n) = gcd(m, n).
(2) (m != 0 \/ n != 0) => Euclid(m, n) = gcd(m, n).
We have, according to the definition of `Euclid', four cases
By (3), we have n != 0 and, by definition of `gcd' and `Euclid',
gcd(m, n) = n = Euclid(m, n)which implies (4).
We have, by definition of `gcd' and `Euclid',
gcd(m, n) = m = Euclid(m, n)which implies (4).
We know
which implies (4).
gcd(m, n) = (0) gcd(m-n, n) = (1) Euclid(m-n, n) = (definition Euclid) Euclid(m, n)
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
with induction term m+n.
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)
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
which however requires the construction of an well-founded ordering of the arguments to show termination (please try).
Euclid"(m, n) := if n = 0 then m else Euclid"(n, m mod n)
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.