17.22 Correctness Proofs
Geometric algorithms are easy to test visually and surprisingly easy to get wrong.
17.22 Correctness Proofs
Problem
Geometric algorithms are easy to test visually and surprisingly easy to get wrong.
A convex hull may look correct on ordinary inputs but fail on collinear points. A sweep-line algorithm may work for separated rectangles but miscount shared boundaries. A point-in-polygon test may pass random examples but fail when the query point lies exactly on an edge.
To trust a geometric algorithm, you need more than a few sample runs. You need a correctness argument that explains why the algorithm handles all required cases.
Solution
Build correctness proofs around invariants, predicates, and decomposition.
Most computational geometry proofs use a small number of recurring techniques:
invariants
case analysis
exchange arguments
ordering arguments
convexity arguments
exhaustive decomposition
The goal is not to write a formal proof for every production function. The goal is to understand what must remain true while the algorithm runs.
Start with the Specification
Before proving an algorithm correct, state the problem precisely.
For convex hull:
Return the smallest convex polygon containing every input point.
For segment intersection:
Return true exactly when two closed segments share at least one point.
For rectangle union area:
Return the measure of the region covered by at least one rectangle.
The specification must define boundary behavior.
For example:
Does endpoint touching count as segment intersection?
Does a point on a polygon edge count as inside?
Are rectangles closed, open, or half-open?
Many correctness bugs are really specification bugs.
Proving Predicates First
Many geometric algorithms depend on low-level predicates.
Example:
def orientation(a, b, c):
return (
(b.x - a.x) * (c.y - a.y)
-
(b.y - a.y) * (c.x - a.x)
)
Correctness claim:
orientation(a,b,c) > 0 iff a -> b -> c is a left turn
orientation(a,b,c) < 0 iff a -> b -> c is a right turn
orientation(a,b,c) = 0 iff a,b,c are collinear
Once this predicate is trusted, later proofs can use it as a lemma.
This mirrors good software design: prove or test the foundation once, then reuse it.
Segment Intersection Proof
The standard segment-intersection algorithm checks orientations.
For segments:
AB
CD
the proper-crossing case occurs when:
C and D lie on opposite sides of AB
A and B lie on opposite sides of CD
That is exactly what these tests express:
o1 = orientation(A, B, C)
o2 = orientation(A, B, D)
o3 = orientation(C, D, A)
o4 = orientation(C, D, B)
if o1 * o2 < 0 and o3 * o4 < 0:
return True
Correctness argument:
If C and D are on opposite sides of line AB, then segment CD crosses the infinite line through AB.
If A and B are on opposite sides of line CD, then segment AB crosses the infinite line through CD.
Both conditions together imply the crossing point lies on both finite segments.
Collinear cases are handled separately by checking whether a point lies inside the bounding box of the other segment.
This proof is a case split:
proper crossing
endpoint touching
collinear overlap
disjoint
Every possible relationship between two segments belongs to one of these cases.
Convex Hull Proof
Andrew’s monotonic chain algorithm keeps a stack-like list of hull vertices.
The key invariant for the lower hull:
After processing each point, lower is the lower convex chain of all processed points.
The algorithm maintains this invariant with:
while len(lower) >= 2 and orientation(lower[-2], lower[-1], p) <= 0:
lower.pop()
lower.append(p)
Correctness argument:
When the last two points of lower and the new point p do not make a left turn, the middle point cannot be a vertex of the lower hull. It lies on or above the segment that should form the lower boundary.
Removing that point restores the possibility of convexity.
The loop continues until the chain is convex again.
Because points are processed in sorted x-order, no future point can make a removed point necessary for the lower hull.
The same argument applies symmetrically to the upper hull.
Joining the two chains gives the full convex hull.
Closest Pair Proof
The divide-and-conquer closest-pair algorithm uses exhaustive decomposition.
Every closest pair must be one of three kinds:
both points in the left half
both points in the right half
one point in each half
The recursive calls solve the first two cases.
Let:
d
be the smaller distance found recursively.
Any cross-boundary pair closer than d must lie within distance d of the split line. Therefore, it must appear in the strip.
The strip is sorted by y-coordinate. A packing argument shows that each point only needs to be compared with a constant number of following points.
Therefore, the merge step checks every cross-boundary pair that could improve the answer.
All cases are covered.
Sweep-Line Proof
Sweep-line proofs usually depend on an active-set invariant.
For rectangle union area:
Immediately before processing events at x, active contains exactly the y-intervals of rectangles covering the slab from previous_x to x.
Between two adjacent event coordinates, no rectangle starts or ends.
Therefore, the active set is constant throughout that slab.
The area contribution is:
covered_y_length(active) × (x - previous_x)
After processing all events at x, the invariant holds for the next slab.
By induction over event positions, the algorithm accumulates exactly the union area.
Rotating Calipers Proof
Rotating-calipers algorithms use monotonicity.
For a convex polygon, as one edge advances around the boundary, the farthest opposite vertex does not move backward.
This monotonicity implies:
each pointer completes at most one full rotation
Correctness argument for diameter:
The farthest pair of points on a convex polygon must be an antipodal pair.
The algorithm enumerates all antipodal pairs by rotating support lines around the hull.
Since every possible diameter pair appears among these pairs, and the algorithm measures each candidate, the maximum found is the true diameter.
Point-in-Polygon Proof
Ray casting relies on parity.
Draw a ray from the query point to infinity.
Each time the ray crosses the polygon boundary, the location changes between:
outside
inside
outside
inside
If the ray crosses the boundary an odd number of times, the point is inside.
If it crosses an even number of times, the point is outside.
Boundary cases must be removed first. If the point lies on an edge, return the boundary classification immediately. This avoids ambiguous parity when the ray passes through a vertex or along an edge.
Common Proof Patterns
Invariant
Used when an algorithm maintains a structure over time.
Examples:
convex hull stack
sweep-line active set
Delaunay triangulation after each insertion
Exhaustive Case Split
Used when geometric objects have a small number of possible relationships.
Examples:
segments intersect properly
segments touch at endpoint
segments overlap collinearly
segments are disjoint
Exchange Argument
Used to show that a chosen object can replace another without making the solution worse.
Examples:
convex hull vertex removal
greedy geometric optimization
Monotonicity
Used when a pointer, event, or boundary only moves in one direction.
Examples:
rotating calipers
two-pointer interval scans
sweep-line event order
Convexity
Used when straight-line containment and supporting lines simplify the problem.
Examples:
half-plane intersection
convex hull
Delaunay and Voronoi reasoning
Testing the Proof
A proof should suggest tests.
For segment intersection, test each proof case:
proper crossing
endpoint touch
collinear overlap
parallel disjoint
same segment
zero-length segment
For convex hull, test the invariant-breaking cases:
all points collinear
duplicate points
interior points
points already sorted
points in reverse order
For sweep line, test event-order cases:
shared boundaries
same x-coordinate events
zero-width rectangles
nested rectangles
disjoint rectangles
Good tests exercise the proof structure, not just ordinary examples.
Common Pitfalls
Proving the Easy Case Only
Many algorithms work on general position inputs. Real data contains degeneracy.
Leaving Boundary Semantics Undefined
A proof cannot be precise if the specification is vague.
Ignoring Numeric Assumptions
A mathematical proof assumes exact predicates. Floating-point code may violate that assumption.
Confusing Candidate Generation with Correctness
A spatial index returns candidates. The exact predicate proves the result.
Trusting a Diagram Too Much
Diagrams help intuition, but proofs need explicit cases and invariants.
Discussion
Correctness proofs in computational geometry are often compact once the right invariant is visible. Convex hull algorithms maintain convex chains. Sweep-line algorithms maintain active sets. Closest-pair algorithms decompose all possible answers into left, right, and crossing cases. Point-in-polygon algorithms rely on parity. Segment intersection relies on orientation signs and bounding boxes.
The practical value of a proof is not just confidence. It tells you what to test, what assumptions to document, and where numeric robustness matters.