Context-free languages are closed under string homomorphisms

A map f : T → List T' on letters extends to a monoid homomorphism on words, List.flatMap f, and to a semiring homomorphism Language.stringMap f on languages. The image of a context-free language under it is context-free: replace every terminal a in every rule by the string f a ([HMU00]).

Main definitions

• Language.stringMap: the image of a language under a string homomorphism.
• Symbol.applyHom, ContextFreeRule.applyHom, ContextFreeGrammar.applyHom: a string homomorphism applied to a symbol, a rule and a grammar.

Main results

• ContextFreeGrammar.applyHom_language: the image grammar generates the image language.
• Language.IsContextFree.stringMap: closure under string homomorphisms, with its contrapositive Language.not_isContextFree_of_stringMap_not.

References

• [HMU00]

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

The image of a language under the string homomorphism induced by f : T → List T', the monoid homomorphism List.flatMap f on words; Language.map is the case of one-letter images.

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_1} {T' : Type u_2} {f : T → List T'} {L : Language T} {w : List T'} : w ∈ (stringMap f) L ↔ ∃ v ∈ L, List.flatMap f v = w

theorem Language.stringMap_singleton {T : Type u_1} {T' : Type u_2} (f : T → T') (L : Language T) : (stringMap fun (a : T) => [f a]) L = (map f) L

def Symbol.applyHom {T : Type u_1} {T' : Type u_2} {N : Type u_3} (h : T → List T') : Symbol T N → List (Symbol T' N)

A string homomorphism on terminals applied to a symbol: a terminal becomes the string of terminals it maps to, a nonterminal stays.

Equations

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

@[simp]

theorem Symbol.applyHom_terminal {T : Type u_1} {T' : Type u_2} {N : Type u_3} (h : T → List T') (a : T) : applyHom h (terminal a) = List.map terminal (h a)

@[simp]

theorem Symbol.applyHom_nonterminal {T : Type u_1} {T' : Type u_2} {N : Type u_3} (h : T → List T') (A : N) : applyHom h (nonterminal A) = [nonterminal A]

theorem Symbol.flatMap_applyHom_map_terminal {T : Type u_1} {T' : Type u_2} {N : Type u_3} (h : T → List T') (w : List T) : List.flatMap (applyHom h) (List.map terminal w) = List.map terminal (List.flatMap h w)

theorem Symbol.eq_map_terminal_of_flatMap_applyHom {T : Type u_1} {T' : Type u_2} {N : Type u_3} {h : T → List T'} {l : List (Symbol T N)} {w' : List T'} : List.flatMap (applyHom h) l = List.map terminal w' → ∃ (w : List T), l = List.map terminal w ∧ List.flatMap h w = w'

A word of the image grammar comes from a word of the source.

theorem Symbol.exists_eq_of_flatMap_applyHom {T : Type u_1} {T' : Type u_2} {N : Type u_3} {h : T → List T'} {l : List (Symbol T N)} {p q : List (Symbol T' N)} {X : N} : List.flatMap (applyHom h) l = p ++ [nonterminal X] ++ q → ∃ (l₁ : List (Symbol T N)) (l₂ : List (Symbol T N)), l = l₁ ++ [nonterminal X] ++ l₂ ∧ List.flatMap (applyHom h) l₁ = p ∧ List.flatMap (applyHom h) l₂ = q

A nonterminal in the image of a sentential form comes from the same nonterminal in the source.

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

A string homomorphism applied to a rule.

Equations

• ContextFreeRule.applyHom h r = { input := r.input, output := List.flatMap (Symbol.applyHom h) r.output }

@[simp]

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

@[simp]

theorem ContextFreeRule.applyHom_output {T : Type u_1} {T' : Type u_2} {N : Type u_3} (h : T → List T') (r : ContextFreeRule T N) : (applyHom h r).output = List.flatMap (Symbol.applyHom h) r.output

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

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

A string homomorphism applied to a grammar: every terminal in every rule is replaced by its image.

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_1} {T' : Type u_2} (h : T → List T') {G : ContextFreeGrammar T} : (applyHom h G).NT = G.NT

@[simp]

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

theorem ContextFreeGrammar.mem_applyHom_rules {T : Type u_1} {T' : Type u_2} (h : T → List T') {G : ContextFreeGrammar T} {r' : ContextFreeRule T' G.NT} : r' ∈ (applyHom h G).rules ↔ ∃ r ∈ G.rules, ContextFreeRule.applyHom h r = r'

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

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

theorem ContextFreeGrammar.Produces.of_applyHom {T : Type u_1} {T' : Type u_2} (h : T → List T') {G : ContextFreeGrammar T} {l : List (Symbol T G.NT)} {t' : List (Symbol T' G.NT)} (hp : (ContextFreeGrammar.applyHom h G).Produces (List.flatMap (Symbol.applyHom h) l) t') : ∃ (t : List (Symbol T G.NT)), G.Produces l t ∧ List.flatMap (Symbol.applyHom h) t = t'

A step of the image grammar from the image of a sentential form is the image of a step of the source grammar.

theorem ContextFreeGrammar.Derives.of_applyHom {T : Type u_1} {T' : Type u_2} (h : T → List T') {G : ContextFreeGrammar T} {l : List (Symbol T G.NT)} {t' : List (Symbol T' G.NT)} (hd : (ContextFreeGrammar.applyHom h G).Derives (List.flatMap (Symbol.applyHom h) l) t') : ∃ (t : List (Symbol T G.NT)), G.Derives l t ∧ List.flatMap (Symbol.applyHom h) t = t'

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

The image grammar generates the image language.

theorem Language.IsContextFree.stringMap {T : Type u_1} {T' : Type u_2} (f : T → List T') {L : Language T} (hL : L.IsContextFree) : ((Language.stringMap f) L).IsContextFree

Context-free languages are closed under string homomorphisms.

theorem Language.not_isContextFree_of_stringMap_not {T : Type u_1} {T' : Type u_2} (f : T → List T') {L : Language T} (h : ¬((stringMap f) L).IsContextFree) : ¬L.IsContextFree

If the homomorphic image of L is not context-free, then L is not context-free.