Context-Free Closure Under String Homomorphism

This file proves that context-free languages are closed under string homomorphism and epsilon-free string homomorphism.

Main declarations

• CF_closed_under_homomorphism : CFLs are closed under string homomorphism.
• CF_closed_under_epsfree_homomorphism : CFLs are closed under ε-free string homomorphism.

theorem is_CF_singleton {β : Type} (w : List β) : is_CF {w}

Singleton word languages are context-free.

theorem CF_closed_under_homomorphism {α β : Type} (L : Language α) (h : α → List β) (hL : is_CF L) : is_CF (L.homomorphicImage h)

The class of context-free languages is closed under string homomorphism.

Given a context-free language L over alphabet α and a string homomorphism h : α → List β, the image {h(w) | w ∈ L} is also context-free.

Proof sketch: A string homomorphism is a special case of substitution where each symbol a is replaced by the singleton language {h(a)}. Since every singleton language is context-free and CFLs are closed under substitution (CF_of_subst_CF), the result follows.

theorem CF_closed_under_epsfree_homomorphism {α β : Type} (L : Language α) (h : α → List β) (hL : is_CF L) (_heps : IsEpsFreeHomomorphism h) : is_CF (L.homomorphicImage h)

The class of context-free languages is closed under ε-free string homomorphism.

This is a direct corollary of CF_closed_under_homomorphism, since every ε-free string homomorphism is in particular a string homomorphism.

theorem CF_closedUnderHomomorphism : ClosedUnderHomomorphism fun {α : Type} [Fintype α] => is_CF

The class of context-free languages is closed under string homomorphism.

theorem CF_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => is_CF

The class of context-free languages is closed under ε-free string homomorphism.