LR Languages Under Injective Terminal Maps

This file proves that LR(k) languages are closed under injective letter-to-letter terminal maps. The construction relabels terminals in a context-free grammar and uses injectivity to reflect rightmost derivations back to the original grammar, where the LR(k) uniqueness condition is available.

@[reducible]

def map_CF_rule {T₁ T₂ N : Type} (f : T₁ → T₂) (r : N × List (symbol T₁ N)) : N × List (symbol T₂ N)

Map a context-free rule along a terminal map, leaving nonterminals unchanged.

Equations

• map_CF_rule f r = (r.1, List.map (map_symbol_fn f) r.2)

@[reducible]

def map_CF_grammar {T₁ T₂ : Type} (g : CF_grammar T₁) (f : T₁ → T₂) : CF_grammar T₂

Map a context-free grammar along a terminal map, leaving nonterminals unchanged.

Equations

• map_CF_grammar g f = { nt := g.nt, initial := g.initial, rules := List.map (map_CF_rule f) g.rules }

theorem map_CF_grammar_language_of_leftInverse {T₁ T₂ : Type} (g : CF_grammar T₁) {f : T₁ → T₂} {g' : T₂ → T₁} (hfg : Function.LeftInverse g' f) : CF_language (map_CF_grammar g f) = (Language.map f) (CF_language g)

The relabelled context-free grammar generates exactly the image language.

theorem map_CF_grammar_isLRk_of_injective {T₁ T₂ : Type} [Nonempty T₁] (g : CF_grammar T₁) {f : T₁ → T₂} (hf : Function.Injective f) {k : ℕ} (hg : g.IsLRk k) : (map_CF_grammar g f).IsLRk k

Relabelling a grammar by an injective terminal map preserves the LR(k) condition.

theorem is_LRk_map_injective {T₁ T₂ : Type} [Nonempty T₁] {f : T₁ → T₂} (hf : Function.Injective f) {k : ℕ} {L : Language T₁} (hL : is_LRk k L) : is_LRk k ((Language.map f) L)

LR(k) languages are closed under injective terminal maps.

theorem is_LR_map_injective {T₁ T₂ : Type} [Nonempty T₁] {f : T₁ → T₂} (hf : Function.Injective f) {L : Language T₁} (hL : is_LR L) : is_LR ((Language.map f) L)

LR languages are closed under injective terminal maps.