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.

The definition uses the standard fresh-start augmentation. This matters even for language recognition: the completed augmented start rule is the parser's accept action, so including it in handle uniqueness rules out accept/reduce and accept/shift conflicts as well as ordinary reduce/reduce and shift/reduce conflicts.

This is the grammar-side class matching DPDAs. The equivalence is proved by the two standard constructions in Langlib.Grammars.LR.Equivalence:

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

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.augmentSymbol {T N : Type} : symbol T N → symbol T (Option N)

Embed an original grammar symbol into a grammar with a fresh start nonterminal. none is reserved for the fresh start and original nonterminals are embedded with some.

Equations

• CF_grammar.augmentSymbol (symbol.terminal t) = symbol.terminal t
• CF_grammar.augmentSymbol (symbol.nonterminal A) = symbol.nonterminal (some A)

@[simp]

theorem CF_grammar.augmentSymbol_terminal {T N : Type} (t : T) : augmentSymbol (symbol.terminal t) = symbol.terminal t

@[simp]

theorem CF_grammar.augmentSymbol_nonterminal {T N : Type} (A : N) : augmentSymbol (symbol.nonterminal A) = symbol.nonterminal (some A)

def CF_grammar.augmentString {T N : Type} (w : List (symbol T N)) : List (symbol T (Option N))

Embed a sentential form into the fresh-start augmentation.

Equations

• CF_grammar.augmentString w = List.map CF_grammar.augmentSymbol w

@[simp]

theorem CF_grammar.augmentString_nil {T N : Type} : augmentString [] = []

@[simp]

theorem CF_grammar.augmentString_cons {T N : Type} (a : symbol T N) (w : List (symbol T N)) : augmentString (a :: w) = augmentSymbol a :: augmentString w

def CF_grammar.augmentRule {T N : Type} (r : N × List (symbol T N)) : Option N × List (symbol T (Option N))

Embed a production into the fresh-start augmentation.

Equations

• CF_grammar.augmentRule r = (some r.1, CF_grammar.augmentString r.2)

def CF_grammar.augmentStartRule {T : Type} (g : CF_grammar T) : Option g.nt × List (symbol T (Option g.nt))

The distinguished production of the augmented grammar.

Equations

• g.augmentStartRule = (none, [symbol.nonterminal (some g.initial)])

def CF_grammar.augment {T : Type} (g : CF_grammar T) : CF_grammar T

Fresh-start augmentation of a context-free grammar.

The new initial nonterminal is none; every original nonterminal is renamed to some A; and the sole production headed by the fresh start is none → some S.

Equations

• g.augment = { nt := Option g.nt, initial := none, rules := g.augmentStartRule :: List.map CF_grammar.augmentRule g.rules }

@[simp]

theorem CF_grammar.augment_initial {T : Type} (g : CF_grammar T) : g.augment.initial = none

@[simp]

theorem CF_grammar.augment_start_ne_original {T : Type} (g : CF_grammar T) (A : g.nt) : g.augment.initial ≠ some A

@[simp]

theorem CF_grammar.augmentString_terminal {T : Type} (g : CF_grammar T) (t : T) : augmentString [symbol.terminal t] = [symbol.terminal t]

@[simp]

theorem CF_grammar.augmentString_nonterminal {T : Type} (g : CF_grammar T) (A : g.nt) : augmentString [symbol.nonterminal A] = [symbol.nonterminal (some A)]

@[simp]

theorem CF_grammar.augmentString_append {T : Type} (g : CF_grammar T) (u v : List (symbol T g.nt)) : augmentString (u ++ v) = augmentString u ++ augmentString v

@[simp]

theorem CF_grammar.augmentString_map_terminal {T : Type} (g : CF_grammar T) (w : List T) : augmentString (List.map symbol.terminal w) = List.map symbol.terminal w

@[simp]

theorem CF_grammar.augmentStartRule_mem {T : Type} (g : CF_grammar T) : g.augmentStartRule ∈ g.augment.rules

theorem CF_grammar.augmentRule_mem {T : Type} (g : CF_grammar T) {r : g.nt × List (symbol T g.nt)} (hr : r ∈ g.rules) : augmentRule r ∈ g.augment.rules

def CF_grammar.projectAugmentSymbol {T : Type} (g : CF_grammar T) : symbol T (Option g.nt) → symbol T g.nt

Forget the fresh start symbol. The fresh start itself is sent to the original initial nonterminal, so the augmented start production projects to a reflexive step.

Equations

• g.projectAugmentSymbol (symbol.terminal t) = symbol.terminal t
• g.projectAugmentSymbol (symbol.nonterminal none) = symbol.nonterminal g.initial
• g.projectAugmentSymbol (symbol.nonterminal (some A)) = symbol.nonterminal A

@[simp]

theorem CF_grammar.projectAugmentSymbol_augmentSymbol {T : Type} (g : CF_grammar T) (a : symbol T g.nt) : g.projectAugmentSymbol (augmentSymbol a) = a

def CF_grammar.projectAugmentString {T : Type} (g : CF_grammar T) (w : List (symbol T (Option g.nt))) : List (symbol T g.nt)

Forget the fresh start symbol in a sentential form.

Equations

• g.projectAugmentString w = List.map g.projectAugmentSymbol w

@[simp]

theorem CF_grammar.projectAugmentString_append {T : Type} (g : CF_grammar T) (u v : List (symbol T (Option g.nt))) : g.projectAugmentString (u ++ v) = g.projectAugmentString u ++ g.projectAugmentString v

@[simp]

theorem CF_grammar.projectAugmentString_augmentString {T : Type} (g : CF_grammar T) (w : List (symbol T g.nt)) : g.projectAugmentString (augmentString w) = w

@[simp]

theorem CF_grammar.projectAugmentString_map_terminal {T : Type} (g : CF_grammar T) (w : List T) : g.projectAugmentString (List.map symbol.terminal w) = List.map symbol.terminal w

theorem CF_grammar.RewritesRightmost.augment {T : Type} (g : CF_grammar T) {r : g.nt × List (symbol T g.nt)} {u v : List (symbol T g.nt)} (h : RewritesRightmost r u v) : RewritesRightmost (augmentRule r) (augmentString u) (augmentString v)

An original rightmost rewrite embeds as a rightmost rewrite of the augmented grammar.

theorem CF_grammar.ProducesRightmost.augment {T : Type} (g : CF_grammar T) {u v : List (symbol T g.nt)} (h : g.ProducesRightmost u v) : g.augment.ProducesRightmost (augmentString u) (augmentString v)

An original rightmost production step embeds into the augmented grammar.

theorem CF_grammar.DerivesRightmost.augment {T : Type} (g : CF_grammar T) {u v : List (symbol T g.nt)} (h : g.DerivesRightmost u v) : g.augment.DerivesRightmost (augmentString u) (augmentString v)

An original rightmost derivation embeds into the augmented grammar, starting at the embedded original start symbol.

theorem CF_grammar.augment_start_producesRightmost {T : Type} (g : CF_grammar T) : g.augment.ProducesRightmost [symbol.nonterminal g.augment.initial] [symbol.nonterminal (some g.initial)]

The distinguished start production is a rightmost step.

theorem CF_grammar.augment_derivesRightmost {T : Type} (g : CF_grammar T) {v : List (symbol T g.nt)} (h : g.DerivesRightmost [symbol.nonterminal g.initial] v) : g.augment.DerivesRightmost [symbol.nonterminal g.augment.initial] (augmentString v)

Lift an original rightmost derivation from its start symbol to a derivation from the fresh augmented start symbol.

theorem CF_grammar.transforms_augment {T : Type} (g : CF_grammar T) {u v : List (symbol T g.nt)} (h : CF_transforms g u v) : CF_transforms g.augment (augmentString u) (augmentString v)

An ordinary context-free rewrite embeds into the augmented grammar.

theorem CF_grammar.derives_augment {T : Type} (g : CF_grammar T) {u v : List (symbol T g.nt)} (h : CF_derives g u v) : CF_derives g.augment (augmentString u) (augmentString v)

An ordinary derivation embeds into the augmented grammar.

theorem CF_grammar.augment_start_transforms {T : Type} (g : CF_grammar T) : CF_transforms g.augment [symbol.nonterminal g.augment.initial] [symbol.nonterminal (some g.initial)]

The distinguished start production is an ordinary context-free step.

theorem CF_grammar.augment_derives {T : Type} (g : CF_grammar T) {v : List (symbol T g.nt)} (h : CF_derives g [symbol.nonterminal g.initial] v) : CF_derives g.augment [symbol.nonterminal g.augment.initial] (augmentString v)

Lift an original derivation from its start symbol to a derivation from the fresh augmented start symbol.

theorem CF_grammar.derives_project_augment_of_transforms {T : Type} (g : CF_grammar T) {u v : List (symbol T (Option g.nt))} (h : CF_transforms g.augment u v) : CF_derives g (g.projectAugmentString u) (g.projectAugmentString v)

Projecting one augmented context-free step gives zero or one original steps. The zero-step case is exactly the fresh start production.

theorem CF_grammar.derives_project_augment {T : Type} (g : CF_grammar T) {u v : List (symbol T (Option g.nt))} (h : CF_derives g.augment u v) : CF_derives g (g.projectAugmentString u) (g.projectAugmentString v)

Project an augmented derivation back to the original grammar.

theorem CF_grammar.derivesRightmost_project_augment_of_produces {T : Type} (g : CF_grammar T) {u v : List (symbol T (Option g.nt))} (h : g.augment.ProducesRightmost u v) : g.DerivesRightmost (g.projectAugmentString u) (g.projectAugmentString v)

Projecting one augmented rightmost step gives zero or one original rightmost steps. Again, the zero-step case is the fresh start production.

theorem CF_grammar.derivesRightmost_project_augment {T : Type} (g : CF_grammar T) {u v : List (symbol T (Option g.nt))} (h : g.augment.DerivesRightmost u v) : g.DerivesRightmost (g.projectAugmentString u) (g.projectAugmentString v)

Project an augmented rightmost derivation back to the original grammar.

theorem CF_grammar.augment_language {T : Type} (g : CF_grammar T) : CF_language g.augment = CF_language g

Fresh-start augmentation preserves the generated language.

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

Knuth's semantic handle-uniqueness condition, before fresh-start augmentation.

Suppose the first derivation has just used r₁ after the prefix p₁, so its handle ends after p₁ ++ r₁.2. The equality in the premise says that the entire second right-sentential form can also be split at that first handle boundary, with a terminal suffix y. If the actual suffix s₁ of the first handle and y have the same k visible terminals, an LR(k) grammar must choose the same handle position and production.

Allowing the second handle to end later than the first is essential: that is the case which detects a possible shift instead of the first reduction. Requiring only p₁ ++ r₁.2 = p₂ ++ r₂.2 would detect reduce/reduce conflicts but miss shift/reduce conflicts.

Equations

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

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

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

Handle uniqueness is checked after adjoining a genuinely fresh start symbol and the production S′ → S. Thus the condition includes conflicts with the accept action, not only conflicts between original productions.

Equations

• g.IsLRk k = g.augment.CoreIsLRk k

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

Core LR lookahead is monotone: a grammar satisfying the handle condition with k symbols also satisfies it with any larger lookahead.

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 LRk {T : Type} (k : ℕ) : Set (Language T)

The class of languages generated by LR(k) grammars for a fixed amount of lookahead.

Equations

• LRk k = setOf (is_LRk k)

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.