Program correctness in Discrete math

Question

Given a nonzero integer a and $b∈\Bbb N$, we want to compute $a^b$. Consider the following recursive algorithm $\operatorname{POW}(a,b)$.

If $b=0$, return $1$

Otherwise, if b is odd, return $a\cdot(\operatorname{POW}(a,\lfloor b/2\rfloor))^2$.

Otherwise (i.e., if $b>0$ and $b$ is even), return $(\operatorname{POW}(a,\lfloor b/2\rfloor))^2$.

And we want to prove that POW is correct. Namely, to prove that POW halts and returns $a^b$.

For the proof: Let $p(b)$ be the predicate $\operatorname{POW}(a,b)$ halts and returns $a^b$. It is easy to prove the base case which is: when $b=0$, we observe that $\operatorname{POW}(a,0)$ halts and returns $1$, which is equal to $a^0$. But I am not sure how to continue the inductive step.

Can somebody give me some hints?

Answer 1

Given a nonzero integer $a\in \Bbb N$ and $b∈\Bbb N_0$, we want to compute $a^b$. Consider the following recursive algorithm $\operatorname{POW}(a,b)$.

function POW(a,b):
    If b=0:
        return 1
    else if b is odd:
        return a*POW(a,[b/2])^2
    else (b is even):
        return POW(a,[b/2])^2

Proof by induction:

$\text{POW}(a,0)=1=a^0$, so $\text{POW}(a,b)=a^b$, if $b=0$

Assume we have already proved this for $b-1$. If $b$ is odd, then $b=2n+1$. Then we return $$\text{POW}(a)=a\cdot\text{POW}(a,[b/2])^2=a\cdot\text{POW}(a,n)^2=a\cdot (a^n)^2=a^{2n+1}=a^b$$ The equation $\text{POW}(a,n)=a^n$ holds because $n\le b-1$. If b is even, then $b=2n$. Then we return $$\text{POW}(a)=a\cdot\text{POW}(a,[b/2])^2=\text{POW}(a,n)^2=(a^n)^2=a^{2n}=a^b$$ Again the equation $\text{POW}(a,n)=a^n$ holds because $n\le b-1$.

---

A non recursive version of the algorithm is the following:

function POW(a,b):
    r:=1
    m:=a
    e:=b
    # r*m^e = a^b
    while e>=0:
        if e=0:
            # r*m^e = a^b
            return r
        else if e is odd:
            r:=r*m
            e:=e-1
            # r*m^e = a^b
        else if m is even:
            m:=m^2
            e:=e/2
            # r*m^e = a^b

# is a comment sign here. r*m^e is the loop invariant. It remains a^b after each step (check it!). So if e=0 and the function returns r, r is a^b.