Go backward to 5.2 Induction as a Proof TechniqueGo up to 5 Induction and RecursionGo 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

we would like to show that the formulaf:A->B

holds whereforallxinA: O(x,f(x))

aforallx:I(x) => O(x,f(x))

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

x^{0}:= 1,x^{n+1}:=x*x^{n}.

is indeed true for above definition.forallx,ninN:x^{n}= (prod_{1 <= i <= n}x).

Take arbitrary `x`; we proceed by induction over `n`.

We have `x`^{0} = 1 = (**prod**_{1 <= i <= 0} `x`) and
thus the induction base holds.

We take arbitrary `n` in **N** and assume

(1)We have to provex^{n}= (prod_{1 <= i <= n}x).

(2)We knowx^{n+1}= (prod_{1 <= i <= n+1}x).

which implies (2).

x^{n+1}= (definition exponentiation) x*x^{n}= (1) x* (prod_{1 <= i <= n}x)= (definition ( prod_{}))( prod_{1 <= 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(The corresponding implementation in the Logic Evaluatorx,y) :=suchzinN:z|x/\z|y/\ (forallw: (w|x/\w|y) =>w<=z).

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 **N**_{m} (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)forallminN,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) :=ifm= 0thennelse ifn= 0thenmelse ifn<=mthenEuclid(m-n,n)elseEuclid(m,n-m).

forallminN,ninN: (m!= 0 \/n!= 0) => Euclid(m,n) = gcd(m,n).

First we check that above equation defines a function

Euclid: Nat x Nat ->by constructing a termination termN

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) forallxinN,yinN:x+y<m+n=>( x!= 0 \/y!= 0) => Euclid(x,y) = gcd(x,y).

We assume (3) (

(2) ( m!= 0 \/n!= 0) => Euclid(m,n) = gcd(m,n).

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

`m`= 0.By (3), we have

`n`!= 0 and, by definition of `gcd' and `Euclid',gcd(

which implies (4).`m`,`n`) =`n`= Euclid(`m`,`n`)`m`!= 0 /\`n`=`0`.We have, by definition of `gcd' and `Euclid',

gcd(

which implies (4).`m`,`n`) =`m`= Euclid(`m`,`n`)`m`!= 0 /\`n`!=`0`/\`n`<=`m`.We know

which implies (4).gcd( `m`,`n`)= (0) gcd( `m`-`n`,`n`)= (1) Euclid( `m`-`n`,`n`)= (definition Euclid) Euclid( `m`,`n`)`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')which triggers the following recursive function definitionforallminN,n!= 0: gcd(m,n) = gcd(m,mmodn)

with induction term

Euclid'( m,n) :=ifm= 0thennelse ifn= 0thenmelse ifn<=mthenEuclid'(mmodn,n)elseEuclid'(m,nmodm)

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

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

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) :=ifn= 0thenmelseEuclid"(n,mmodn)

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