Variants
May 142018An algorithm is correct if it always returns the correct result.
Assertions are our main tool for proving algorithms are correct; they state that some condition will be true whenever a particular line of code is reached. The goal is to assert that, when the algorithm finishes running, the result is correct. If this assertion never fails, then the algorithm will never return a wrong result.
An unfortunate problem
Consider the following sorting algorithm; assume the is_sorted
function tests whether lst
is sorted or not.
def infinite_loop_sort(lst):
while not is_sorted(lst):
# do nothing
pass
This loop does nothing! Certainly, it makes no progress towards sorting the list. Yet we can be absolutely sure it never returns a wrong result, because it never returns a result at all!
This is really a problem.
If we write a return
statement, and assert
that the result is correct, the techniques we developed in the previous post actually allow us to “prove” that this clearly incorrect algorithm is “correct”:
def infinite_loop_sort(lst):
while not is_sorted(lst):
# do nothing
pass
assert is_sorted(lst)
return lst
The “proof” is as follows.
At the end of the loop, the assertion cannot fail, because if is_sorted(lst)
is false, the loop would not have stopped.
So, the algorithm never returns a wrong result.
Termination
What we want to prove is that the algorithm always returns a correct result. But assertions only let us say that if the algorithm returns a result, then the result will be correct.(1)
We also need to prove that the algorithm will return a result at all — i.e. that it will eventually terminate, or finish running. In this post, we’ll explore the idea of variants, which are needed to prove that algorithms terminate. The good news is that variants are simpler and easier to use than invariants.
Analogy
In the game of chess, a pawn can only move forwards. If you keep moving the same pawn, eventually it must reach the end of the board.
The y coordinate gets smaller on every move, so it must eventually reach 0. This proves that the pawn will reach the end of the board in finitely many moves — it can’t get stuck in an “infinite loop”.
In other words, the y coordinate is a variant.
Example: factorial
The following algorithm computes the factorial of n
:
def factorial(n):
if n < 0:
raise ValueError('n must not be negative')
r = 1
while n > 0:
r *= n
n -= 1
return r
In this loop, n
is a variant — it gets smaller on each iteration, and the loop stops when n
is 0.
Therefore, this algorithm will always terminate.
Example: insertion sort
Consider the insertion sort algorithm.
def insertion_sort(lst):
n = len(lst)
for i in range(n):
j = i
while j > 0 and lst[j-1] > lst[j]:
tmp = lst[j]
lst[j] = lst[j-1]
lst[j-1] = tmp
j -= 1
The inner while loop must terminate, because j
gets smaller on each iteration, and the loop terminates when j
is 0.
If the other condition lst[j-1] > lst[j]
is false, then the loop might terminate sooner — but it will terminate.
So, j
is a loop variant.
Example: exponentiation
In the previous post we proved that the following algorithm never returns a wrong result:
def power(x, n):
if n < 0:
raise ValueError('n must not be negative')
r = 1
i = 0
while i < n:
r *= x
i += 1
return r
Let’s also prove that the loop must terminate.
This example is a bit different, since there is no variable “counting down”, and the loop stops when i
reaches n
, not when something reaches 0.
This loop terminates because i
keeps getting bigger, so it must eventually reach n
.
Put another way, the difference n - i
keeps getting smaller.
For example, consider the trace from computing power(3, 4)
:
n | i | n - i |
---|---|---|
4 | 0 | 4 |
4 | 1 | 3 |
4 | 2 | 2 |
4 | 3 | 1 |
4 | 4 | 0 |
The expression n - i
gets smaller on every iteration, because i
gets bigger but n
stays the same.
When n - i
reaches 0, the condition i < n
becomes false and so the loop terminates.
So, n - i
is a loop variant.
Example: binary search
Consider the binary search algorithm:
def binary_search(lst, target):
left = 0
right = len(lst) - 1
while left <= right:
middle = (left + right) // 2
value = lst[middle]
if value == target:
return middle
elif value < target:
left = middle + 1
else:
right = middle - 1
return -1
This example is a bit more complicated, because there’s no variable counting up or down to a fixed limit.
Intuitively, binary search should terminate because the “range of possibilities” keeps getting smaller — this range is from left
to right
, so right - left
could be a loop variant.
On each iteration, one of three things happens:
- The algorithm might terminate immediately — so, no problem.
- Or
left
becomesmiddle + 1
. - Or
right
becomesmiddle - 1
.
The loop condition is left <= right
, and middle
is halfway between them.
So, either left
gets bigger, or right
gets smaller — either way, right - left
gets smaller.
To prove the loop terminates, we need to show that left <= right
eventually becomes false.
This happens when right - left
reaches −1, so the proof is complete.(2)
Loop variants
After these examples, hopefully it’s clear what loop variants are, and how we can use them to prove algorithms terminate. But let’s also give a proper definition.
A loop variant is an expression which:
- Has an integer value.
- Gets at least 1 smaller on every iteration of the loop.
- When it gets below some threshold (usually 0), the loop condition becomes false.
Any loop with a variant is guaranteed to terminate, because an integer can’t keep getting smaller forever without falling below the threshold. Once it reaches the threshold, the loop condition becomes false, so the loop terminates.
A note on ‘for’ loops
In this post we’ve only analysed while loops. On the other hand, many algorithms use for loops:
for i in range(n):
# ...
If a for
loop iterates over a finite collection, such as a list, set or dictionary, or a finite range of integers, then the number of iterations is strictly limited to the size of that collection or range, so it can’t be an infinite loop.(3)
If necessary, we can still use variants to prove that a for
loop terminates, by writing an equivalent while
loop.
This example iterates over the same range, and has the variant n - i
.
i = 0
while i < n:
# ...
i += 1
Footnotes
- Fundamentally, an assertion says that when a line of code is reached, the condition will be true. There is no way to assert that a line of code will be reached.
- The variant is guaranteed to reach −1 for the same reason it’s guaranteed to reach 0.
Alternatively, we could choose
right - left + 1
as a variant. - This assumes the size doesn’t change during the loop.
It’s generally a mistake to make a collection larger while you’re iterating over it with a
for
loop, and many languages will raise an error if they detect this happening.
There are no published comments.