2
$\begingroup$

I have the following exponentiation routine, which takes $O(\log n)$ steps

function power(a:real, n:positive integer)
begin
  x:=1;
  i:=n;
  while i > 0 do
  begin
    if(i % 2 == 1) then   //i odd
      x:=x*a
    i:=floor(i/2)
    if(i > 0) then
      a:=a*a
  end;
  power:=x
end

I'm trying to prove that it always gives $a^n$. I think it might be provable via induction on $n$. in the examples i went through i found that it always ends with $i=1$ before the final division down to $0$.

$\endgroup$
  • 2
    $\begingroup$ So, what's the question? $\endgroup$ – Raphael May 24 '16 at 22:45
  • 2
    $\begingroup$ @Raphael Seems clear to me: how to prove that the final value of a is $a^n$ where $a$ is the initial value of a. (The code is either missing var in front of a:real or should be a function that ends by returning a.) $\endgroup$ – Gilles May 24 '16 at 23:25
  • 1
    $\begingroup$ @Gilles It's a problem dump with some narrative about an approach. Where exactly is miniparser stuck? What do they need to know? $\endgroup$ – Raphael May 24 '16 at 23:48
  • $\begingroup$ @Raphael Presumably stuck trying induction on $n$, which isn't an easy approach here. miniparser, you want a loop invariant; proving it will involve recursion on $i$. $\endgroup$ – Gilles May 24 '16 at 23:56
  • 2
    $\begingroup$ miniparser please state more clearly how your attempt failes or what do you expect. As Raphael stated there is no question, just statements what you are doing. @reuns your comment looks more like answer. $\endgroup$ – Evil May 25 '16 at 15:13
3
$\begingroup$

A standard approach to proving correctness of a program involving a loop is to use a loop invariant. Loop invariant $P(j)$ is a statement indexed by the iteration number $j$ (or a parameter related to the iteration number) that asserts a certain mathematical relationship between some variables appearing in your code. Proving $P(j)$ is true for all $j$ is typically done by induction. You show that $P(0)$ is true, i.e., the loop invariant is true prior to the beginning of the loop. You show that $P(i)$ is true implies $P(i+1)$ is true. Then you can conclude that the statement $P(n)$ (or $P(n+1)$) must be true, which asserts the relationship between the variables of interest that is directly relevant to the correctness of the algorithm. Note that if $j$ is some parameter related to the iteration number (e.g., $j$ could be $n$ minus the iteration number), the starting point and the direction of the induction might be different. Finding the right loop invariant is usually the hardest part.

Let's find a loop invariant for your code. Note that you overwrite the variable $a$ inside the loop. This means that I cannot use $a$ in the loop invariant to refer to the original input, but I'd like to. Therefore I introduce a new letter $\alpha$ to refer to the value of $a$ that is passed to the function, i.e., the first input. The rest of the variables are exactly as in your code. Our loop invariant $P(i)$ will be indexed by the variable $i$, which is related to the iteration number, but starts with $n$ and decreases to $0$ similar to what I wrote about above. Define the following loop invariant: $$P(i) \text{ is true if and only if } x*a^i == \alpha^n$$ Clearly, at the beginning you have $x=1$, $a=\alpha$, and $i = n$, so $P(n)$ is true. I leave proving the inductive step to you (note you will be proving $P(n)$ is true implies $P(\lfloor n/2 \rfloor)$ is true, so this induction skips over lots of values, but it's okay - why?). When the algorithm terminates you have $P(0)$, which asserts $x*a^0 = \alpha^n$, i.e., $x = \alpha^n$, which is what you needed to prove.

$\endgroup$
  • $\begingroup$ it's ok for the induction to skip over values of $n$ because the induction is on the number of times the loop executes. $\endgroup$ – miniparser Jun 21 '16 at 13:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.