存活区间引理
前段时间写作业的时候，随手推了一个很小的引理，姑且叫它存活区间引理：对于满足任何一处对变量的使用都被这个变量的定义支配（姑且称为强定义条件）的SSA程序，任何变量的存活区间都是支配树上以定义为根的子树内，包含定义本身在内的一个连通子图。
证明是简单的：明确一下存活的定义，一个变量在某个点$P$处是存活的，当且仅当存在一条从入口出发的路径满足其依次经过变量的定义$D$、$P$和对变量的使用$U$，并且在$P$到$U$的部分没有再次经过$D$。
对于不在子树内的$P$，若变量在此是存活的，拼接一条从入口到$P$且不经过$D$的路径和上述路径的后半部分，可以发现存在$U$不被定义所支配，不符合强定义条件。
对于在子树内的$P$，首先我们证明对于任意$P’ \neq D$满足$D$支配$P’$，$P’$支配$P$，都存在一条路径从$P’$到$P$且不经过$D$。考虑反证，若任何一条从$P’$到$P$的路径都经过$D$，对于最短的这样的路径，其中从$D$到$P$的部分一定不经过$P’$（否则有一条更短的路径），既然$P’$不支配$D$，拼接路径就可以发现$P’$不支配$P$，矛盾。
然后，利用这个结论可以很容易地得出，如果变量在$P$处是存活的，则它在任意$P’$处也是存活的，因此存活区间是包含定义本身在内的一个连通子图。
弦图
几天前聊天的时候，发现这个引理和某个很酷的结论其实非常近：满足强定义条件的SSA程序的干涉图都是弦图。
利用上面的小引理，证明也是简单的：同样先明确一下干涉的定义，如果两个变量的存活区间有交，它们就互相干涉。
从存活区间引理可以看出，如果两个变量相互干涉，其中一个变量的定义必定支配另一个。也就是说，干涉图上的任意一条边都对应支配树上一条深度单调的路径，从这个结果出发对干涉图上的环分类讨论就能轻松地完成证明。
对于干涉图上的一个非三元环，记其某一顶点序列为$D_1,D_2,\cdots,D_n$，我们需要证明它一定存在一条弦。由于$D_1$和$D_n$一定存在支配关系，不妨设$D_n$支配$D_1$。
若除$D_n$之外的所有点都在以$D_1$为根的子树内，记其他这些点的最小公共祖先为$C$，考虑深度可以发现一定存在一个$1 < i < n$满足$D_i=C$，于是$D_i \neq D_1, D_i \neq D_n$，同时根据存活区间引理可以知道$D_i$和$D_1, D_n$都相互干涉，也就是它们构成一个三元环，如此便找到了弦。
否则，考虑该序列中第一个不在以$D_1$为根的子树内的顶点$D_i, 1 < i < n$，由存活区间引理可以发现$D_i$必定与$D_1$相互干涉。若$i \neq 2$，$D_1D_i$就是一条弦。否则若$i = 2$，考虑要么$D_2$支配$D_n$，要么$D_n$支配$D_2$，对两种情况应用存活区间引理都可以容易地得到$D_2D_n$是一条弦。
我还以为这个结论很难证，结果竟然这么简单，在此稍微记一下。
鸣谢
timetraveler314