Proofs: Lengauer-Tarjan algorithm

The Lengauer-Tarjan algorithm computes the immediate dominators full

This proof shows: correctness, termination.

Setting. $G$ is a directed graph with start vertex $r$. Only the vertices reachable from $r$ matter: an edge from an unreachable vertex lies on no path from $r$, so dropping such edges, as line L4 does, changes no dominator. After line L1 the reachable vertices are identified with their preorder numbers $0, \ldots, k - 1$ in a depth-first search from $r$, so $r = 0$. $T$ is the DFS tree. We write $x \to^* y$ if $x$ is an ancestor of $y$ in $T$ (possibly $x = y$) and $x \to^+ y$ for a proper ancestor. All paths start where stated; "dominates" refers to paths from $r$. Dominance is a partial order whose strict dominators of a vertex form a chain, and $\mathrm{idom}(w)$ is the lowest of them; this is proved on the page of the dominator tree. The semidominator $\mathrm{sdom}(w)$ for $w \ne r$ is the least $v$ such that some path $v = v_0, \ldots, v_j = w$ has $v_i > w$ for $0 < i < j$; we call such a path an sdom path for $w$. Removing a cycle from an sdom path gives an sdom path, so we may take them simple.

Lemma 0 (preorder intervals). The descendants of $x$ in $T$ are exactly the numbers $x, x + 1, \ldots, x + s(x) - 1$, where $s(x)$ is the size of the subtree of $x$. The ancestors of a vertex $y$ form the tree path from $r$ to $y$, with numbers increasing downward.

Proof. The DFS numbers $x$ when it first reaches it and then numbers all vertices reached before it leaves $x$, which are exactly the descendants of $x$, so they get the next $s(x) - 1$ numbers. A parent is numbered before its child. $\square$

Lemma 1 (DFS edges). If $(v, w)$ is an edge with $v < w$, then $v \to^* w$.

Proof. When the DFS examines the edge $(v, w)$, $v$ is on the stack. If $w$ is unvisited, it becomes a child of $v$. Otherwise $w$ was numbered after $v$ and before this moment, that is, while $v$ was on the stack, so $w$ is a descendant of $v$. $\square$

Lemma 2 (path lemma). If $v \le w$, every path from $v$ to $w$ contains a common ancestor of $v$ and $w$.

Proof. Let $x$ be the vertex of least number on the path. By induction along the path, every vertex $y$ after $x$ is a descendant of $x$: for an edge $(y, z)$ with $y$ a descendant of $x$, either $z > y$, and $z$ is a descendant of $y$ by Lemma 1, or $x \le z < y$, and $z$ lies in the interval of $x$ by Lemma 0. So $w$ is a descendant of $x$, and $x \le v \le w$ places $v$ in the interval of $x$ as well. $\square$

Lemma 3 (positions). For $w \ne r$: $\mathrm{idom}(w) \to^+ w$, $\mathrm{sdom}(w) \to^+ w$, and $\mathrm{idom}(w) \to^* \mathrm{sdom}(w)$.

Proof. The tree path from $r$ to $w$ is a path in $G$, so every dominator of $w$ is on it, and the strict ones are proper ancestors. The edge from the parent of $w$ is an sdom path, so $\mathrm{sdom}(w) \le parent(w) < w$. Take an sdom path from $v_0 = \mathrm{sdom}(w)$ to $w$. By Lemma 2 it contains a common ancestor $x$ of $v_0$ and $w$, so $x \le v_0 < w$; internal vertices are $> w$ and $w$ itself is not an ancestor of $v_0 < w$, so $x = v_0$, and $v_0 \to^+ w$. Finally, the tree path from $r$ to $\mathrm{sdom}(w)$ followed by the sdom path is a path to $w$ whose vertices are ancestors of $\mathrm{sdom}(w)$, numbers $> w$, or $w$. A proper ancestor $y$ of $w$ with $\mathrm{sdom}(w) \to^+ y$ has $\mathrm{sdom}(w) < y < w$ and lies on neither part, so it does not dominate $w$. Hence $\mathrm{idom}(w)$, a proper ancestor of $w$, is an ancestor of $\mathrm{sdom}(w)$. $\square$

Lemma 4 (nesting). If $v \to^* w$ and $v \ne r$, then $v \to^* \mathrm{idom}(w)$ or $\mathrm{idom}(w) \to^* \mathrm{idom}(v)$.

Proof. Let $x$ satisfy $\mathrm{idom}(v) \to^+ x \to^+ v$. Then $x$ does not dominate $v$, since the dominators of $v$ are $v$ and the ancestors of $\mathrm{idom}(v)$. So some path from $r$ to $v$ avoids $x$; followed by the tree path from $v$ to $w$, whose vertices are descendants of $v$ and hence not $x$, it reaches $w$ avoiding $x$. So $\mathrm{idom}(w)$, which is on the tree path to $w$, is not strictly between $\mathrm{idom}(v)$ and $v$: it is either a descendant of $v$ or an ancestor of $\mathrm{idom}(v)$. $\square$

Theorem 1 (semidominator formula). For $w \ne r$, $\mathrm{sdom}(w) = \min(A \cup B)$, where $A = \{v : (v, w) \in E, v < w\}$ and $B = \{\mathrm{sdom}(u) : u > w \text{ and } u \to^* v \text{ for some edge } (v, w) \in E\}$.

Proof. Let $x = \min(A \cup B)$; $A$ contains $parent(w)$, so it is not empty. $\mathrm{sdom}(w) \le x$. An element $v \in A$ is the start of the sdom path $v, w$. For an element $\mathrm{sdom}(u) \in B$, take an sdom path for $u$, then the tree path from $u$ to $v$, then the edge $(v, w)$. The internal vertices of the first part are $> u > w$, $u$ itself is $> w$, and the tree path from $u$ consists of descendants of $u$, numbered $\ge u > w$. So this is an sdom path for $w$ from $\mathrm{sdom}(u)$.

$x \le \mathrm{sdom}(w)$. Let $v_0 = \mathrm{sdom}(w), v_1, \ldots, v_j = w$ be a simple sdom path. If $j = 1$, then $v_0 \in A$. If $j > 1$, let $i \ge 1$ be the least index with $v_i \to^* v_{j-1}$; it exists because $i = j - 1$ qualifies. We claim $v_t > v_i$ for $0 < t < i$. Otherwise let $v_t$ be the least of $v_1, \ldots, v_{i-1}$, with $v_t < v_i$ (equality is excluded because the path is simple). By Lemma 2 the subpath from $v_t$ to $v_i$ contains a common ancestor $v_s$ of both, with $t \le s \le i$. Then $v_s \le v_t$, so $s = t$ or $s = i$ by the choice of $t$. If $s = t$, $v_t \to^* v_i \to^* v_{j-1}$ with $1 \le t < i$, contradicting the choice of $i$; if $s = i$, $v_i$ is an ancestor of $v_t$ and $v_i \le v_t$, a contradiction. So $v_0, \ldots, v_i$ is an sdom path for $v_i$, and $\mathrm{sdom}(v_i) \le v_0$. Also $v_i > w$ because it is an internal vertex, and $v_i \to^* v_{j-1}$ with $(v_{j-1}, w) \in E$. So $\mathrm{sdom}(v_i) \in B$ and $x \le \mathrm{sdom}(v_i) \le v_0$. $\square$

Theorem 2 (immediate dominator rule). For $w \ne r$, let $u$ be a vertex of least $\mathrm{sdom}(u)$ among the vertices $y$ with $\mathrm{sdom}(w) \to^+ y \to^* w$. Then $\mathrm{sdom}(u) \le \mathrm{sdom}(w)$, and $\mathrm{idom}(w) = \mathrm{sdom}(w)$ if $\mathrm{sdom}(u) = \mathrm{sdom}(w)$, while $\mathrm{idom}(w) = \mathrm{idom}(u)$ if $\mathrm{sdom}(u) < \mathrm{sdom}(w)$.

Proof. The set contains $w$, so $\mathrm{sdom}(u) \le \mathrm{sdom}(w)$. We use one claim twice.

Claim. Let $z \ne r$ be a proper ancestor of $w$ and $P$ a path from $r$ to $w$ that avoids $z$. Let $x$ be the last vertex of $P$ with $x < z$ (it exists because $r < z$), and $y$ the first vertex after $x$ on $P$ with $z \to^+ y \to^* w$ (it exists because $w$ qualifies). Then $\mathrm{sdom}(y) \le x < z$.

Proof of the claim. Let $x = x_0, x_1, \ldots, x_q = y$ be the part of $P$ between them, made simple. Suppose some internal $x_t$ has $x_t < y$, and take the least such $x_t$. By Lemma 2 the subpath from $x_t$ to $y$ contains a common ancestor $x_s$ of $x_t$ and $y$; as before $s = t$, so $x_t \to^* y \to^* w$. Since $x_t$ comes after $x$ on $P$, $x_t \ge z$, and $x_t \ne z$ because $P$ avoids $z$; an ancestor of $w$ numbered above the ancestor $z$ of $w$ is a proper descendant of $z$ (Lemma 0). So $z \to^+ x_t \to^* w$, and $x_t$ comes before $y$, against the choice of $y$. So all internal vertices exceed $y$, the part is an sdom path for $y$, and $\mathrm{sdom}(y) \le x$. $\square$

Case $\mathrm{sdom}(u) = \mathrm{sdom}(w)$. Then $\mathrm{sdom}(y) \ge \mathrm{sdom}(w)$ for every $y$ with $\mathrm{sdom}(w) \to^+ y \to^* w$. If $\mathrm{sdom}(w) = r$, it dominates $w$. Otherwise suppose a path $P$ avoids $z = \mathrm{sdom}(w)$; the claim gives such a $y$ with $\mathrm{sdom}(y) < \mathrm{sdom}(w)$, a contradiction. So $\mathrm{sdom}(w)$ dominates $w$; it is a proper ancestor of $w$ and, by Lemma 3, a descendant of $\mathrm{idom}(w)$. As $\mathrm{idom}(w)$ is the lowest strict dominator, $\mathrm{idom}(w) = \mathrm{sdom}(w)$.

Case $\mathrm{sdom}(u) < \mathrm{sdom}(w)$. Here $u \ne r$, since $u > \mathrm{sdom}(w) \ge r$. By Lemma 3, $\mathrm{idom}(u) \to^* \mathrm{sdom}(u)$, and $\mathrm{sdom}(u)$ is an ancestor of $u$ numbered below $\mathrm{sdom}(w)$, hence $\mathrm{sdom}(u) \to^+ \mathrm{sdom}(w)$. So $\mathrm{idom}(u) \to^+ \mathrm{sdom}(w) \to^+ u \to^* w$. By Lemma 4 applied to $u \to^* w$, either $u \to^* \mathrm{idom}(w)$, which is impossible because $\mathrm{idom}(w) \to^* \mathrm{sdom}(w) \to^+ u$ (Lemma 3), or $\mathrm{idom}(w) \to^* \mathrm{idom}(u)$.

It remains to show that $z = \mathrm{idom}(u)$ dominates $w$; then $z$ is a strict dominator of $w$, hence an ancestor of $\mathrm{idom}(w)$, and the two are equal. If $z = r$ this is clear. Otherwise suppose a path $P$ to $w$ avoids $z$ and take $x$ and $y$ from the claim, with $\mathrm{sdom}(y) \le x < z$. If $\mathrm{sdom}(w) \to^+ y$, then $y$ is in the set that defines $u$, and $\mathrm{sdom}(y) < z \le \mathrm{sdom}(u)$ (by Lemma 3, $z \to^* \mathrm{sdom}(u)$) contradicts the choice of $u$. Otherwise $z \to^+ y \to^* \mathrm{sdom}(w) \to^+ u$, so $y$ is strictly between $z$ and $u$ on the tree path. Now $\mathrm{sdom}(y)$ is an ancestor of $y$ (Lemma 3) numbered below $z$, so it is a proper ancestor of $z$. The tree path from $r$ to $\mathrm{sdom}(y)$ (ancestors of $\mathrm{sdom}(y)$, all numbered below $z$), an sdom path from $\mathrm{sdom}(y)$ to $y$ (internal vertices above $y > z$), and the tree path from $y$ to $u$ (descendants of $y$) form a path from $r$ to $u$ that avoids $z = \mathrm{idom}(u)$, a contradiction. $\square$

Lemma 5 (the forest). Consider the moment just before EVAL is called. Every vertex $x$ with $ancestor[x] \ne$ none has been linked, $ancestor[x] \to^+ x$, every vertex on the tree path from $ancestor[x]$, exclusive, down to $x$ has been linked, and $label[x]$ is a vertex of least $semi$ on that path. Moreover $semi$ of a linked vertex no longer changes. Then EVAL$(v)$ returns $v$ if $v$ is unlinked, and otherwise a vertex of least $semi$ on the tree path from the highest unlinked ancestor of $v$, exclusive, down to $v$; and it preserves the invariant.

Proof. The invariant holds after line L6 links $w$, since $label[w] = w$ and the path from $parent(w)$, exclusive, to $w$ is $\{w\}$; $semi[w]$ is final at that point and is not written again. If $v$ is unlinked, line L12 returns $v$. Otherwise line L14 collects $v = x_1, x_2 = ancestor[x_1], \ldots$ as long as $ancestor[ancestor[x]]$ exists, so it stops at a vertex $x_{j+1}$ whose ancestor $z$ is unlinked: $z$ is the root of the forest tree, and the highest unlinked ancestor of $v$, because all vertices strictly below $z$ on the path are linked by the invariant, and $z$ is unlinked. Line L15 processes $x_j, \ldots, x_1$. When it reaches $x_t$, $ancestor[x_{t+1}] = z$ already holds and $label[x_{t+1}]$ is a minimum on the path from $z$, exclusive, to $x_{t+1}$ (for $t = j$ this is the invariant for $x_{j+1}$, whose ancestor is $z$). Combining with $label[x_t]$, a minimum on the path from $x_{t+1}$, exclusive, to $x_t$, gives a minimum on the path from $z$, exclusive, to $x_t$, and $ancestor[x_t]$ becomes $z$. So the invariant holds after the update, and $label[v]$ is the required minimum. $\square$

Theorem 3. The algorithm terminates and returns $\mathrm{idom}(w)$ for every $w \ne r$ reachable from $r$.

Proof. Termination. The DFS pushes each vertex once. Each loop of lines L3 to L11 runs over a finite set, and the loop of line L14 climbs strictly upward in $T$ (by Lemma 5, $ancestor[x] \to^+ x$).

Semidominators. We show that when $w$ is processed, line L5 sets $semi[w] = \mathrm{sdom}(w)$. At that time the linked vertices are exactly those numbered above $w$, with their final $semi$ by induction. For a predecessor $v < w$: $v$ is unlinked, $semi[v] = v$, and EVAL returns $v$: these are the elements of $A$. For a predecessor $v > w$: the ancestors of $v$ numbered above $w$ are linked, and the highest unlinked ancestor $z$ of $v$ has $z \le w$, so the tree path from $z$, exclusive, to $v$ is exactly the set of ancestors $u$ of $v$ with $u > w$, by Lemma 0. EVAL returns one of them with least $semi = \mathrm{sdom}$. These give the elements of $B$, and $semi[w]$ starts at $w > $ every element of $A \cup B$, so line L5 computes $\min(A \cup B) = \mathrm{sdom}(w)$ by Theorem 1.

Buckets. Vertex $v$ enters $bucket[\mathrm{sdom}(v)]$ when it is processed. Let $c$ be the child of $p = \mathrm{sdom}(v)$ on the tree path to $v$. The vertices processed after $v$ and before $c$ are numbered between $c$ and $v$, hence lie in the subtree of $c$ (Lemma 0), and none of them is a child of $p$. So $v$ stays in $bucket[p]$ until $c$ is processed, and is handled in line L8 at $w = c$, after $c$ is linked. At that moment the linked vertices are those numbered $\ge c$, so the whole tree path from $c$ to $v$ is linked and $p$ is not, and by Lemma 5 EVAL$(v)$ returns a vertex $u$ of least $\mathrm{sdom}$ among $y$ with $p \to^+ y \to^* v$, which is the vertex of Theorem 2. If $semi[u] \ge semi[v]$, then $\mathrm{sdom}(u) = \mathrm{sdom}(v)$ and line L8 sets $idom[v] = p = \mathrm{idom}(v)$. Otherwise it sets $idom[v] = u$ with $\mathrm{idom}(v) = \mathrm{idom}(u)$ and $p < u < v$.

Final pass. Line L11 changes $idom[w]$ exactly when $idom[w] = u \ne semi[w] = p$, that is, in the second case; there $u < w$, so in increasing order $idom[u]$ is already final, and $idom[w] \leftarrow idom[u] = \mathrm{idom}(u) = \mathrm{idom}(w)$. In the first case $idom[w] = semi[w]$ and nothing changes. Renaming back to the original labels preserves all answers. $\blacksquare$