LR(k) Grammars

This file defines the grammar-side deterministic context-free notion used in parser theory, as a restriction of the repository's own context-free grammars (CF_grammar). The key definition is CF_grammar.IsLRk: after a rightmost derivation step, the reducible handle is uniquely determined by the already-built sentential prefix and by k terminal lookahead symbols.

This is the grammar-side class intended to match DPDAs. The full equivalence with is_DCF requires the two standard constructions:

• an LR(k) parser as a DPDA, proving is_LR → is_DCF;
• a deterministic grammar construction from a DPDA, proving is_DCF → is_LR.

Those constructions are not encoded here yet.

A context-free rule is, in this development, a pair r : g.nt × List (symbol T g.nt) whose first component r.1 is the left-hand nonterminal and whose second component r.2 is the right-hand output string.

def CF_grammar.RewritesRightmost {T N : Type} (r : N × List (symbol T N)) (u v : List (symbol T N)) : Prop

A rightmost use of a context-free rule r = (input, output).

The rule rewrites an occurrence of r.1 whose suffix contains terminals only.

Equations

• One or more equations did not get rendered due to their size.

def CF_grammar.ProducesRightmost {T : Type} (g : CF_grammar T) (u v : List (symbol T g.nt)) : Prop

A single rightmost derivation step in a context-free grammar.

Equations

• g.ProducesRightmost u v = ∃ r ∈ g.rules, CF_grammar.RewritesRightmost r u v

@[reducible, inline]

abbrev CF_grammar.DerivesRightmost {T : Type} (g : CF_grammar T) : List (symbol T g.nt) → List (symbol T g.nt) → Prop

Rightmost derivation: reflexive-transitive closure of rightmost production.

Equations

• g.DerivesRightmost = Relation.ReflTransGen g.ProducesRightmost

def CF_grammar.lrLookahead {T : Type} (k : ℕ) (w : List T) : List T

The k terminal symbols visible as LR lookahead.

Equations

• CF_grammar.lrLookahead k w = List.take k w

def CF_grammar.IsLRk {T : Type} (g : CF_grammar T) (k : ℕ) : Prop

Semantic LR(k) condition for a context-free grammar.

If two rightmost derivations reach configurations where one more rightmost step creates the same sentential prefix, and their remaining terminal suffixes have the same k-symbol lookahead, then the reducible handle and rule are identical. The terminal suffixes themselves need not be equal beyond the visible lookahead.

Equations

• One or more equations did not get rendered due to their size.

theorem CF_grammar.IsLRk.mono {T : Type} (g : CF_grammar T) {k l : ℕ} (hkl : k ≤ l) (hg : g.IsLRk k) : g.IsLRk l

LR lookahead is monotone: a grammar that is LR(k) is also LR(l) for any l ≥ k.

def is_LRk {T : Type} (k : ℕ) (L : Language T) : Prop

Language class generated by an LR(k) grammar.

Equations

• is_LRk k L = ∃ (g : CF_grammar T), g.IsLRk k ∧ CF_language g = L

def is_LR {T : Type} (L : Language T) : Prop

Language class generated by an LR(k) grammar for some finite k.

Equations

• is_LR L = ∃ (k : ℕ), is_LRk k L

def LR {T : Type} : Set (Language T)

The class of LR languages.

Equations

• LR = setOf is_LR

theorem is_LR_of_is_LRk {T : Type} {k : ℕ} {L : Language T} (h : is_LRk k L) : is_LR L

Every LR(k) language is an LR language.

theorem is_LRk_mono {T : Type} {k l : ℕ} (hkl : k ≤ l) {L : Language T} (h : is_LRk k L) : is_LRk l L

LR language classes are monotone in the amount of lookahead.