Lengauer-Tarjan算法的相关证明
0. 约定
为简单起见，下文中的路径均指简单路径（事实上非简单路径不会对结论造成影响）。
(V)代表图的点集，(E)代表图的边集，(T)代表图的DFS树。
(a o b)代表从点(a)直接经过一条边到达点(b)（即((a, b) in T)），
(a leadsto b)代表从点(a)经过某条路径到达点(b)，
(a dot o b)代表从点(a)经过(T)的树边到达点(b)（在(T)上(a)是(b)的祖先），
(a overset{+} o b)代表(a dot o b)且(a
e b)。
这4种符号也同时表示路径。
1. 基本介绍 支配树(Dominator Tree)
(G = (V, E, r))为点集为(V)，边集为(E)，起点为(r)的流程图。如果一个从(r)到(w)的所有路径都经过(v)，那么称(v)支配(w)，(v)是(w)的支配点。如果(v)是(w)的支配点，且(w)的其他所有支配点均支配(v)，那么称(v)是(w)的直接支配节点(immediate dominator)，记作(idom(w) = v)。
定理1. 图(G)中除点(r)外其他所有点都有唯一的直接支配节点。点集(V)和边集({ (idom(w), w) | w in V - {r} })组成了一棵以点(r)为根的有向树，称为图(G)的支配树(Dominator Tree)。点(v)支配点(w)当且仅当在支配树上点(v)是点(w)的祖先。
2. 支配树相关性质
首先，我们从起点(r)对图(G)进行DFS，得到了一棵DFS树(T)。原图(G)中的边((u, v))就分为了树边(( (u, v) in T))和非树边(( (u, v) otin T))。非树边还可以分为前向边（(u)是(v)的祖先），后向边（(u)是(v)的后代），横叉边（(u, v)非祖先后代关系）。
我们通过DFS序比较两个点的大小关系。那么前向边((u, v))满足(u < v)，后向边((u, v))满足(u > v)，横叉边((u, v))满足(u > v)。
接下来给出一些有关支配树算法的重要引理。
引理1.（路径引理） 如果图(G)的两个点(v, w)满足(v le w)，那么点(v)到点(w)任意路径一定经过点(v)和点(w)的某个在树(T)上的公共祖先（至少一个）
证明： 如果(v)是(w)的祖先，结论显然成立（必然经过点(v)）。否则(v, w)非祖先后代关系，令(p)为(LCA(u, v))，显然(p e v and p e w)。删掉从起点(r)到(p)的路径上的所有点（这些点是(v, w)的公共祖先），那么(v)和(w)在以(p)为根两棵子树内，并且因为公共祖先被删去，无法通过后向边到达子树外面，前向边也无法跨越子树，而横叉边只能从大到小（(v)所在子树内的点均大于(w)所在子树内的点），所以从(v)出发不能离开这颗子树到达w。所以如果本来(v)能够到达(w)，就说明这些路径必须经过(v, w)的公共祖先。
一个小推论： 如果图(G)的两个点(v, w)满足(v lt w)，那么点(v)到点(w)任意路径一定经过点(w)的某个在树(T)上的真祖先（至少一个）。
对于图(G)中的点(w)（(w e r)），定义它的半支配点(semi-dominator)(sdom(w) = min { v | exists (v_0, v_1, cdots, v_{k - 1}, v_k), v_0 = v, v_k = w, forall 1 leq i leq k - 1, v_i gt w } ag{1})
半支配点有很多性质，使得它们的计算成为支配点计算中的一个方便的中间步骤。对于任意点(w)（(w eq r)），(sdom(w))是(w)在树(T)上的真祖先，(idom(w))是(sdom(w))在树(T)上的祖先。如果把图(G)中的树边边集替换为边集({ (sdom(w), w) | w in V and w eq r })，在新图(G')中的所有点的支配点并不会改变。因此如果我们知道了DFS树和半支配点，我们可以计算出支配点。
以下将证明半支配点的这些性质。接下来的引理给出了DFS树，半支配点和支配点之间一般关系。
引理2. 对于任意点(w)（(w e r)），有(idom(w) overset{+}{ o} w)。
证明： 显然，如果不是这样的话就可以直接通过树边不经过(idom(w))就到达(w)了，与(idom)定义矛盾。
引理3. 对于任意点(w)（(w e r)），有(sdom(w) overset{+}{ o} w)。
证明： 对于(w)在树(T)上的父亲(fa_w)，(fa_w o w)这条路径只有两个点，所以满足(sdom)定义中的条件，于是它是(sdom(w))的一个候选，所以(sdom(w) le fa_w)，就有(sdom(w) lt w)。根据引理1（路径引理）可以证明(sdom(w))不可能在另一棵子树，因为如果是那样的话就至少会经过(w)的一个真祖先，(w)的真祖先小于(w)，与(sdom(w))的定义矛盾，于是(sdom(w))就是(w)的真祖先。
引理4. 对于任意点(w)（(w e r)），有(idom(w) dot o sdom(w))。
证明： 如果不是这样的话，按照(sdom)的定义，就会有一条路径是(r dot o sdom(w) leadsto w)不经过(idom(w))了，与(idom)的定义矛盾。
引理5. 对于满足(v dot o w)的点(v, w)，有(v dot o idom(w))或(idom(w) dot o idom(v))。
证明： 如果(v = w)显然成立。否则，如果不是这样的话，就是(idom(v) overset{+}{ o} idom(w) overset{+}{ o} v overset{+}{ o} w)，那么存在路径(r dot o idom(v) leadsto v overset{+}{ o}w)不经过(idom(w))到达了(w)（因为(idom(w))是(idom(v))的真后代，一定不支配(v)，所以存在绕过(idom(w))到达(v)的路径），与(idom)的定义矛盾。
通过引理1-5，我们获得了能提供从半支配点计算支配点的方法的两个结论。
定理2. 对于任意点(w)（(w e r)），如果所有满足(sdom(w) overset{+}{ o} u dot o w)的(u)也满足(sdom(u) ge sdom(w))，即(sdom(w) dot o sdom(u) overset{+}{ o} u dot o w)，那么(idom(w) = sdom(w))。
证明： 由引理4知道(idom(w) dot o sdom(w))，所以只需要证明(sdom(w))支配(w)就可以证明此定理。对于(r)到(w)的任意一条路径(p)，令(x)为路径(p)上最后一个满足(x lt sdom(w))的点。如果(x)不存在，那么(sdom(w) = r)支配(w)，得证。否则令(y)为路径(p)上(x)之后的满足(sdom(w) dot o y dot o w)的最小的点。令(q = (x = v_0, v_l, v_2, dots , v_k = y))为路径(p)上(x)到(y)的部分。我们可以断言(v_i gt y, forall 1 le i le k - 1)。假设它不成立，即(exists v_i lt y, 1 le i le k - 1)。通过引理1可得存在(v_j(i le j le k - 1))是(y)的真祖先。由(x)的定义可得(v_j ge sdom(w))，所以(sdom(w) dot o v_j overset{+}{ o} y dot o w)，这与(y)的定义矛盾，所以此断言得证。
此断言使得路径(q)也是满足半支配点定义中的路径，并且由于(x)的定义，所以(sdom(y) le x lt sdom(w))。因为所有满足(sdom(w) overset{+}{ o} u dot o w)的(u)也满足(sdom(u) ge sdom(w))，而(sdom(w) dot o y dot o w)，所以(y = sdom(w))，由此可得(r)到(w)的任意一条路径都经过(sdom(w))，(sdom(w))支配(w)，此定理得证。
定理3. 对于任意点(w)（(w e r)），令(u)为所有满足(sdom(w) overset{+}{ o} u dot o w)的(u)中(sdom(u))最小的一个，且(sdom(u) le sdom(w)) ，即(sdom(u) dot o sdom(w) overset{+}{ o} u dot o w)，那么(idom(w) = idom(u))。
证明： 令(z)为满足(sdom(w) o z dot o w)的点，有(sdom(u) le sdom(z) le sdom(w))。
由引理5可得(u dot o idom(w))或(idom(w) dot o idom(u)成立)。由引理4和命题条件可得(idom(w) dot o sdom(w) overset{+}{ o} u)，所以前者不成立，那么后者一定成立。为了证明(idom(w) = idom(u))，只需要证明(idom(u))支配(w)。
对于(r)到(w)的任意一条路径(p)，令(x)为路径(p)上最后一个满足(x lt idom(u))的点。如果(x)不存在，那么(idom(u) = r)支配(w)，得证。否则令(y)为路径(p)上(x)之后的满足(idom(u) dot o y dot o w)的最小的点。令(q = (x = v_0, v_l, v_2, dots , v_k = y))为路径(p)上(x)到(y)的部分。类似定理2中这部分的证明，(x)和(y)的定义说明(v_i gt y(1 le i le k - 1))，因此(sdom(y) le x)。由于由引理4得到的(idom(u) dot o sdom(u))，有(sdom(y) le x lt idom(u) le sdom(u))。
由于(u)是树(T)上从(z)到(w)的路径上的点中半支配点最小的点，所以(y)一定不是(sdom(w))的真后代。此外，(y)一定不是(idom(u))的真后代和(u)的祖先，否则就存在一条由(r dot o sdom(y))，(sdom(y) = v_0, v_1, dots , v_k = y(v_i lt y, forall 1 le i le k - 1))和(y dot o u)组成的路径没有经过(idom(u))，这与(idom)的定义矛盾。
由于(idom(u) dot o y dot o w)，所以只有可能(y = idom(u))。由此可得(r)到(w)的任意一条路径都经过(idom(u))，(idom(u))支配(w)，此定理得证。
推论1. 对于任意点(w)（(w
eq r)），令点(u)为所有满足(sdom(w) overset{+}{ o} u dot o w)的点(u)中(sdom(u))最小的一个，有
(idom(w) = left { egin{aligned} & sdom(w) & (sdom(u) = sdom(w)) & \ & idom(u) & (sdom(u) lt sdom(w)) & end{aligned}
ight. ag{2})
证明： 通过定理2和定理3可以直接得到。
因为(w)也是(u)的候选，所有一定有(sdom(u) le sdom(w))
接下来的定理提供了一种计算半支配点的方法。
定理4. 对于任意点(w)（(w e r)），有(sdom(w) = min({v | (v, w) in E , v lt w } cup {sdom(u) | u gt w , exists (v, w) in E , u dot o v} ) ag{3})
证明： 令(x)为((3))右边的值。我们先证明(sdom(w) le x)。假设第一种情况：(x)是满足(exists (x, w) in E, x lt w)。由((1))所以(sdom(w) le x)。另一种情况：(x = sdom(u))，(u)是满足(u gt w and exists (v, w) in E and u dot o v)的点。由((1))存在一条路径(x = v_0, v_1, dots , v_j = u)满足(v_i gt u gt w, forall 1 le i le j - 1)。树(T)上的路径(u = v_j o v_{j + 1} o dots o v_{k - 1} = v)满足(v_i ge u gt w, forall j le i le k - 1)。因此路径(x = v_0, v_1, dots , v_{k - 1} = v, v_k = w)满足(v_i gt w, forall 1 le i le k - 1)。由((1))所以(sdom(w) le x)。
接下来证明(sdom(w) ge x)。(sdom(w) = v_0, v_1, dots , v_k = w)为一条满足(v_i gt w, forall 1 le i le k - 1)的路径。当(k = 1)时，((sdom(w), w) in E)，由引理3可得(sdom(w) lt w)。因此(sdom(w) ge x)。另一种情况当(k gt 1)时，令(j)为最小的满足(1 le j le k - 1 and v_j dot o v_{k - 1})。这样的(j)存在因为(k - 1)是(j)的候选。
我们断言(v_i gt v_j, forall 1 le i le j - 1)。假设它不成立，即(exists v_i lt v_j(1 le i le j - 1))。选择满足(v_i lt v_j(1 le i le j - 1))并且(v_i)最小的(i)。由引理1（路径引理）可得(v_i overset{+}{ o} v_j)，与(j)的定义矛盾。此断言得证。
这个断言说明了(sdom(w) ge sdom(v_j) ge x)。因此当(k ge 1)时(sdom(w) ge x)，所以(x = sdom(w))，此定理得证。
来源
Lengauer T, Tarjan R E. A fast algorithm for finding dominators in a flowgraph[M]. ACM, 1979.