paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The amazing mixed polynomial closure and its applications to two-variable first-order logic

令人惊奇的混合多项式闭包及其在二变量一阶逻辑中的应用
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 2/10 · 论文属于形式语言与自动机理论,研究多项式闭包与二变量一阶逻辑 FO2 的可判定性,是纯逻辑理论工作。用户研究方向聚焦于静态分析、Agentic 程序分析、LLM 与形式化验证/浮点/贝叶斯程序分析的交叉,本文未涉及程序分析、LLM/Agent 或工程实现,与核心方向基本无关。引用 3 inbox
Thomas Place
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:提出混合多项式闭包 MPol,证明其保持成员与分离可判定性,并用于 FO2 量词交替层级。

本文研究正则语言类上的多项式闭包算子,引入左、右、混合三种限制,其中混合多项式闭包 MPol 为新定义。针对成员问题(给定正则语言是否属于某类)与分离问题(是否存在该类中同时包含第一个语言且与第二个语言不相交的语言),作者证明 LPol、RPol 与 MPol 在较弱假设下保持成员可判定性,在更强假设下保持分离可判定性。随后将其应用于语言理论层级与二变量一阶逻辑 FO2 的量词交替层级:这些层级可几乎完全用 MPol 定义,且可用 MPol 逐级攀升,结果对多数标准签名具有一般性。由此证明多数签名下 FO2 各级成员可判定,并证明仅含线性序的 FO2(<) 的分离问题可判定。

问题
如何用多项式闭包算子刻画正则语言类,并判定正则语言是否属于闭包生成的类(成员问题)以及两个正则语言能否被该类中的语言分离(分离问题)。
方法
定义左、右、混合多项式闭包 LPol/RPol/MPol,在温和或更强假设下证明其保持成员与分离可判定性,并用于语言理论层级和 FO2 量词交替层级。
评估
以理论证明为主:给出保可判定性的定理,推导 FO2 多数标准签名下逐级成员可判定,以及 FO2(<) 的分离可判定。
原文摘要(Abstract)

Polynomial closure is a standard operator which is applied to a class of regular languages. In this paper, we investigate three restrictions called left (LPol), right (RPol) and mixed polynomial closure (MPol). The first two were known while MPol is new. We look at two decision problems that are defined for every class . Membership takes a regular language as input and asks if it belongs to . Separation takes two regular languages as input and asks if there exists a third language in including the first one and disjoint from the second. We prove that LPol, RPol and MPol preserve the decidability of membership under mild hypotheses on the input class, and the decidability of separation under much stronger hypotheses. We apply these results to natural hierarchies. First, we look at several language theoretic hierarchies that are built by applying LPol, RPol and MPol recursively to a single input class. We prove that these hierarchies can actually be defined using almost exclusively MPol. We also consider quantifier alternation hierarchies for two-variable first-order logic (FO2) and prove that one can climb them using MPol. The result is generic in the sense that it holds for most standard choices of signatures. We use it to prove that for most of these choices, membership is decidable for all levels in the hierarchy. Finally, we prove that separation is decidable for the hierarchy of two-variable first-order logic equipped with only the linear order (FO2(<)).

链接与引用

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

BibTeX
@inproceedings{Place22,
  title = {The amazing mixed polynomial closure and its applications to two-variable first-order logic},
  author = {Thomas Place},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3532410}
}