paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Definability of summation problems for Abelian groups and semigroups

阿贝尔群与半群求和问题的可定义性
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 1/10 · 该论文属于描述复杂性/逻辑可定义性理论,研究阿贝尔群/半群求和问题在 FPC 中的可定义性,与用户关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析均无直接关联。它可能仅与形式化验证的逻辑基础有非常间接的联系,但并非问题画像中的核心方向。引用 5 inbox
Faried Abu Zaid, Anuj Dawar, Erich Gradel, Wied Pakusa
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:证明阿贝尔群/半群求和问题在带计数固定点逻辑 FPC 中可定义,且计数算子不可去除。

本文研究阿贝尔半群与群上求和问题的描述复杂度。输入由乘法表表示的阿贝尔半群 G 和子集 X 给出,需计算 X 中元素之和。若有线性顺序,该问题算法上很平凡;但在无序抽象结构上,同构不变的多项式时间模型难以逐个处理元素,因此其逻辑可定义性十分微妙,并引出 Rossman 关于 CPT 能否定义该问题的长期问题。作者证明该问题可在带计数固定点逻辑 FPC 中定义,采用动态规划并充分使用计数机制;由于 FPC 包含于 CPT,这回答了 Rossman 的问题。作者还给出匹配下界:即使在阿贝尔群上,该问题也不能在无计数的纯固定点逻辑中定义,证明基于概率论证。

问题
研究阿贝尔半群/群上的求和问题在多项式时间逻辑中是否可定义,特别回答 Rossman 提出的 CPT 可定义性问题。
方法
利用 FPC 的计数能力设计动态规划定义,并用概率方法证明无计数固定点逻辑的不可定义性下界。
评估
通过逻辑可定义性证明进行评估:给出 FPC 上界,并给出无计数固定点逻辑下界,从而精确刻画该问题的逻辑复杂度。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · DBLP

BibTeX
@inproceedings{ZaidDGP17,
  title = {Definability of summation problems for Abelian groups and semigroups},
  author = {Faried Abu Zaid and Anuj Dawar and Erich Gradel and Wied Pakusa},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005082}
}