paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Separation for dot-depth two

dot-depth 2 的分离
LMCS vol.Volume 17, Issue 32021匹配度 1/10 · 该论文研究自动机理论与描述复杂性中的 dot-depth/拼接层级分离问题,与用户关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析均无直接交集;虽然形式化程度高,但不涉及程序分析或机器学习系统。引用 3 inbox
Thomas Place, Marc Zeitoun
crossref: 2026-09-10

AI 速览

一句话:为 dot-depth 2 给出分离算法,并证明基有限的拼接层级第一层分离可判定。

dot-depth 层级刻画星自由语言与一阶可定义语言,其各层对应一阶量词交替块数;判定给定正则语言是否属于某一层(membership)是自动机理论著名难题,目前仅低层已知。本文转向更一般的分离问题:给定两个语言,判定是否存在该层语言包含第一个且与第二个不相交。作者为 dot-depth 2 设计了分离算法;更一般地,证明对任意基为有限的拼接层级,第一层分离可判定,再结合已有结果将其提升到 dot-depth 2。

问题
dot-depth 层级与一阶量词交替层级对应,但各层 membership 是否可判定长期未决,低层之外缺乏算法。
方法
把 membership 推广为分离问题,针对拼接层级设计算法;证明基为有限的拼接层级第一层分离可判定,并利用已有结果提升到 dot-depth 2。
评估
以可判定性定理与分离算法为结果,主要应用是 dot-depth 2;评估为理论证明而非实验。
原文摘要(Abstract)

The dot-depth hierarchy of Brzozowski and Cohen classifies the star-free languages of finite words. By a theorem of McNaughton and Papert, these are also the first-order definable languages. The dot-depth rose to prominence following the work of Thomas, who proved an exact correspondence with the quantifier alternation hierarchy of first-order logic: each level in the dot-depth hierarchy consists of all languages that can be defined with a prescribed number of quantifier blocks. One of the most famous open problems in automata theory is to settle whether the membership problem is decidable for each level: is it possible to decide whether an input regular language belongs to this level? Despite a significant research effort, membership by itself has only been solved for low levels. A recent breakthrough was achieved by replacing membership with a more general problem: separation. Given two input languages, one has to decide whether there exists a third language in the investigated level containing the first language and disjoint from the second. The motivation is that: (1) while more difficult, separation is more rewarding (2) it provides a more convenient framework (3) all recent membership algorithms are reductions to separation for lower levels. We present a separation algorithm for dot-depth two. While this is our most prominent application, our result is more general. We consider a family of hierarchies that includes the dot-depth: concatenation hierarchies. They are built via a generic construction process. One first chooses an initial class, the basis, which is the lowest level in the hierarchy. Further levels are built by applying generic operations. Our main theorem states that for any concatenation hierarchy whose basis is finite, separation is decidable for level one. In the special case of the dot-depth, this can be lifted to level two using previously known results.

链接与引用

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

BibTeX
@article{paperbot1277,
  title = {Separation for dot-depth two},
  author = {Thomas Place and Marc Zeitoun},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 17, Issue 3},
  year = {2021},
  doi = {10.46298/lmcs-17(3:24)2021}
}