Separating Parsing Expression Grammars using Cell-Probe Lower Bounds
Jungyeom Kim, Jihyeok Park
cs.PL
Aug 30, 2026 · v1
cs.CC cs.FL
TL;DR
All main separation and closure-property results for parsing expression grammars are formally verified in Lean 4, with dependent axioms tracked.
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.
Problem
Several open problems about parsing expression grammars (PEGs) remained unresolved: whether every linear context-free language is a PEG language, whether PEG languages are closed under reversal, and whether they are closed under concatenation and Kleene star.
Approach
A transfer framework converts scaffolding automata (SCAs), which characterize reversals of PEG languages, into cell-probe data structures where each transition uses O(1) probes. Cell-probe lower bounds then prove SCA non-membership and, by reversal, PEG non-membership. The framework is applied to Multiphase Inner Product using Ko's cell-probe lower bound. All main results are formalized and checked in Lean 4, with explicit budget functions replacing asymptotic notation and dependent axioms reported.
Results
A witness language C is constructed with C in LIN∩PEG but C^R in LIN∖PEG, proving LIN⊄PEG and non-closure under reversal. The same witness refutes closure under concatenation (PEG·REG⊄PEG while REG·PEG⊆PEG), Kleene star, homomorphisms, and substitutions.