Closure of IsContextFree under string homomorphism

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

Main definitions

• Language.stringMap f : Language T →+* Language T' — image under the string homomorphism. Since List α = FreeMonoid α, the action List.flatMap f is the free-monoid lift FreeMonoid.lift f; bundled as a semiring hom mirroring mathlib's Language.map, of which the letter-to-letter case is the special case Language.stringMap_letterMap.

Main theorems

• Language.IsContextFree.stringMap — context-free languages are closed under string homomorphism.
• ContextFreeGrammar.applyHom_language — the grammar construction realizes stringMap.

[HMU00] (homomorphism-closure construction).

def Language.stringMap {T : Type u} {T' : Type v} (f : T → List T') : Language T →+* Language T'

The image of a language under the string homomorphism induced by a per-symbol map f : T → List T'. On a word the action is List.flatMap f — i.e. the free-monoid lift FreeMonoid.lift f, since List α = FreeMonoid α. Bundled as a semiring hom mirroring mathlib's Language.map; the letter-to-letter map is the special case Language.stringMap_letterMap.

Equations

• Language.stringMap f = { toFun := Set.image (List.flatMap f), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Language.mem_stringMap {T : Type u} {T' : Type v} {f : T → List T'} {L : Language T} {w : List T'} : w ∈ (stringMap f) L ↔ ∃ v ∈ L, List.flatMap f v = w

@[simp]

theorem Language.stringMap_letterMap {T : Type u} {T' : Type v} (f : T → T') (L : Language T) : (stringMap fun (a : T) => [f a]) L = (map f) L

Bridge to mathlib's Language.map. The letter-to-letter map f : T → T' (singleton outputs) is the special case of stringMap that collapses to mathlib's Language.map f, so stringMap genuinely generalizes the existing letter image.

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 ([HMU00] 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} (f : T → List T') {L : Language T} (hL : L.IsContextFree) : ((Language.stringMap f) L).IsContextFree