Closure of IsContextFree under string homomorphism

The image of a context-free language under a string homomorphism h : T → List T' is context-free. Construction: replace each terminal a in each grammar rule's output with the symbol-list (h a).map .terminal. Nonterminals are unchanged.

Owns the Language.stringMap definition and proves Language.IsContextFree.stringMap. Together with the parallel Bar-Hillel proof in InterRegular.lean, this dissolves the closure axioms previously in Closure.lean.

@cite{hopcroft-motwani-ullman-2000} Theorem 7.24 part 4 (p. 284-285, homomorphism case).

def Language.stringMap {T : Type u} {T' : Type v} (h : Core.StringHom T T') (L : Language T) : Language T'

The homomorphic image of a language under a string homomorphism. Language.stringMap h L = {h(v) | v ∈ L}.

Equations

• Language.stringMap h L = {w : List T' | ∃ v ∈ L, h.apply v = w}

def ContextFreeRule.Symbol.applyHom {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') : Symbol T N → List (Symbol T' N)

Apply a string homomorphism h : T → List T' to a single Symbol, producing a symbol-list. Terminals are substituted; nonterminals are preserved as singletons.

Equations

• ContextFreeRule.Symbol.applyHom h (Symbol.terminal a) = List.map Symbol.terminal (h a)
• ContextFreeRule.Symbol.applyHom h (Symbol.nonterminal X) = [Symbol.nonterminal X]

def ContextFreeRule.applyHomList {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') : List (Symbol T N) → List (Symbol T' N)

Apply a string homomorphism h : T → List T' to a symbol list (free monoid functoriality).

Equations

• ContextFreeRule.applyHomList h = List.flatMap (ContextFreeRule.Symbol.applyHom h)

@[simp]

theorem ContextFreeRule.applyHomList_nil {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') : applyHomList h [] = []

@[simp]

theorem ContextFreeRule.applyHomList_cons {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') (s : Symbol T N) (ss : List (Symbol T N)) : applyHomList h (s :: ss) = Symbol.applyHom h s ++ applyHomList h ss

theorem ContextFreeRule.applyHomList_append {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') (xs ys : List (Symbol T N)) : applyHomList h (xs ++ ys) = applyHomList h xs ++ applyHomList h ys

@[simp]

theorem ContextFreeRule.applyHomList_singleton_terminal {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') (a : T) : applyHomList h [Symbol.terminal a] = List.map Symbol.terminal (h a)

@[simp]

theorem ContextFreeRule.applyHomList_singleton_nonterminal {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') (X : N) : applyHomList h [Symbol.nonterminal X] = [Symbol.nonterminal X]

theorem ContextFreeRule.applyHomList_map_terminal {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') (w : List T) : applyHomList h (List.map Symbol.terminal w) = List.map Symbol.terminal (List.flatMap h w)

For a list of terminals, applyHomList becomes flatMap h followed by re-wrapping as terminals.

def ContextFreeRule.applyHom {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') (r : ContextFreeRule T N) : ContextFreeRule T' N

Apply a string homomorphism to a CFG rule.

Equations

• ContextFreeRule.applyHom h r = { input := r.input, output := ContextFreeRule.applyHomList h r.output }

@[simp]

theorem ContextFreeRule.applyHom_input {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') (r : ContextFreeRule T N) : (applyHom h r).input = r.input

@[simp]

theorem ContextFreeRule.applyHom_output {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') (r : ContextFreeRule T N) : (applyHom h r).output = applyHomList h r.output

theorem ContextFreeRule.Rewrites.applyHom {T : Type u} {T' : Type v} {N : Type u_1} (h : T → List T') {r : ContextFreeRule T N} {u v : List (Symbol T N)} (hr : r.Rewrites u v) : (ContextFreeRule.applyHom h r).Rewrites (applyHomList h u) (applyHomList h v)

A single rule's Rewrites relation lifts under applyHom.

noncomputable def ContextFreeGrammar.applyHom {T : Type u} {T' : Type v} (h : T → List T') (G : ContextFreeGrammar T) : ContextFreeGrammar T'

Apply a string homomorphism to a CFG: substitute terminals in every rule. Noncomputable due to Finset.image requiring decidable equality on rules (provided classically).

Equations

• ContextFreeGrammar.applyHom h G = { NT := G.NT, initial := G.initial, rules := Finset.image (ContextFreeRule.applyHom h) G.rules }

@[simp]

theorem ContextFreeGrammar.applyHom_NT {T : Type u} {T' : Type v} (h : T → List T') (G : ContextFreeGrammar T) : (applyHom h G).NT = G.NT

@[simp]

theorem ContextFreeGrammar.applyHom_initial {T : Type u} {T' : Type v} (h : T → List T') (G : ContextFreeGrammar T) : (applyHom h G).initial = G.initial

theorem ContextFreeGrammar.applyHom_rules {T : Type u} {T' : Type v} (h : T → List T') (G : ContextFreeGrammar T) : (applyHom h G).rules = Finset.image (ContextFreeRule.applyHom h) G.rules

theorem ContextFreeGrammar.Produces.applyHom {T : Type u} {T' : Type v} (h : T → List T') {G : ContextFreeGrammar T} {u v : List (Symbol T G.NT)} (huv : G.Produces u v) : (ContextFreeGrammar.applyHom h G).Produces (ContextFreeRule.applyHomList h u) (ContextFreeRule.applyHomList h v)

Produces lifts under applyHom.

theorem ContextFreeGrammar.Derives.applyHom {T : Type u} {T' : Type v} (h : T → List T') {G : ContextFreeGrammar T} {u v : List (Symbol T G.NT)} (huv : G.Derives u v) : (ContextFreeGrammar.applyHom h G).Derives (ContextFreeRule.applyHomList h u) (ContextFreeRule.applyHomList h v)

Derives lifts under applyHom.

theorem ContextFreeGrammar.applyHom_language_subset {T : Type u} {T' : Type v} (h : T → List T') (G : ContextFreeGrammar T) : Language.stringMap h G.language ≤ (applyHom h G).language

Forward inclusion: every (G.applyHom h)-generated string is in Language.stringMap h G.language.

theorem ContextFreeGrammar.applyHom_language_subset_inv {T : Type u} {T' : Type v} (h : T → List T') (G : ContextFreeGrammar T) : (applyHom h G).language ≤ Language.stringMap h G.language

Backward inclusion: every (G.applyHom h)-generated string is the image of some G-generated preimage under h. The construction lifts G'-derivations to G-derivations step-by-step using decompose_applyHomList and liftMapTerminal. Standard textbook construction (@cite{hopcroft-motwani-ullman-2000} Theorem 7.24 part 4 (p. 284-285, homomorphism case)).

theorem ContextFreeGrammar.applyHom_language {T : Type u} {T' : Type v} (h : T → List T') (G : ContextFreeGrammar T) : (applyHom h G).language = Language.stringMap h G.language

theorem Language.IsContextFree.stringMap {T : Type u} {T' : Type v} (h : Core.StringHom T T') {L : Language T} (hL : L.IsContextFree) : (Language.stringMap h L).IsContextFree