一句话:证明阿贝尔群/半群求和问题在带计数固定点逻辑 FPC 中可定义,且计数算子不可去除。
本文研究阿贝尔半群与群上求和问题的描述复杂度。输入由乘法表表示的阿贝尔半群 G 和子集 X 给出,需计算 X 中元素之和。若有线性顺序,该问题算法上很平凡;但在无序抽象结构上,同构不变的多项式时间模型难以逐个处理元素,因此其逻辑可定义性十分微妙,并引出 Rossman 关于 CPT 能否定义该问题的长期问题。作者证明该问题可在带计数固定点逻辑 FPC 中定义,采用动态规划并充分使用计数机制;由于 FPC 包含于 CPT,这回答了 Rossman 的问题。作者还给出匹配下界:即使在阿贝尔群上,该问题也不能在无计数的纯固定点逻辑中定义,证明基于概率论证。
We study the descriptive complexity of summation problems in Abelian groups and semigroups. In general, an input to the summation problem consists of an Abelian semigroup G, explicitly represented by its multiplication table, and a subset X of G. The task is to determine the sum over all elements of X. Algorithmically this is a very simple problem. If the elements of X come in some order, then we can process these elements along that order and calculate the sum in a trivial way. However, what makes this fundamental problem so interesting for us is that from the viewpoint of logical definability its tractability is much more delicate. If we consider the semigroup G as an abstract structure and X as an abstract set, without a linear order and hence without a canonical way to process the elements one by one, then it is unclear how to define the sum in any logic that does not have the power to quantify over a linear order. Indeed the trivial summation algorithm cannot be expressed in any polynomial-time logic or, in fact, in any computational model which works on abstract mathematical structures in an isomorphism-invariant way without violating polynomial resource bounds. The surprising difficulty, in terms of logical definability, of this basic mathematical problem is the reason why Ben Rossman asked, more than ten years ago, whether it can be expressed in the logic Choiceless Polynomial Time with counting (CPT). Note that, to date, CPT is one of the most powerful known candidates for a logic that might be capable of defining every polynomial-time property of finite structures. In this paper we clarify the status of the definability for the summation problem for Abelian groups and semigroups in important polynomial-time logics. In our first main result we show that the problem can be defined in fixed-point logic with counting (FPC). Since FPC is contained in CPT this settles Rossman's question. Our proof is based on a dynamic programming approach and heavily uses the counting mechanism of FPC. In our second main result we give a matching lower bound and show that the use of counting operators cannot be avoided: the summation problem, even over Abelian groups, cannot be defined in pure fixed-point logic without counting. Our proof is based on a probabilistic argument.