Fixed Points and Strike Mandates
4 days ago
- 编译和程序分析中的许多任务涉及寻找形如 x = f(x) 的方程组的不动点，但通常我们并不指明要找哪一个不动点。
- 完全格上的单调函数保证存在最小和最大不动点，这要归功于塔斯基定理，可用于定义并集和交集等运算。
- 人们通常凭直觉设计出收敛到最小或最大不动点的算法，这揭示了对另一种选择的常见盲点。
- 例如：死值消除从所有值均为活跃开始，收敛到最大不动点；但为了最小化计算量，正确的解应使用最小不动点。
- 其他例子包括引用计数与标记，以及在 SBCL 等编译器中从顶部类型开始的类型传播。
- 现实应用：魁北克学生工会的罢工授权是单调的；所需的不动点是在罢工的最大工会集合，而不是最小集合。
- 从空集（没有工会罢工）开始的算法会收敛到最小不动点，可能导致死锁；而从所有工会开始并逐步移除则效果更好。
- 保守的初始选择往往会产生更快但正确却次优的解决方案；初始值的选择应该是有意为之，而不是疏忽。