paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A crevice on the Crane Beach: Finite-degree predicates

Crane Beach 上的一道裂缝:有限度谓词
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 1/10 · 该论文属于逻辑与自动机理论,研究单词上一阶逻辑的表达力与 Crane Beach 性质,与用户关注的程序静态分析、LLM/Agent 辅助形式化验证、浮点程序分析及贝叶斯程序分析均无直接关联。虽涉及形式化逻辑,但不对应其研究问题或应用场景。引用 2 inbox
Michael Cadilhac, Charles Paperman
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:证明 FO[A_RB] 与 FO[≤, MSB0, F_IN] 等表达,且 FO[≤, F_IN] 和 FO[≤, MSB0] 满足强 Crane Beach 性质。

该论文研究词上的一阶逻辑(FO)在数值谓词扩展下的表达力与 Crane Beach 性质(CBP)。作者证明 FO[A_RB] 与仅含序、二元 MSB0 谓词和有限度谓词的 FO[≤, MSB0, F_IN] 等表达。CBP 要求所有含中性字母的可表达语言都是正则的;已知 FO[A_RB] 不满足 CBP,但本文证明 FO[≤, F_IN] 与 FO[≤, MSB0] 满足强 CBP。因此 FO[≤, F_IN] 同时具有局部性和 CBP,能表达大量语言,却仅比 FO[A_RB] 少一个简单谓词。最后将其计数能力作为应用进行了研究。

问题
词上一阶逻辑的数值谓词扩展(尤其 FO[A_RB] 及有限度谓词)的表达力边界与 Crane Beach 性质是否成立。
方法
通过逻辑等表达证明和强 CBP 的证明,比较 FO[A_RB] 与 FO[≤, MSB0, F_IN] 等系统的表达力,并分析其计数能力。
评估
以可表达语言类与正则性判据(中性字母下 CBP)为理论评估标准,给出等表达定理和强 CBP 结果。
原文摘要(Abstract)

First-order logic (FO) over words is shown to be equiexpressive with FO equipped with a restricted set of numerical predicates, namely the order, a binary predicate MSB<inf>0</inf>, and the finite-degree predicates: FO[A<inf>RB</inf>] = FO[≤, MSB<inf>0</inf>, F<inf>IN</inf>]. The Crane Beach Property (CBP), introduced more than a decade ago, is true of a logic if all the expressible languages admitting a neutral letter are regular. Although it is known that FO[A<inf>RB</inf>] does not have the CBP, it is shown here that the (strong form of the) CBP holds for both FO[≤, F<inf>IN</inf>] and FO[≤, MSB<inf>0</inf>]. Thus FO[≤, F<inf>IN</inf>] exhibits a form of locality and the CBP, and can still express a wide variety of languages, while being one simple predicate away from the expressive power of FO[A<inf>RB</inf>]. The counting ability of FO[≤, F<inf>IN</inf>] is studied as an application.

链接与引用

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

BibTeX
@inproceedings{CadilhacP17,
  title = {A crevice on the Crane Beach: Finite-degree predicates},
  author = {Michael Cadilhac and Charles Paperman},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005148}
}