The Central Idea
To prove termination, identify a measurable form of progress.
A typical argument shows that:
- a quantity is bounded in a direction;
- every iteration or recursive call changes that quantity toward the bound;
- therefore, the process cannot continue forever.
This is the basic logic behind most termination proofs.
Termination and Total Correctness
In the previous lesson, total correctness was separated into two parts:
\[ \boxed{\text{partial correctness}+\text{termination}}. \]Partial correctness says the answer is right if the algorithm stops.
Termination proves that the algorithm actually does stop.
A Simple Counting Loop
Consider a loop that starts with
\[ i=1 \]and increases \(i\) by \(1\) until
\[ i>n. \]If \(n\) is a fixed finite integer, then \(i\) can be incremented only finitely many times before the loop condition becomes false.
Progress Measures
A progress measure is a quantity used to show that an algorithm is moving toward completion.
Examples include:
- the number of unprocessed items;
- the size of a remaining interval;
- the number of unvisited vertices;
- the value of a positive integer parameter;
- the number of unresolved constraints.
Variants
A variant is a progress measure that changes strictly in a direction that cannot continue forever.
A common form is a nonnegative integer that strictly decreases on each iteration.
\[ V\in\{0,1,2,\ldots\}. \]If \(V\) decreases every time the loop repeats, then the loop must eventually stop.
Why Nonnegative Integers Are Useful
There is no infinite strictly decreasing sequence of nonnegative integers:
\[ n>n_1>n_2>n_3>\cdots. \]Eventually, a lower limit such as \(0\) must be reached.
Well-Founded Descent
More generally, termination can be proved using a well-founded order.
An order is well-founded when there is no infinite strictly descending chain.
If every recursive call or loop iteration strictly descends in such an order, infinite execution is impossible.
Loop Termination by Remaining Work
Suppose a loop processes one new array entry on every iteration.
Let
\[ V=n-i \]represent the number of entries remaining after position \(i\).
If \(i\) increases by \(1\), then \(V\) decreases by \(1\).
Because \(V\ge0\), the loop must terminate.
Termination of Linear Search
Linear search examines at most one new position per iteration.
A simple variant is
\[ V=\text{number of unexamined positions}. \]Each unsuccessful comparison reduces \(V\) by \(1\). Since the list is finite, eventually the target is found or \(V=0\).
Termination of Binary Search
Binary search repeatedly reduces the active interval.
Let
\[ V=\text{number of positions in the current search interval}. \]Each unsuccessful step replaces the interval with a strictly smaller one. Since \(V\) is a nonnegative integer, the search must terminate.
Repeated Halving Terminates Quickly
If the active size is approximately halved each time,
\[ n,\quad \frac{n}{2},\quad \frac{n}{4},\ldots, \]then after roughly
\[ \log_2 n \]reductions, constant size is reached.
Termination and efficiency are related but distinct ideas.
Recursive Termination
For recursive algorithms, a termination proof must show that every recursive call moves toward a base case.
A typical pattern is:
\[ n\longrightarrow n-1\longrightarrow n-2\longrightarrow\cdots\longrightarrow0. \]If the input is a nonnegative integer, this chain must eventually reach the base case.
Factorial Termination
Recursive factorial uses
\[ F(n)=nF(n-1) \]with base case
\[ F(0)=1. \]The variant is simply
\[ V=n. \]Each recursive call reduces \(V\) by \(1\).
Euclidean Algorithm Termination
The recursive Euclidean algorithm uses
\[ \gcd(a,b)=\gcd(b,a\bmod b) \]for \(b>0\).
The remainder satisfies
\[ 0\le a\bmod bWhy Merely Having a Base Case Is Not Enough
Suppose a recursive function has base case
\[ F(0) \]but for positive \(n\) calls
\[ F(n+1). \]The base case exists, but execution moves away from it.
Therefore, a base case alone does not prove termination.
Mutual Recursion
Sometimes one function calls another, which later calls the first. This is called mutual recursion.
Termination still requires a global progress measure that decreases across the entire chain of calls.
Lexicographic Variants
One number is not always enough to measure progress.
A pair such as
\[ (a,b) \]can be ordered lexicographically: first reduce \(a\), and when \(a\) is unchanged, reduce \(b\).
This can prove termination when progress happens in stages.
Example of a Two-Part Variant
Suppose an algorithm processes groups.
Let
\[ a=\text{number of unfinished groups} \]and
\[ b=\text{number of unfinished items in the current group}. \]Each step either reduces \(b\), or completes a group and reduces \(a\). The pair \((a,b)\) therefore descends lexicographically.
Finite-State Termination Arguments
Sometimes an algorithm moves through a finite set of states. If it never revisits a state and each step moves to a new state, then only finitely many steps are possible.
Visited Sets and Termination
Graph traversals commonly mark vertices when they are discovered.
If a finite graph has \(V\) vertices and each vertex is permanently marked at most once, then only finitely many discoveries can occur.
BFS Termination
- the graph has finitely many vertices;
- each vertex is enqueued at most once under standard visited-set logic;
- each queue removal handles one previously enqueued vertex.
Therefore, the queue eventually becomes empty.
DFS Termination
- each recursive call corresponds to a newly discovered vertex;
- there are only finitely many vertices;
- no visited vertex generates another recursive discovery call.
Therefore, recursion cannot continue indefinitely.
Backtracking Termination
Backtracking terminates when its search tree is finite and every recursive step moves one level deeper toward a bounded maximum depth.
Once a branch reaches a complete solution or a dead end, it returns. Eventually, every eligible finite branch has been explored or pruned.
Termination of Divide and Conquer
Divide-and-conquer methods terminate when every recursive subproblem is strictly smaller than the original.
For merge sort, list size decreases approximately as
\[ n,\quad \frac{n}{2},\quad \frac{n}{4},\ldots. \]Eventually, one-element base cases are reached.
Termination of Dynamic Programming
Bottom-up dynamic programming usually terminates because it fills a finite table.
If the table has \(N\) states and each state is processed once, only finitely many updates occur.
Memoized Recursion Still Needs a Termination Argument
Memoization prevents repeated work, but it does not automatically guarantee termination.
Recursive calls must still move through a well-founded dependency structure toward base states.
Greedy Algorithm Termination
Greedy procedures often process a finite candidate set. If each iteration permanently accepts or rejects at least one candidate, then the number of unprocessed candidates strictly decreases.
Termination of Kruskal's Algorithm
Kruskal's algorithm considers edges in sorted order. Each edge is processed at most once.
Since the graph has finitely many edges, the algorithm must stop after at most \(E\) edge considerations.
Termination of Dijkstra's Algorithm
In standard Dijkstra execution, each iteration settles one previously unsettled vertex.
A finite graph has only finitely many vertices. Therefore, after at most \(V\) settlements, no unsettled reachable vertex remains.
While Loops Require Extra Care
A loop written as "while a condition is true" does not reveal termination from syntax alone.
The proof must show that the loop body changes the state so the condition eventually becomes false.
A Nonterminating Loop
Suppose
\[ i=1 \]and the loop repeats while
\[ i>0 \]but updates
\[ i\leftarrow i+1. \]The condition remains true forever. The loop does not terminate.
Oscillation
Nontermination can occur even when variables change.
\[ A\to B\to A\to B\to\cdots. \]The algorithm is changing state, but not making progress toward a terminal state.
Cycles in State Space
If an algorithm can revisit an earlier state indefinitely, the execution may cycle.
Graph search avoids this by marking visited states. More generally, termination proofs often need to rule out infinite cycles in the state-transition structure.
Strict Progress Matters
Suppose a proposed variant satisfies
\[ V_{k+1}\le V_k. \]This only says the measure never increases. It may remain constant forever.
A stronger termination argument usually needs
\[ \boxed{V_{k+1}Bounded Increase Can Also Prove Termination
A variant does not have to decrease.
Suppose \(i\) strictly increases each iteration but can never exceed a finite bound \(n\). Then only finitely many increases are possible.
Increasing toward a finite ceiling is equivalent in spirit to decreasing remaining work toward \(0\).
Termination and Invariants
Invariants and variants serve different roles.
- An invariant describes what remains true.
- A variant describes what makes progress.
Both may be needed for a total-correctness proof.
Invariant Plus Variant
A loop proof may use an invariant such as
\[ \text{processed prefix is correct} \]together with a variant such as
\[ \text{number of unprocessed entries}. \]The invariant proves correctness; the variant proves termination.
Termination Does Not Prove Correctness
An algorithm may stop quickly and still return the wrong answer.
\[ \boxed{\text{termination}\not\Rightarrow\text{correctness}}. \]Both properties must be established separately.
Correctness Does Not Automatically Prove Termination
A proof may show that if an algorithm ever returns, the result is correct. But the algorithm may still run forever on some valid input.
This is the distinction between partial and total correctness.
Termination and Efficiency Are Different
A terminating algorithm may still take an impractically large amount of time.
Exhaustive search over \(2^n\) possibilities terminates for every finite \(n\), but its running time may grow very quickly.
The next lesson studies such growth more systematically.
Probabilistic Algorithms
Some randomized algorithms have termination behavior that depends on random choices.
One may distinguish:
- algorithms guaranteed to terminate after a bounded number of steps;
- algorithms that terminate with probability \(1\);
- algorithms whose expected running time is finite.
External Waiting Is Different
Some real programs wait for:
- user input;
- a network response;
- an external event;
- a sensor condition.
In such systems, termination may depend on assumptions about the environment rather than only on internal computation.
Preconditions Can Affect Termination
A termination proof may depend on input restrictions.
For example, a recursive procedure designed for nonnegative integers may fail to terminate if given a negative integer and repeatedly subtracting \(1\).
The valid input domain must be included in the argument.
Common Error: Naming a Variant That Does Not Change
A quantity cannot prove progress if some repeating iteration leaves it unchanged.
The variant must strictly move in the required direction whenever the algorithm continues.
Common Error: Using an Unbounded Measure
A variable may decrease without proving termination if it can decrease forever through an unbounded domain.
\[ 0,-1,-2,-3,\ldots \]A lower bound or well-founded domain is essential.
Common Error: Base Case Not Reachable
A recursive algorithm may contain a valid base case that no recursive path actually reaches.
Termination requires proving reachability of the base case from every valid starting input.
Common Error: One Branch Makes Progress, Another Does Not
In recursive algorithms with several branches, every recursive call must satisfy the termination argument.
It is not enough that one branch decreases the variant if another branch can keep the same or larger measure indefinitely.
Common Error: Assuming Finite Input Implies Finite Execution
A finite input does not guarantee termination. A program can loop forever while repeatedly manipulating the same finite data.
Progress must still be demonstrated.
Common Error: Confusing No Immediate Loop with Termination
A program may have no obvious loop statement and still fail to terminate because of recursive calls.
Termination analysis must follow the full control flow, including recursion and mutual recursion.
A Reliable Procedure for Proving Termination
- Identify the repeating structure: loop, recursion, search expansion, or repeated state transition.
- Choose a progress measure.
- State the domain or bound of that measure.
- Prove that every continuing step changes the measure strictly toward the bound.
- Show that the bound corresponds to a stopping condition or base case.
- Check every branch of the control flow.
- Check that the argument holds for every valid input.
- If one measure is insufficient, use a lexicographic or structural variant.
- Separate termination from correctness and from efficiency.
Example: Countdown Loop
Suppose \(n\ge0\) and a loop repeats while \(n>0\), replacing
\[ n\leftarrow n-1. \]Choose variant
\[ V=n. \]It is a nonnegative integer and decreases by \(1\) on every iteration. Therefore, the loop terminates.
Example: Processing a Queue
Suppose a procedure repeatedly removes one item from a finite queue and never adds new items.
Let
\[ V=\text{queue length}. \]Each iteration decreases \(V\) by \(1\). Since \(V\ge0\), the queue eventually becomes empty.
Example: Nested Loops
Suppose an outer loop processes \(n\) rows and, for each row, an inner loop processes \(m\) columns.
- the inner loop terminates after finitely many column steps;
- the outer loop advances after each completed inner loop;
- there are finitely many rows.
A lexicographic pair can formalize this nested progress.
Practice 1: Variant
A loop processes one new list element on each iteration.
Give a natural variant for proving termination.
Practice 2: Binary Search
What quantity can serve as a variant for binary search?
Practice 3: Recursive Termination
A recursive procedure on nonnegative integer \(n\) calls itself with \(n-2\) until \(n\le1\). Why does it terminate?
Practice 4: Bad Recursion
A procedure has base case \(F(0)\), but for \(n>0\) calls \(F(n+1)\). Why does the base case fail to prove termination?
Practice 5: Graph Traversal
Why does visited marking help prove termination of BFS or DFS on a finite graph?
Practice 6: Strict Progress
Why is the condition \(V_{k+1}\le V_k\) generally weaker than needed for a termination proof?
Practice 7: Bounded Increase
A variable starts at \(0\), increases by \(1\) each iteration, and the loop stops when it reaches \(100\). Why does the loop terminate?
Practice 8: Termination Versus Correctness
Does proving that an algorithm terminates prove that its answer is correct?
Practice 9: Finite Input
Does a finite input automatically guarantee that a program terminates?
Practice 10: Euclidean Algorithm
In \(\gcd(a,b)=\gcd(b,a\bmod b)\), what quantity provides the main termination progress?
Practice Answers
Practice 1
A natural variant is
\[ \boxed{\text{number of unprocessed list elements}}. \]Practice 2
Use
\[ \boxed{\text{size of the active search interval}}. \]Practice 3
The nonnegative input decreases by \(2\) on each recursive call and must eventually reach \(0\) or \(1\).
Practice 4
The recursive call moves away from \(0\). Starting with positive \(n\), the sequence \(n,n+1,n+2,\ldots\) never reaches the base case.
Practice 5
Visited marking prevents repeated rediscovery. Since a finite graph has only finitely many vertices, only finitely many first discoveries can occur.
Practice 6
The measure could remain constant forever. Termination typically needs strict progress whenever execution continues.
Practice 7
The variable strictly increases but is bounded above by \(100\). Only finitely many increments are possible.
Practice 8
No. Termination proves only that the algorithm stops.
Practice 9
No. A program can revisit the same states or loop forever even on finite input.
Practice 10
The second argument decreases because
\[ 0\le a\bmod bWhat to Remember
- Termination proves that an algorithm eventually stops on every valid input.
- A variant or progress measure must move strictly toward a bound or base case.
- Nonnegative integers are useful because they cannot decrease forever.
- Recursive calls must move toward reachable base cases.
- Visited sets can prevent infinite revisiting in graph algorithms.
- Finite search trees support backtracking termination.
- Invariants prove preserved truth; variants prove progress.
- Termination does not imply correctness, and correctness does not automatically imply termination.
- A terminating algorithm may still be inefficient.
The most important habit is: identify exactly what gets closer to completion every time the algorithm continues, and prove that this progress cannot continue forever.
Where We Go Next
Once an algorithm is known to be correct and terminating, another question becomes central: how much work and memory does it require as the input grows?
The next lesson, Time and Space Complexity, develops input size, operation counts, growth rates, asymptotic notation, best and worst cases, memory usage, and the comparison of algorithmic efficiency.