LR(k) languages are exactly DPDA languages

Over every finite terminal alphabet, the languages generated by LR(k) grammars with any fixed positive amount of lookahead are exactly the languages recognized by deterministic pushdown automata (DPDAs). Consequently, allowing an existential finite lookahead does not enlarge the class:

• is_LRk_iff_is_DPDA proves is_LRk k L ↔ is_DPDA L when 0 < k;
• is_LR_iff_is_DPDA proves is_LR L ↔ is_DPDA L;
• LRk_eq_DPDA and LR_eq_DPDA state the corresponding equalities of language classes.

The restriction 0 < k belongs only to the fixed-lookahead equivalence. Every LR(0) language is still a DPDA language, while the reverse construction produces an LR(1) grammar. The existential class LR therefore agrees with DPDA.Class without an additional hypothesis.

Combining these equalities with DCF ⊊ CF also yields the exact hierarchy statements LRk_strict_subclass_CF_of_card (for every k > 0) and LR_strict_subclass_CF_of_card, uniformly over every finite terminal type with at least three elements.

LR(k) grammar to DPDA

The theorem is_DPDA_of_is_LRk compiles a semantic LR(k) grammar into a concrete deterministic shift/reduce machine. Its finite control contains a fixed-size lookahead buffer and canonical LR item kernels; its stack stores the kernel reached after each viable prefix. Reductions pop one saved kernel per right-hand-side symbol and then push the nonterminal-goto kernel.

The machine reads an explicit fresh endmarker. The automata-level theorem CF_grammar.LRk.Buffered.marked_machine_correct proves that it accepts a properly marked word exactly when the original grammar generates the word. Intersection with the regular language of well-formed marked inputs, regular right quotient, and injective renaming then remove that implementation marker. Zero-lookahead grammars are covered by monotonicity from LR(0) to LR(1).

DPDA to LR(1) grammar

The theorem is_LRk_one_of_is_DPDA starts by normalizing a DPDA so that a computation cannot pass between two accepting configurations without reading input. Final-state acceptance is then converted to empty-stack acceptance and the productive part of its characteristic context-free grammar is retained.

The LR(1) proof follows Knuth’s active partial-tree argument. A rightmost prehandle carries an ancestry spine whose active node is paired with the corresponding pushdown computation. Determinism and one symbol of lookahead make the productive introducing transition unique; the normalization handles the otherwise exceptional end-of-input drain choice. This proves handle uniqueness for the characteristic grammar, including its empty productions and the fresh augmented start rule.

Source

The public equivalence and class equalities are in Langlib.Grammars.LR.Equivalence. The two construction directions are exposed by is_DPDA_of_is_LRk and is_LRk_one_of_is_DPDA.

Keywords

LR(k) grammar, LR(1) grammar, deterministic context-free language, DCFL, deterministic pushdown automaton, DPDA, canonical LR parser, shift-reduce parser, grammar automaton equivalence.