Fibonacci and the greatest common divisor

fibonacci and the greatest common divisor

Let the function $f$ (from naturals to naturals) be given by

(0) ${f}{1}{0}^{ = }0,{f}{1} = 1,{f}{1}\left( {n + 2}\right) = {f}{1}\left( {n + 1}\right) + {f}_{1}n$

Then, $f$ application distributes over $\gcd$ , i.e.

(1) ${f}^{\prime }\left( {X\gcd Y}\right) = f \cdot X\gcd f \cdot Y$

Our interest is not in the above theorem, nor in its proofs. We wish to explore how we could design a proof for it.

We know the gcd for positive operands as the outcome of Euclid's Algorithm:

(2) ${x}{1}{y}{1} = {x}{2}{y}{2}$

$$ \begin{array}{l} ; \underline {{\underline {{d o}}}} x > y \rightarrow x := x - y \ [ y > x \rightarrow y = y - x \ \operatorname {o d} {x = X _ {\operatorname * {g c d}} Y ^ {j} \wedge y = X _ {\operatorname * {g c d}} Y } \ \end{array} $$

and this knowledge raises the question of

whether we can prove (1) by a properly

chosen invariant for program (2) which

Invariant, true before the repeatable

statement, allows us to conclude (1)

upon termination? We observe, starting

with the left-hand side of (1)

$$ \begin{array}{l} f. (X _ {g c d} Y) \ = {g c d i s i d e m p o t e n t: Z g c d Z = Z } \ f. (X _ {g c d} Y) g c d f. (X _ {g c d} Y) \ = {x = X _ {g c d} Y \wedge y = X _ {g c d} Y } \ f. x \quad g. c d \quad f. y \ = {(3), \mathrm {s e e} ^ {\mathrm {b e l o w}} } \ f. X \underset {g c d} {=} f. Y \ \end{array} $$

with the suggested invariant (3) given by

(3) ${f}{x}$ gcd ${f}{y} = {f}{x}$ gcd ${f}{z}$

Since (3) is obviously established by the initialization of (2), we only need to show that (3) is maintained by (2)'s repeatable statement, i.e. we have to show

$$ f. (x - y) \operatorname * {g c d} f. y = f. x \operatorname * {g c d} f. y \quad \mathrm {f o r} x > y \land y > 0 $$

or, more symmetrically written:

(4) $f \cdot a\;g \cdot d\;f \cdot b = f \cdot \left( {a + b}\right) \;g \cdot d\;f \cdot b\;\;f \cdot a > 0,b > 0.$

It is obviously time to take into account what has been given about $f$

The first step is to rewrite (0) a little bit more elegantly as

(5a) $\left( {{p}{0},{p}{1}}\right) = 0,1$ $\left( {5b}\right) \;\left( {f.}\left( {n + 1}\right) ,f.\left( {n + 2}\right) \right) = f.$

In terms of pairs of successive f-values, i.e. $p.n = \left( {{p}_{n},{f}^{\prime }\left( {n + 1}\right) }\right)$ ,these equations have

the form

$$ (6) \quad p. 0 = (0, 1), \quad p. (n + 1) = F. (p. n); $$

the advantage of (6) is that the introduc-tion of the function $F$ -from pairs of naturals to pairs of naturals- enables us to write the solution in closed form:

$$ p. n = F ^ {n} (0, 1) \quad . $$

In view of our remaining proof obligation (4), we shall now try to exploit the associativity of function composition, in particular

$$ F ^ {a + b} = F ^ {a} \circ F ^ {b}. \tag {7} $$

This exploitation requires that the specific shape of $F$ is taken into account. Writing p.n as column vector

$$ p. n = \begin{array}{l} f. n \ f. (n + 1) \end{array} , $$

we see from (5b) that $F$ application is translated into premultiplication by matrix

$$ F = \left| \begin{array}{l l} 0 & 1 \ 1 & 1 \end{array} \right| $$

from which

(8)

$$ F ^ {n} = \left| \begin{array}{l l} f _ {- 1} & f _ {- n} \ f _ {- n} & f _ {- (n + 1)} \end{array} \right| $$

follows (by mathematical induction).

Remark "Analytical extension" of (0) yields $f\left( {-1}\right) = 1$ . This value yields in (8) for ${F}^{0}$ the unit matrix,as it should.(End of Remark.)

With $F$ denoting a matrix, the o in (7) has to be interpreted as matrix multiplication; then, (7) and (8) yield - for the top-right element of ${F}^{a + b}$

$f\left( {a + b}\right) = f\left( {a - 1}\right) \cdot {f}_{1}b + f \cdot a \cdot f\left( {b + 1}\right)$

which contains all the terms occurring in (4), which has to be proved. To do so, we observe

$$ \begin{array}{l} f: (a + b) \mathrm {g c d} f. b \ = {(g) } \ (f. (a - 1) \cdot f. b + f. a \cdot f. (b + 1)) \mathrm {g c d} f. b \ = {\mathrm {p r o p e r t h y o f} g c d } \ (f \cdot a \cdot f. (b + 1)) \cdot a c d f \cdot b \ = {\mathrm {l e m m a} 0, \mathrm {b e l o w}, \mathrm {w i t h} n := b; \mathrm {p r o p e r t y} \mathrm {g c d} } \ f. a \quad g. c d \quad f. b \ \end{array} $$

$$ \mathrm {L e m m a 0} \quad \mathrm {f . n . g c d} \quad \mathrm {f . (n + 1)} = 1. $$

For $n = 0$ ,the lemma follows from the definition of $f.0$ and ${f}{1}$ . For larger values of $n$ ,it follows from Euclid's Algorithm with ${X}{1}{Y}{1} = {P}{n},{P}_{\left( n + 1\right) }$ . On account of the last definition in (0)

$$ (\underline {{E}} m: m > 0: {x, y } = {f _ {m}, f _ {(m + 1)} }) $$

is then an invariant of the algorithm.

The transition from (0) to (5) could strike one as a rabbit, but it isn't for someone who has seen a little bit more. It underlies one of the oldest examples of program transformation -from the pen of R.M. Burstall; it is quite common wherever functional composition plays a significant role -functional programming, constructive type theory, or category theory, just to mention a few-. I am more surprised by the very different ways in which the gcd enters the picture.

Austin, 9 April 1990

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 USA