paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Characterization and Decidability of FC-Definable Regular Languages

FC-可定义正则语言的刻画与可判定性
LICS 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2025匹配度 1/10 · 该论文研究 FC 逻辑可定义正则语言的理论刻画，属于纯形式语言与自动机理论，与用户关注的可编程语言静态分析、浮点/贝叶斯程序分析以及 LLM/Agent 与静态分析/形式化验证的交叉均无直接关联。引用 0 inbox
Sam M. Thompson, Nicole Schweikardt, Dominik D. Freydenberger
逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：证明存在非 FC-可定义的正则语言，并给出 FC-可定义正则语言的可判定刻画与表达式形式。

论文研究一阶逻辑 FC 可定义的语言类，其中 FC 可借助连接量词考察有限词的所有因子，并已能定义如 ww 之类的非正则语言。作者首先证明并非所有正则语言都能由 FC 定义，从而区分 FC-可定义语言与正则语言。随后，他们从代数、自动机和正则表达式三个角度给出 FC-可定义正则语言的精确且可判定的特征刻画；在表达式层面，该刻画可自然简洁地表述为：在无星广义正则表达式上加入 terminal words 的 Kleene 星。该结果明确了 FC 在正则语言范围内的表达能力，并提供了判定某正则语言是否 FC-可定义的途径。

问题
确定哪些正则语言可由 FC 定义，并判断该语言类是否具有可判定刻画。
方法
结合代数特征、自动机刻画与正则表达式，对 FC-可定义正则语言进行分类，并证明其可判定性；同时证明存在非 FC-可定义的正则语言。
评估
以数学证明和构造性刻画为主要论证方式，给出的正则表达式刻画为无星广义正则表达式扩展 terminal words 的 Kleene 星。
原文摘要（Abstract）

FC is a first-order logic that reasons over all factors of a finite word using concatenation, and can define non-regular languages like that of all squares (ww). In this paper, we establish that there are regular languages that are not FC-definable. Moreover, we give a decidable characterization of the FC-definable regular languages in terms of algebra, automata, and regular expressions. The latter of which is natural and concise: Star-free generalized regular expressions extended with the Kleene star of terminal words.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot8624,
  title = {Characterization and Decidability of FC-Definable Regular Languages},
  author = {Sam M. Thompson and Nicole Schweikardt and Dominik D. Freydenberger},
  booktitle = {LICS},
  year = {2025},
  doi = {10.1109/lics65433.2025.00033}
}