I am currently studying the Skiena `Algorithm Design Manual' and need a little help with a proof of correctness. The problem goes as follows:
Prove the correctness of the following algorithm for evaluating a polynomial.
$P(x)=a_nx^n+a_{n-1}x^{n-1}+\ldots+a_1x+a_0$function horner($A,x$)
- $p=A_n$
- for $i$ from $n-1$ to $0$
- $p=p*x+A_i$
- return $p$
It is intuitively obvious, that this algorithm gives the right result. But as I want a proof of correctness, I have to make sure this becomes obvious. My idea is proof by induction. We want to use, rigorously, that the inductive hypotheses is true up to and including step $n-1$.
To consider the algorithm, let $(a_i)_{i\in\mathbf{N}_0}$ be some sequence of real numbers and let $P$ be a function on $\mathbf{N}_0\times\mathbf{R}$ into $\mathbf{R}$ given by $$\forall (n,x)\in \mathbf{N}_0\times\mathbf{R} , \quad P(n,x)=\sum_{j=0}^n a_jx^j.$$
So let us consider the base case of $n=0$. This case is no problem, and the algorithm exites with $P(0,x)=a_0$ for all $x\in\mathbf{R}$.
Now, for the inductive step, assume the algorithm holds for all steps up to and including step $n-1$ for some arbitrary $n\in\mathbf{N}$. I want to express the iterative scheme symbolically, but of course, it is a nonsense to write $p=p*x+A_i$, since this just yields a function given by $p=A_i/(1-x)$ (when the division is well-defined). So I will give up the notation of the algorithm.
For this arbitrary $n$, what we want to show is that
$$\{[(a_nx+a_{n-1})x+a_{n-2}]x+\ldots\}x+a_0=\sum_{j=0}^n a_jx^j.$$
It is, as I said above, intuitively clear that this equation holds true, but I feel the left hand side is a bit too ambiguous. My problem is that I do not know how to express the left hand side of nested multiplication and summation in unambiguous notation (a product-operator and summation-operator). This is where I would like some help,
Thanks in advance
Best Answer
In arguing about the properties of algorithms involving a loop, it is often useful to think in terms of a loop invariant: something that you expect to be true after each iteration of the loop. Then, the principle is: if you have a loop where some proposition $P$ related to the current state is true before starting execution of the loop; and for each iteration of the loop, if before the loop body $P$ is true, then after the loop body $P$ is true; then, after the loop terminates, $P$ is still true.
In this algorithm, let us first expand the "for" statement a bit in order to simplify the analysis:
Then the loop invariant we will use is: $$p = \sum_{j=0}^{n-i} A_{n-j} x^{n-i-j} = A_n x^{n-i} + A_{n-1} x^{n-i-1} + \cdots + A_{i+1} x + A_i.$$ Just before the "while" statement starts executing, we indeed have $i = n$ and $p = \sum_{j=0}^0 A_{n-j} x^{n-i-j} = A_n$. Now, when executing the body, let us suppose at the start that $i = i_s$ and $p = A_n x^{n-i_s} + A_{n-1} x^{n-i_s-1} + \cdots + A_{i_s}$. (Here, $i_s$ will be used for the "start" value of $i$ in order to avoid confusion due to the changing value of $i$.) Then after the loop body executes, we will have $i = i_s - 1$ and $$p = (A_n x^{n-i_s} + A_{n-1} x^{n-i_s-1} + \cdots + A_{i_s}) x + A_{i_s-1} = \\ A_n x^{n-i_s+1} + A_{n-1} x^{n-i_s} + \cdots + A_{i_s} x + A_{i_s-1} = \\ A_n x^{n-i} + A_{n-1} x^{n-i-1} + \cdots + A_{i+1} x + A_i.$$ Therefore, the condition will indeed be preserved by each iteration of the loop. But then, after the loop exits, we will have $i = 0$, so $p = A_n x^n + A_{n-1} x^{n-1} + \cdots + A_1 x + A_0$ and the next "return" statement will return the correct value.
(Incidentally, if you're designing an algorithm, then the concept of loop invariant can also be useful in reverse: to come up with a description of exactly what state you want the variables to be in at the end of each execution of the loop body. Then keeping that in mind will aid in avoiding bugs that are due to "jumping the gun", so to speak, and prematurely performing calculations that really belong to the next iteration.)