Separating Parsing Expression Grammars using Cell-Probe Lower Bounds
Programming LanguagesComputational ComplexityFormal Languages and Automata Theory
Summary
The authors solve three known problems about parsing expression grammars (PEGs) by creating a special language that is both linear context-free and a PEG language, but whose reversed version is not a PEG language. This shows that PEG languages do not always behave nicely when reversed and are not closed under some operations like concatenation, Kleene star, or substitutions. They use a new method linking PEGs to a computational model called scaffolding automata and cell-probe data structures to prove these results rigorously. Their approach also includes formal verification of the arguments in a proof assistant called Lean 4.
Authors
Jungyeom Kim, Jihyeok Park
Abstract
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.