关于Dataflow Analysis中不同节点遍历顺序的Iterative Solver结果相等的证明
以下以may analysis为例，must analysis基本同理，区别主要在于是$\sqsupseteq$还是$\sqsubseteq$。
注意
以下谈到的所有$F$，首先要满足是safe的，包括transfer function设计合理并且每一轮中每个node都需要（至少）被visit过一次。 注意这一点的意义在于你可以说我有一个$F$，transfer function或者每轮遍历内容为空，那么bottom就是它的最小不动点，但这显然不是我们想要的。
记号
代表整个程序状态的完全格$L$，完全格的信息不仅有所有OUT, 还有所有IN；每一轮对$L$的映射记为$F: L \rightarrow L$。 分别代表两个不同轮内遍历顺序的$F_1$, $F_2$。
对于visit到一个node时发生的事情，有以下步骤：merge所有前驱的out到in，然后OUT = transfer(IN)。
由于merge函数具有可交换性，所以visit到一个node时merge的顺序对于遍历完一个node之后的结果无影响。（也可以认为遍历一个node是一个原子操作）
所以任意取一个每一次merge动作和transfer动作也可以看成是一个原子操作$f: L \rightarrow L$。
所以一个有k个前驱的node $i$被visit的动作的形式化写法可以写成下面形式（记visit前的程序状态格为$L_o$, visit之后为$L_r$）:
$L_r = f_{transfer_i} \circ f_{merge_{i,k}} \circ … \circ f_{merge_{i,1}} (L_o)$，复合函数记为$L_r = f_{node_i} (L_o)$
其中的$f_{transfer_i}$代表transfer，$f_{merge_{i,j}}$代表前驱j的OUT merge到当前node的IN中。
记号部分整理完毕，现在开始正式的证明。
Iterative Solver最小不动点相等的证明
在iterative solver中，一轮迭代分解为对node以某个顺序遍历，所以对于一个有n个node的CFG的第$i$轮遍历，可以写成
$L_{i} = f_{node_n} \circ … \circ f_{node_1} (L_{i-1})$，$F$即为复合函数$f_{node_n} \circ … \circ f_{node_1}$, $L_{i} = F(L_{i-1})$
整理一下，$F = f_{node_n} \circ … \circ f_{node_1}$ $= (f_{transfer_n} \circ f_{merge_{n,k}} \circ … \circ f_{merge_{n,1}}) \circ … \circ (f_{transfer_1} \circ f_{merge_{1,k}} \circ … \circ f_{merge_{1,1}})$ $= f_{transfer_n} \circ f_{merge_{n,k}} \circ … \circ f_{merge_{n,1}} \circ … \circ f_{transfer_1} \circ f_{merge_{1,k}} \circ … \circ f_{merge_{1,1}}$
首先，上面出现的每一个映射，无论是$F$还是某个原子函数$f$，都是在$L$上的单调函数。
对于$F_1$的任一不动点$p_1$，有$p_1 = F_1(p_1) = f_{transfer_n} \circ f_{merge_{n,k}} \circ … \circ f_{merge_{n,1}} \circ … \circ f_{transfer_1} \circ f_{merge_{1,k}} \circ … \circ f_{merge_{1,1}}(p_1)$，
根据原子函数的单调性可得，$p_1$ apply每一个原子函数$f$的结果都是$p_1$。
对于另一个顺序遍历的函数$F_2$，他也是由$F_1$中的原子函数$f$以不同顺序构成，即
$F_2 = f_s \circ … \circ f_1$，
原子函数存在一个一一映射:
${f_1, …, f_s} \rightarrow \cup_{i \in {1, …, n}} ({f_{transfer_i}} \cup {f_{merge_{i, k}}, …, f_{merge_{i, 1}}})$
下面的记法与上面等价：
${f_1, …, f_s} \rightarrow \cup_{i \in {1, …, n}} ({f_{transfer_i}} \cup (\cup_{k \in 节点i的前驱节点的标号集合} {f_{merge_{i, k}}}))$
所以$p_1 = F_2(p_1)$，$p_1$是$F_2$的不动点。
同理，$F_2$的任意一个不动点$p_2$是$F_1$的不动点。
所以两个$F$的不动点集合相等，二者有同一个最小不动点。
Q.E.D.
WorkList Solver与Iterative Solver最小不动点相等的证明
TODO.
暂时还没时间细想，但是可能是可以证明对于一个类似Iterative Solver，但每一轮中遍历顺序不同的Solver，只要是到达不动点，那么这个不动点就是所有Iterative Solver的不动点。 然后证明WorkList Solver由于相当于去掉了上述Solver的遍历序列中对$L$没有影响的$f_{node_i}$而得到的遍历序列，从而最后结果也是最小不动点。
对WorkList算法的可能优化
TODO.