PaperlayerView exact revision on arXiv

Source-linked AI summary

Separating Parsing Expression Grammars using Cell-Probe Lower Bounds

Jungyeom Kim, Jihyeok Park

arXiv:2608.29592v1cs.PLcs.CCcs.FL

TL;DR

The paper addresses whether every context-free language is PEG-recognizable and whether PEGs are closed under reversal. It transfers SCA recognition to cell-probe data structures, then uses a lower bound to establish a linear context-free language outside PEG and additional closure failures.

  • Problem

    Whether every context-free language is recognized by a PEG and whether PEG languages are closed under reversal remain open questions.

    Source: §1 · pp. 1–2

  • Method

    The paper converts suitably local SCA encodings of three-stage data-structure problems into exact deterministic cell-probe structures, enabling lower bounds to establish PEG non-membership by reversal.

    Source: §1 · pp. 2–3

  • Results

    C ∈ LIN ∩ PEG and C^R ∈ LIN \ PEG, and PEG languages are not closed under reversal, concatenation, Kleene star, homomorphisms, or substitutions.

    Source: §6 · p. 23, §5.3 · p. 23

  • Takeaways & Limitations

    The witness shows that the boundary between linear context-free languages and PEG languages is nontrivial.

    Source: §6 · pp. 23–24

    The transfer method establishes non-membership only when a language is connected to a data-structure problem with a suitable lower bound; it does not identify an intrinsic obstruction within SCAs.

    Source: §6 · p. 23

Abstract

from arXiv · show

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.

1 Introduction

The introduction frames two open questions about whether context-free languages fit within PEGs and whether PEGs are closed under reversal. It presents a linear context-free witness, a cell-probe transfer framework for proving PEG non-membership, and further negative closure results.

1 Introduction

  • PEG non-membership is difficult to establish because no comparably effective general technique is known, and PEGs lack a pumping lemma analogous to the context-free one.Existing translations into PEGs cover only restricted context-free grammar subclasses.Source: §1 · p. 2
  • An SCA encoding of a three-stage data-structure problem yields an exact deterministic cell-probe structure with word size Θ(log n) and operation costs tied to encoding lengths.Contrapositively, cell-probe lower bounds establish SCA non-membership and, by reversal, PEG non-membership.Source: §1 · pp. 2–3
  • The Multiphase Inner Product encoding uses constant-length update blocks and an O(log n)-length query suffix, while its language and reversal are both linear context-free.Ko's lower bound supplies the query-time separation used for the witness.Source: §1 · p. 3
  • C ∈ LIN ∩ PEG while C^R ∈ LIN \ PEG, showing some linear context-free languages are not PEG languages and PEGs are not closed under reversal.The paper also concludes that not every context-free language is recognized by a PEG.Source: §1 · p. 3
  • The same witness refutes PEG closure under concatenation and Kleene star, and further implies non-closure under homomorphisms and substitutions.Concatenation fails even in the strong form PEG · REG ⊈ PEG.Source: §1 · p. 3
  • The separation argument for the witness language is additionally formalized in Lean 4.The paper says the formalization's scope and trust assumptions are described in its Formal Verification section.Source: §1 · p. 3

2 Preliminaries

The preliminaries establish notation and the relevant grammar classes, then define PEGs, scaffolding automata, and the cell-probe model. They state the PEG–SCA reversal characterization that supports the paper's lower-bound strategy.

2.1 Notation; 2.2 Context-Free Grammars and Linear Languages

  • For a language L, L^R denotes the set of reversals of its words; a context-free grammar is linear when each production has at most one nonterminal on its right-hand side.LIN is the class of languages generated by linear context-free grammars.Source: §2.1 · p. 3, §2.2 · pp. 3–4

2.3 Parsing Expression Grammars

  • A PEG defines deterministic recognition using parsing expressions, including prioritized choice and lookahead; the paper's PEG language convention requires consuming the whole input.Under prioritized choice, the second expression is attempted only if the first fails; the paper notes that the full-consumption convention does not change the class recognized by total PEGs.Source: §2.3 · pp. 4–5

2.4 Scaffolding Automata

  • An SCA appends scaffold nodes as it reads input, with each node's edges pointing to earlier nodes or itself, and its transitions inspect a bounded-radius neighborhood.The characterization states L ∈ PEG exactly when L^R ∈ SCA, so K ∉ SCA implies K^R ∉ PEG.Source: §2.4 · pp. 5–6

2.5 Cell-Probe Model

  • In the deterministic cell-probe model, preprocessing initializes persistent memory and update and query procedures access it through reads and writes, each counted as one probe.The model measures worst-case probes per operation, uses word size Θ(log n), and permits polynomially many addressable cells.Source: §2.5 · p. 7

3 The SCA–Cell-Probe Transfer Framework

The framework serializes three-stage Boolean problems as languages and uses SCA recognition to model their processing as cell-probe operations. Its transfer theorem and the PEG–SCA characterization turn cell-probe lower bounds into PEG non-membership results.

3.1 Three-Stage Problems and SCA Encodings

  • Three-stage problems serialize preprocessing, updates, and a final query as strings whose membership records whether the query answer is 1.The update and query encoders are local to each operation; query-independent processing leaves a scaffold snapshot before the query begins.Source: §3.1 · pp. 7, 9

3.2 The Transfer Theorem

  • A fixed SCA transition can be simulated with O(1) probes by exploring a constant-size pointer neighborhood, while read-only query nodes stay in a local overlay.The overlay is discarded after the query simulation, leaving persistent memory unchanged.Source: §3.2 · pp. 9–10
  • The transfer theorem turns an SCA recognizer into an exact deterministic cell-probe structure with Θ(log n)-bit words, O(a(n)) updates, O(b(n)) queries, and polynomial space.The returned bit is the required value of the problem's Boolean function.Source: §3.2 · p. 10

3.3 From Cell-Probe Lower Bounds to PEG Lower Bounds

  • If no exact deterministic cell-probe structure meets the transfer bounds, the encoding's reversal is outside PEG by the PEG–SCA characterization.The next step applies this principle to Multiphase Inner Product and establishes the needed encoding and language properties.Source: §3.3 · p. 11

4 Separation via Multiphase Inner Product

The section establishes a language C in LIN ∩ PEG whose reversal is linear context-free but not in PEG. It presents the witness and its PEG membership test, and uses a reduction from Multiphase Inner Product and its cell-probe lower bound to show non-membership of the reversal.

4 Separation via Multiphase Inner Product

  • C ∈ LIN ∩ PEG while C^R ∈ LIN \ PEG, so some linear context-free language is not a PEG language and PEG languages are not closed under reversal.The non-membership follows by combining an SCA encoding of Multiphase Inner Product with Ko’s cell-probe lower bound; explicit grammars establish the membership results.Source: §4 · p. 11

4.1 The Original Multiphase Problem

  • The original Multiphase Problem preprocesses sets, receives a set T for updates, then reveals an index whose set must be tested for disjointness with T.In its original word-RAM formulation, the Phase II processing budget is total, corresponding to amortized per-coordinate updates followed by one query.Source: §4.1 · p. 11

4.2 Multiphase Inner Product and Its Lower Bound

  • Multiphase Inner Product separates preprocessed vectors, coordinate-by-coordinate updates to a second vector, and a final query selecting the vector for an inner-product test.The section uses N(n) = n^2, with update cost charged per coordinate and a query index representable using Θ(log n) bits.Source: §4.2 · p. 12
  • For N(n) = n^2, no exact deterministic cell-probe structure has word size Θ(log n), tu = O(1), tq = O(log n), and polynomial space.Ko’s lower bound [9] exceeds the logarithmic query threshold required by the transfer argument; the separation needs an ω(log n) query lower bound under polylogarithmic updates.Source: §4.2 · pp. 12–13

4.3 The Witness Language

  • The record-first witness language C is linear context-free, as is its reversal; membership in C requires a record matching the reversed query key and having odd payload-update inner product.The linear grammar chooses a witness record and matches its key and payload against the query and update vector.Source: §4.3 · pp. 13, 15

4.4 A PEG for the Record-First Language

  • An explicit total PEG for C searches records left to right, trying each as a witness before consuming it and continuing when the attempt fails.Nested key and parity scanners test the reversed key match and equal-length odd inner product; correctness tracks both successful inputs and their unconsumed suffixes.Source: §4.4 · pp. 15–17
  • A total PEG recognizes C, and the PEG–SCA characterization gives C^R ∈ SCA.The Hit expression terminates and succeeds exactly when its witness fields satisfy the key, length, and inner-product conditions.Source: §4.4 · p. 17

4.5 The Hard Encoding and Separation

  • An SCA for C would yield a cell-probe data structure for Multiphase Inner Product that violates Ko’s lower bound, proving C ∉ SCA and C^R ∉ PEG.The excluded structure has word size Θ(log n), update cost O(1), query cost O(log n), and space n^O(1).Source: §4.5 · pp. 18–19
  • The hard word W_n(S, x, q) belongs to C exactly when ⟨S_q, x⟩ over F_2 equals 1.The encoding’s key and payload fields isolate the queried index q and its inner product with x.Source: §4.5 · p. 18
  • C is an (a, β)-SCA encoding of Multiphase Inner Product with N(n) = n^2, a(n) = 1, and β(n) = O(log n).Each update block has length one, and the query suffix has logarithmic length.Source: §4.5 · p. 18
  • C ∈ PEG and C^R ∈ LIN \ PEG, so LIN ⊄ PEG and PEG is not closed under reversal, confirming the conjecture of Loff, Moreira, and Reis.The paper also states that CFL ⊄ PEG.Source: §4.5 · p. 19

5 Closure Properties of PEG Languages

A single non-PEG reversal witness and its PEG-prefix/regular-tail factorization refute several closure properties of PEG languages. The results also establish a left–right asymmetry for concatenation and summarize the resulting closure landscape.

5 Closure Properties of PEG Languages

  • PEG is closed under neither unrestricted concatenation nor Kleene star, homomorphisms, or substitutions; concatenation fails even for PEG·REG.The strong failure is PEG·REG ⊈ PEG, despite REG·PEG ⊆ PEG.Source: §5 · p. 19

5.1 The Prefix Language and the Factorization

  • Cutting L after a witnessing record yields L = Pref·RR0, where Pref is PEG and RR0 is regular.Appending the regular suffix preserves the witness, so the factorization recovers L.Source: §5 · p. 19, §5.1 · p. 20

5.2 Concatenation, Kleene Star, and Homomorphisms

  • PEG·REG ⊈ PEG, while REG·PEG ⊆ PEG; the same factorization also gives a Kleene-star counterexample through a regular envelope.The star argument intersects U* with a regular Shape language to recover the non-PEG language L.Source: §5.2 · pp. 21–22
  • PEG is not closed under homomorphisms or substitutions, even when every component language in the substitution belongs to PEG.Inverse homomorphisms, including possibly erasing ones, remain closed.Source: §5.2 · p. 22

5.3 Summary of Closure Properties

  • The closure summary records positive Boolean and inverse-homomorphism closure alongside failures for concatenation, Kleene star, reversal, homomorphisms, and substitutions.The table marks which closure results are established in this work.Source: §5.3 · p. 23

6 Conclusion and Open Problems

The paper uses a transfer from scaffolding automata to cell-probe data structures to establish PEG separations and closure failures. It also identifies limits of this method and open questions about intrinsic characterizations.

6 Conclusion and Open Problems

  • Fixed-radius scaffold access lets each SCA transition be simulated with O(1) cell probes, turning cell-probe lower bounds into PEG expressiveness lower bounds.The framework interprets the scaffold as persistent memory.Source: §6 · p. 23
  • Some linear context-free languages are not PEG languages, and PEG languages are not closed under reversal.The conclusion states these outcomes for the constructed language C and its reversal.Source: §6 · p. 23
  • The transfer method proves non-membership only when a language is connected to a data-structure problem with a suitable lower bound; it does not identify an intrinsic SCA obstruction.The paper leaves direct combinatorial or information-theoretic SCA lower bounds open.Source: §6 · p. 23
  • The same witness refutes closure under concatenation and Kleene star, while REG · PEG ⊆ PEG but PEG · REG ⊈ PEG.The concatenation result is asymmetric with regular factors.Source: §6 · p. 23
  • The result does not characterize LIN ∩ PEG, and finding natural necessary or sufficient conditions for total PEG recognition remains open.An intrinsic theory could yield reusable PEG non-membership criteria without a separate data-structure reduction.Source: §6 · p. 24

Formal Verification

The accompanying Lean 4 artifact checks the paper’s main results and identifies the axioms used by its declarations.

Formal Verification

  • The main results are checked in Lean 4, with separate entry points for the separation and closure properties.Checking either entry point prints the axioms on which its declarations depend.Source: Formal Verification · p. 25
  • Every positive result in the artifact is proved outright, while Corollary 5.11 is the only result using all three additional axioms.The three axioms include the project-facing corollary of Theorem 4.2, inverse-image closure for possibly erasing homomorphisms, and Greibach’s hardest-language theorem.Source: Formal Verification · p. 25
  • The artifact expresses Theorem 3.5 and Corollary 4.4 with explicit budget functions and existentially quantified constants instead of asymptotic notation.The scaffolding-automaton compiler produces this explicit form, leaving the separation unaffected.Source: Formal Verification · p. 25

Generative AI Usage

A generative AI tool was used in developing the witness analysis and generating the Lean 4 proof scripts; the authors describe their review and responsibility for the work.

Generative AI Usage

  • A large-language-model tool examined the witness language and preliminary proof outlines and generated all Lean 4 proof scripts.The scripts are part of the accompanying formal-verification artifact.Source: Generative AI Usage · p. 25
  • The authors reviewed and revised the manuscript arguments and checked that the formal statements correspond to the paper’s claims.They also confirmed that Lean 4 accepts the artifact.Source: Generative AI Usage · p. 25
  • The authors take full responsibility for every definition, claim, proof, and formalization in the paper.Source: Generative AI Usage · p. 25
Loading 2608.29592v1…