不动点与罢工授权
Fixed Points and Strike Mandates (2012)

原始链接: https://pvk.ca/Blog/2012/02/19/fixed-points-and-strike-mandates/

许多程序分析任务都可归结为求单调函数的固定点。在完备格上,塔斯基定理保证最小固定点和最大固定点都存在,但必须根据需求有意识地选择:从底元素开始迭代通常会逼近最小固定点,而从顶元素开始迭代则会逼近最大固定点。 死变量消除很好地说明了这一问题。将所有值都初始化为活跃,并反复删除不再活跃的值,通常只能得到不够理想的固定点,并可能遗漏循环以及其他无用计算。正确的方法是从返回、内存写入等可观察效果出发,将相关值反向标记为活跃,再正向传播活跃性;这样计算得到的是最大固定点。 罢工强制条件分析提供了一个现实示例。从已经参与的工会开始,不断扩充参与罢工的工会集合往往会趋向最小固定点,并可能导致不必要的死锁。若要找出满足所有条件的最大协同群体,就应从所有受强制条件约束的工会开始,反复删除未达到要求的工会,从而计算最大固定点。 保守初始化可以得到安全且可行的中间结果,并加快收敛速度,但可能牺牲完备性。因此,选择初始近似值——也就是选择最终要逼近的固定点——应当明确权衡准确性与性能。

# 黑客新闻 最新 | 往期 | 评论 | 提问 | 展示 | 职位 | 提交 登录 ## 不动点与罢工授权 (pvk.ca) 5 分 由 **luu** 提交 2 小时前 隐藏 | 往期 | 收藏 | 1 条评论 **帮助** **munchler** 13 分钟前 [–] 这是抽象数学直接影响现实情况的一个很酷的例子。实际上,是两个不同的酷例子,而且都解释得很清楚。很棒! 回复 考虑申请 YC 2027 年冬季班次! 申请开放至 11 月 2 日。 指南 | 常见问题 | 列表 | API | 安全 | 法律 | 申请加入 YC | 联系我们 搜索:
相关文章

原文

Many tasks in compilation and program analysis (in symbolic computation in general, I suppose) amount to finding solutions to systems of the form \(x = f(x)\). However, when asked to define algorithms to find such fixed points, we rarely stop and ask “which fixed point are we looking for?”

In practice, we tend to be interested in fixed points of monotone functions: given a partial order \((\prec)\), we have \(a \prec b \Rightarrow f(a)\prec f(b)\). Now, in addition to being a fairly reasonable hypothesis, this condition usually lets us exploit Tarski’s fixed point theorem. If the domain of \(f\) (with \(\prec\)) forms a complete lattice, so does the set of fixpoints of \(f\) ! As a corollary, there then exists exactly one least and one greatest fixed point under \(\prec\).

This is extremely useful, because we can usually define useful meet and join operations, and enjoy a complete lattice. For example, for a domain that’s the power set of a given set, we can use \(\subset\) as the order relation, \(\cup\) as join, and \(\cap\) as meet. However, what I find interesting to note is that, when we don’t pay attention to which fixpoint we wish to find, humans seem to consistently develop algorithms that converge to the least or greatest one, depending on the problem. It’s as though we all have a common blind spot covering one of the extreme fixed points.

A simple example is dead value (useless variable) elimination. When I ask people how they’d identify such variables in a program, the naïve solutions tend to be very similar. They exploit the observation that a value is useless if it’s only used to compute values that are themselves useless. The routines start out with every value live (used), and prune away useless values, until there’s nothing left to remove.

These algorithms converge to solutions that are correct, but suboptimal (except for cycle-free code). We wish to identify as many useless values as possible, to eliminate as many computations as possible. Yet, if we start by assuming that all values are live, our algorithm will fail to identify some obviously-useless values, like x in:

for (...)
  x = x

We could keep adding more special cases. However, the correct (simplest) solution is to try and identify live values, rather than dead ones. A value is live if it’s used to compute a live value. Moreover, return values and writes to memory are always live. Our routine now starts out by assuming that only the latter values are live, and adjoins live values as it finds them, until there’s nothing left to add.

In this case, the intuitive solution converges to the greatest fixed point, but we’re looking for the least fixed point. Setting the right initial value ensures convergence to the right fixed point.

Other common instances of this pattern are reference counting instead of marking, or performing type propagation by initially assigning the top type to all values (like SBCL).

# I recently found a use for fixed point computations outside of math and computer science.

Most university or CEGEP student unions in Québec will vote (or already have voted) on strike mandates to help organize protests against rising university tuition fees this winter and spring. There are hundreds of such unions across the province representing, in total, around four hundred thousand students. The vast majority of these unions comprise a couple hundred (or fewer) students, and many feel it would be counter-productive for only a tiny number of students to be on strike. Thus, strike mandates commonly include conditions regarding the minimal number of other students who also hold strike mandates, along with additional lower bounds on the number of unions and universities or colleges involved. As far as I know, all the mandates adopted so far are monotone: if they are satisfied by a set striking unions, they are also satisfied by all of its supersets.

Tarski’s theorem applies (again, with \((\subset, \cup, \cap)\) on the power set of the set of student unions). Which fixed point are we looking for?

It’s clear to me that we’re looking for the fixed point with the largest set of striking unions. In some situations, the least fixed point could trivially be the empty set (or all unions that did not adopt any lower bound). Moreover, the mandates are usually presented with an explanation to the effect that, if unions representing at least \(n_0\) students adopt the same mandate, then all unions that have adopted the mandate will go on strike simultaneously.

I asked fellow graduate students in computer science to sketch an algorithm to determine which unions should go on strike given their mandates; they started with the set of student unions currently on strike, and adjoined unions for which all the conditions were met. Such algorithms will converge toward the least fixed point. For example, there could be two unions, each comprising 5 000 students, with the same strike floor of 10 000 students, and these algorithms would have both unions deadlocked, waiting for the other to go on strike.

Instead, we should start by assuming that all the unions (with a strike mandate) are on strike, and iteratively remove unions whose conditions are not all met, until we hit the greatest fixed point. I’m fairly sure this will end up being a purely theoretical concern, but it’s a pretty neat case of abstract mathematics helping us interpret a real-world situation.

This pattern of intuitively converging toward a suboptimal solution seems to come up a lot when computing fixed points. It’s not necessarily a bad choice: conservative initial values tend to lead to faster convergence, and often have the property that intermediate solutions are always correct (feasible). When we need quick results, it may make sense to settle for suboptimal solutions. However, it ought to be a deliberate choice, rather than a consequence of failing to consider other possibilities.

联系我们 contact @ memedata.com