paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Simulating Logspace-Recursion with Logarithmic Quantifier Depth

用对数级量词深度模拟对数空间递归
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 1/10 · 该论文属于有限模型论与描述复杂性,研究 LREC= 的逻辑表达力及 Weisfeiler–Leman 轮数刻画,与用户关注的静态分析、程序验证、浮点/贝叶斯程序分析以及 LLM 与程序分析交叉均无直接关系。引用 2 inbox
Steffen van Bergerem, Martin Grohe, Sandra Kiefer, Luca Oeljeklaus
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:证明 LREC= 可定义性质可由 k 变量 FO+C 以对数数量词深度表达,并给出 Weisfeiler–Leman 对数轮数刻画。

论文研究描述复杂性中用于刻画对数空间可判定问题的逻辑 LREC=,它在带计数的一阶逻辑 FO+C 上加入受限递归算子。作者证明:每个 LREC= 可定义性质都存在常数 k,使带计数量词的 k 变量一阶逻辑能以对数数量词深度表达该性质。其方法通过逻辑模拟和量词深度分析,将递归展开压缩到对数深度。由此推出,被该性质区分的图对可在对数次迭代内由 k 维 Weisfeiler–Leman 算法区分;特别地,常数维 WL 能在对数次迭代内识别区间图与无爪弦图,因为它们具有 LREC= 可定义的规范化。

问题
如何用有限变量与对数数量词深度的计数一阶逻辑模拟 LREC= 的受限对数空间递归,并刻画其图区分能力。
方法
通过构造 LREC= 公式到 k 变量 FO+C 公式的翻译,分析量词深度,将递归模拟限制在对数深度;再将该逻辑刻画联系到 Weisfeiler–Leman 算法的迭代。
评估
理论证明:给出一般性翻译定理,并推导出 k 维 WL 在对数次迭代内区分相应图对;应用于区间图和无爪弦图的识别。
原文摘要(Abstract)

The fixed-point logic LREC= was developed by Grohe et al. (CSL 2011) in the quest for a logic to capture all problems decidable in logarithmic space. It extends FO+C, first-order logic with counting, by an operator that formalises a limited form of recursion. We show that for every LREC=-definable property on relational structures, there is a constant k such that the k-variable fragment of first-order logic with counting quantifiers expresses the property via formulae of logarithmic quantifier depth. This yields that any pair of graphs separable by the property can be distinguished with the k-dimensional Weisfeiler–Leman algorithm in a logarithmic number of iterations. In particular, it implies that a constant dimension of the algorithm identifies every interval graph and every chordal claw-free graph in logarithmically many iterations, since every such graph admits LREC=-definable canonisation.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{BergeremGKO23,
  title = {Simulating Logspace-Recursion with Logarithmic Quantifier Depth},
  author = {Steffen van Bergerem and Martin Grohe and Sandra Kiefer and Luca Oeljeklaus},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175818}
}