Loop invariants

More generally, to argue about the behavior of our loop, consider the following while loop:

where is a predicate whose validity depends on (a collection of) variables and be a set of program instructions. Applying instructions on variables would result in . Let be a predicate on . We say that is a loop invariant if the following holds:

That is, if the statement is satisfied before the program enters the loop and is loop-invariant, then must be satisfied after the program leaves the loop.

Exercise 7

Prove: If and are loop invariants for a while-loop, then is also a loop invariant for the same while-loop.

Let us look at a more complicated example where proving the behavior of the program is much less obvious. We are given a collection of squares of arbitrary sizes in the plane. Our goal is to pick as many non-overlapping (a.k.a. independent) squares as possible. How well can we solve this problem?

This problem is among the NP-hard problems, so we should not expect to solve it exactly by an efficient algorithm. In these notes, you will see a very simple heuristic that is always guaranteed to give at least -fraction of an optimal solution (i.e. if an optimal solution has rectangles, the heuristic reports at least rectangles). The idea is quite intuitive: We should be tempted to pick squares that have smaller areas, rather than the big ones. This motivates the following algorithm.

INDSQUARES()

1. Initialize solution
2. while do
   1. Let be the smallest square in
   3. Remove from all its squares that overlap with
3. return

Let denotes the maximum-cardinality of a subset of non-overlapping squares. Our goal is to argue that contains only non-overlapping squares and that .

Theorem 2

The following are loop invariants:

• (R1) No squares in overlap with .

• (R2) is a set of non-overlapping squares

• (R3)

Proof:

The first is easy to prove: Each while-loop updates and . Suppose that (R1) holds before the loop. Now, when is added into , all squares overlapping with are removed from . Therefore, (R1) continues to hold after this update. The second requires the first. Suppose that (R2) holds before the loop. Since is non-overlapping before the loop, from (R1), we know that cannot overlap with anything in . Therefore, is also non-overlapping. Finally, suppose that (R3) holds before the loop, so we have that (before). We need to argue that where contains the squares of that overlap with . Notice that $$\mathcal{M} - (\mathcal{S} - \mathcal{S}') = (\mathcal{M} -\mathcal{S}) \cup (\mathcal{M} \cap \mathcal{S}') $$It suffices to argue that . Consider each square . This square must be at least as large as (since we choose to be smallest in ). Moreover, overlaps with , so must contain a corner of ^[1]. However, since has only four corners, there can be at most four non-overlapping squares that contain its corner. It follows that .

At the end of the algorithm, we can use (R2) to say that is non-overlapping and (R3) to say that . Notice that (R1) is not needed to make this implication; it is stated for the sole purpose of arguing that (R2) is a loop invariant. Proving algorithmic properties rigorously often requires this trick.

Exercise 8

Consider a collection of closed intervals on the line where . Our goal is to choose as many non-overlapping intervals as possible.

• Consider the heuristic : Choose the smallest interval, remove all intervals that overlap with it, and repeat. Prove that this heuristic always returns a solution of size at least half of that of the optimal solution.

• Consider the heuristic : Choose the interval with minimum , remove all intervals that overlap with it, and repeat. Prove that heuristic always returns an optimal solution.

---

Footnotes

1. We assume that the squares in the are parallel for ease of explanation. ↩︎