ads The Invariant Relation Theorem

Section A.2 The Invariant Relation Theorem

Subsection A.2.1 Two Exponentiation Algorithms

Consider the following algorithm implemented in Sage to compute

a^{m} m o d n,

given an arbitrary integer

a,

non-negative exponent

m,

and a modulus

n,

n \geq 0 .

The default sample evaluation computes

2^{5} m o d 7 = 32 m o d 7 = 4,

but you can edit the final line for other inputs.

xxxxxxxxxx
 
def slow_exp(a,m,n):
    b=1
    k=m
    while k>0:
        b=(b*a)%n  # % is integer remainder (mod) operation
        k-=1
    return b
slow_exp(2,5,7)

🔗

It should be fairly clear that this algorithm will successfully compute

a^{m} (m o d n)

since it mimics the basic definition of exponentiation. However, this algorithm is highly inefficient. The algorithm that is most commonly used for the task of exponentiation is the following one, also implemented in Sage.

xxxxxxxxxx
 
def fast_exp(a,m,n):
    t=a
    b=1
    k=m
    while k>0:
        if k%2==1: b=(b*t)%n
        t=(t^2)%n
        k=k//2  # // is the integer quotient operation
    return b    
fast_exp(2,5,7)

🔗

The only difficulty with the "fast algorithm" is that it might not be so obvious that it always works. When implemented, it can be verified by example, but an even more rigorous verification can be done using the Invariant Relation Theorem. Before stating the theorem, we define some terminology.

🔗

Subsection A.2.2 Proving the correctness of the fast algorithm

🔗

Definition A.2.1. Pre and Post Values.

🔗

Given a variable

x,

the pre value of

x,

denoted

\overset{`}{x},

is the value before an iteration of a loop. The post value, denoted

\overset{´}{x},

is the value after the iteration.

Example A.2.2. Pre and post values in the fast exponentiation algorithm.

In the fast exponentiation algorithm, the relationships between the pre and post values of the three variables are as follows.

\overset{´}{b} \equiv \overset{`}{b} {\overset{`}{t}}^{\overset{`}{k} m o d 2} (m o d n)

\overset{´}{t} \equiv {\overset{`}{t}}^{2} (m o d n)

\overset{´}{k} = \overset{`}{k} / / 2

🔗

Definition A.2.3. Invariant Relation.

🔗

Given an algorithm’s inputs and a set of variables that are used in the algorithm, an invariant relation is a set of one or more equations that are true prior to entering a loop and remain true in every iteration of the loop.

Example A.2.4. Invariant Relation for Fast Exponentiation.

We claim that the invariant relation in the fast algorithm is

b t^{k} = a^{m} (m o d n) .

We will prove that this is indeed true below.

🔗

Theorem A.2.5. The Invariant Relation Theorem.

🔗

Given a loop within an algorithm, if

R

is a relation with the properties

🔗

R is true before entering the loop
the truth of R is maintained in any iteration of the loop
the condition for exiting the loop will always be reached in a finite number of iterations.

🔗

then R will be true upon exiting the loop.

Proof.

The condition that the loop ends in a finite number of iterations lets us apply mathematical induction with the induction variable being the number of iterations. We leave the details to the reader.

🔗

We can verify the correctness of the fast exponentiation algorithm using the Invariant Relation Theorem. First we note that prior to entering the loop,

b t^{k} = 1 a^{m} = a^{m} (m o d n) .

Assuming the relation is true at the start of any iteration, that is

\overset{`}{b} {\overset{`}{t}}^{\overset{`}{k}} = a^{m} (m o d n),

then

\begin{aligned} \overset{´}{b} {\overset{´}{t}}^{\overset{´}{k}} & \equiv (\overset{`}{b} {\overset{`}{t}}^{\overset{`}{k} m o d 2}) ({\overset{`}{t}}^{2})^{\overset{`}{k} / / 2} (m o d n) \\ \equiv \overset{`}{b} {\overset{`}{t}}^{2 (\overset{`}{k} / / 2) + \overset{`}{k} m o d 2} (m o d n) \\ \equiv \overset{`}{b} {\overset{`}{t}}^{\overset{`}{k}} (m o d n) \\ \equiv a^{m} (m o d n) \end{aligned}

🔗

Finally, the value of

k

will decrease to zero in a finite number of steps because the number of binary digits of

k

decreases by one with each iteration. At the end of the loop,

b = b t^{0} = b t^{k} \equiv a^{m} (m o d n)

🔗

which verifies the correctness of the algorithm.

🔗

Exercises A.2.3 Exercises

🔗

1.

🔗

How are the pre and post values in the slow exponentiation algorithm related? What is the invariant relation between the variables in the slow algorithm?

🔗

2.

🔗

Verify the correctness of the following algorithm to compute the greatest common divisor of two integers that are not both zero.

xxxxxxxxxx
 
def gcd(a,b):
    r0=a
    r1=b
    while r1 !=0:
        t= r0 % r1
        r0=r1
        r1=t
    return r0
gcd(1001,154)  #test

Hint.

The invariant of this algorithm is

g c d (r 0, r 1) = g c d (a, b) .

🔗

3.

🔗

Verify the correctness of the Binary Conversion Algorithm in Chapter 1.

🔗

4.

🔗

A dragon has 100 heads. A knight can cut off 15, 17, 20, or 5 heads, respectively, with one blow of his sword. In each of these cases 24, 2, 14, or 17 new heads grow on its shoulders, respectively. If all heads are blown off, the dragon dies. Can the dragon ever die? (problem attributed to Biswaroop Roy)

You have attempted of activities on this page.

Prev Top Next