Fixed Points and Strike Mandates
4 days ago
- Many tasks in compilation and program analysis involve finding fixed points of systems like x = f(x), but often we don't specify which fixed point we seek.
- Monotone functions on complete lattices guarantee a least and greatest fixed point, thanks to Tarski's theorem, useful for defining operations like union and intersection.
- Humans often intuitively develop algorithms that converge to the least or greatest fixed point, revealing a common blind spot for the alternative.
- Example: dead value elimination starts with all values live, converging to the greatest fixed point, but the correct solution for minimizing computations uses the least fixed point.
- Other examples include reference counting vs. marking, and type propagation starting with top type in compilers like SBCL.
- Real-world application: Québec student union strike mandates are monotone; the desired fixed point is the largest set of unions on strike, not the least.
- Algorithms starting with the empty set (no unions on strike) converge to the least fixed point, potentially leading to deadlocks, while starting with all unions and removing works better.
- Conservative initial choices often yield faster, correct-but-suboptimal solutions; the choice of initial value should be deliberate, not an oversight.