利用单元探测下界分离解析表达式文法

中文摘要 AI 辅助

我们解决了关于解析表达式文法（PEG）的三个公开问题。我们构造了单一语言 $C$，满足 $C\in\mathsf{LIN}\cap\mathsf{PEG}$ 且 $C^R\in\mathsf{LIN}\setminus\mathsf{PEG}$。这证明部分线性上下文无关语言不是 PEG 语言，且 PEG 语言不关于反转封闭，证实了 Loff、Moreira 和 Reis 的猜想。利用同一实例的因式分解，我们否定了 Rubtsov 和 Chudinov 的连接封闭性问题，得到强形式 $\mathsf{PEG}\cdot\mathsf{REG}\not\subseteq\mathsf{PEG}$，尽管 $\mathsf{REG}\cdot\mathsf{PEG}\subseteq\mathsf{PEG}$。这也否定了 PEG 关于 Kleene 星、同态和替换的封闭性。我们的主要技术将脚手架自动机（SCA，其刻画 PEG 语言的反转）转换为单元探测模型中的动态数据结构。对于任何带预处理、更新和最终布尔查询的问题的适当局部序列化，SCA 识别器会产生精确的确定性单元探测数据结构，其操作代价与对应编码长度成比例。因此，单元探测下界可证明 SCA 的非成员性，并通过反转证明 PEG 的非成员性。我们将此转换应用于多相内积，使用单符号更新块和长度为 $O(\log n)$ 的查询后缀，同时保持该语言及其反转均为线性上下文无关。Ko 的单元探测下界随后得出上述实例。相关论证还在 Lean 4 中完成了形式化。

英文摘要

We resolve three open problems concerning parsing expression grammars (PEGs). We construct a single language $C$ satisfying $C\in\mathsf{LIN}\cap\mathsf{PEG}$ and $C^R\in\mathsf{LIN}\setminus\mathsf{PEG}$. This proves that some linear context-free language is not a PEG language and that PEG languages are not closed under reversal, confirming a conjecture of Loff, Moreira, and Reis. Factoring the same witness resolves the concatenation-closure problem of Rubtsov and Chudinov negatively, in the strong form $\mathsf{PEG}\cdot\mathsf{REG}\not\subseteq\mathsf{PEG}$ despite $\mathsf{REG}\cdot\mathsf{PEG}\subseteq\mathsf{PEG}$. It also refutes closure under Kleene star, homomorphisms, and substitutions. Our main technique converts scaffolding automata (SCAs), which characterize reversals of PEG languages, into dynamic data structures in the cell-probe model. For any suitably local serialization of a problem with preprocessing, updates, and a final Boolean query, an SCA recognizer yields an exact deterministic cell-probe data structure whose operation costs are proportional to the corresponding encoding lengths. Cell-probe lower bounds can therefore prove SCA non-membership and, by reversal, PEG non-membership. We apply this transfer to Multiphase Inner Product using one-symbol update blocks and a query suffix of length $O(\log n)$, while keeping both the language and its reversal linear context-free. Ko's cell-probe lower bound then yields the witness above. The arguments are additionally formalized in Lean 4.

发表机构

• Korea University（韩国大学）

机构由 AI 辅助整理，请以论文原文为准。