Regular Closure Under Homomorphism

Proof idea: a homomorphism is implemented as regular substitution by replacing each input letter with the regular singleton language containing its image string. The epsilon-free variant is the same construction with the extra nonempty-image hypothesis carried through the closure predicate.

Regular Closure Under (String) Homomorphism

This file proves that regular languages are closed under symbol maps (letter-to-letter homomorphisms) and, more generally, under string homomorphisms.

Main results

• Language.IsRegular.map — if L is regular then Language.map f L is regular.
• Language.IsRegular.homomorphicImage — if L is regular (over a finite alphabet) then its image under a string homomorphism is regular.

noncomputable def Language.mapNFA {α : Type u_1} {β : Type u_2} {σ : Type u_3} (M : DFA α σ) (f : α → β) : NFA β σ

NFA recognising the image of a DFA language under a symbol map.

For a DFA M over α and a function f : α → β, the NFA over β has the same states. On symbol b, from state q, the NFA non-deterministically guesses a preimage a with f a = b and transitions to M.step q a.

Equations

• Language.mapNFA M f = { step := fun (q : σ) (b : β) => {q' : σ | ∃ (a : α), f a = b ∧ M.step q a = q'}, start := {M.start}, accept := M.accept }

theorem Language.mapNFA_correct {α : Type u_1} {β : Type u_2} {σ : Type u_3} (M : DFA α σ) (f : α → β) : (mapNFA M f).accepts = (map f) M.accepts

theorem Language.IsRegular.map {α : Type u_1} {β : Type u_2} {L : Language α} (hL : L.IsRegular) (f : α → β) : ((Language.map f) L).IsRegular

Regular languages are closed under symbol maps (letter-to-letter homomorphisms).

Singleton word languages are regular

theorem Language.isRegular_epsilon {γ : Type} : {[]}.IsRegular

theorem Language.isRegular_singleton_letter {γ : Type} (a : γ) : {[a]}.IsRegular

theorem Language.isRegular_singleton_word {γ : Type} (w : List γ) : {w}.IsRegular

Any singleton word language is regular.

theorem Language.IsRegular.homomorphicImage {γ α' : Type} [Fintype α'] {L : Language α'} (hL : L.IsRegular) (h : α' → List γ) : (L.homomorphicImage h).IsRegular

Regular languages are closed under string homomorphism.

Given a regular language L over a finite alphabet and a string homomorphism h : α' → List γ, the image {h(w) | w ∈ L} is regular.

theorem Language.RG_closedUnderHomomorphism : ClosedUnderHomomorphism fun {α : Type} [Fintype α] => is_RG

The class of regular languages is closed under homomorphism.

theorem Language.RG_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => is_RG

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