I've been reading about polynomials lately and found that the polynomial division algorithm is a great example of a real algorithm that can be proved correct, and where a proof actually provides some insight in to how the algorithm works.
First lets get some notation out of the way: A polynomial, say , over a field is a formal sum:
are all polynomials.
The set of all polynomials in variable over a field is denoted .
I assume that if you are reading this you are familiar with the rules for polynomial addition, subtraction and multiplication, and that you know what the degree of a polynomial is, and what a monomial is.
The polynomial division algorithm
The polynomial division problem is: given with find such that:
We need to add the extra possibility because the degree of the zero polynomial is undefined.
An algorithm that can compute and is:
Input: , ,
while and :
The proof of correctness
We will break the proof up into 2 parts
- If the algorithm terminates it produces the correct result
- The algorithm always terminates
Proving the algorithm is correct when it terminates
First lets address part 1: proving that if the algorithm terminates it produces the correct result. This problem in turn will be broken into two parts
- First we prove that at the start of the while loop and after every iteration of the loop: . The statement is the loop invariant
- Second we prove that if the loop terminates or
Proving that the invariant holds
At the start of the loop:
Now we need to show that if on entry to the while loop, then it is true after one execution of the loop. To do this we need to introduce new variables to represent the values of and before and after the loop executes.
Lets call the values of and on entry to the loop and , and the values after execution of the loop and .
So assuming , we need to show that after the execution of the loop .
Looking at the body of the loop we can see that:
Proving the degree condition
Now we need to prove that if the loop terminates:
We split this up into two cases: an . If then we are done. If we have a little more work to do.
Looking at the loop we can see that the only way it will terminate is if
So we need to prove that
This is actually pretty straightforward. By definition of the leading term of a polynomial we know:
So by construction the term: is the result of dividing by . , if and only if this term is not defined.
There are only 2 ways the monomial could be undefined: either , or , but remember that the division algorithm assumes that , so it must be that:
Which is equivalent to the statement:
Which is exactly what we set out to prove! Now we know that if the algorithm terminates it produces the correct quotient and remainder.
Producing the correct result when the algorithm stops is great, but does it always stop? Yes. The outline of why is below:
- Initially or
- When or the algorithm terminates
- After every iteration of the loop either the degree of decreases or becomes zero.
The first statement follows from the definition of the degree of a polynomial. The degree of a polynomial is non-negative if it is defined, and is undefined for the zero polynomial.
The second statement follows straight from the algorithm itself. A program with no loops always terminates, and this program has only one loop, so if that loop terminates the program is guaranteed to terminate, and or is just saying that the loop condition is not met.
Proving that statement 3 is more involved. Lets suppose that the value of going into the loop is and the value after an iteration is . Then by definition:
So we need to prove that either:
Without loss of generality we can rewrite as:
With this rewrite we can see that:
Now we have a few cases to consider. First lets suppose that: , , and .
Then by the properties of polynomial degree we know that:
By definition , and .
Now suppose without loss of generality that :
But since we know:
Since we are in the body of the loop we know that so , so:
So and . It follows that:
So the degree of reduces after each step.
That resolves the most complicated case. Now lets take a look at the others: first suppose that . Since so statement 3 is true and we are done.
If either or