Regular Closure Under Inverse Homomorphism

Proof idea: keep the DFA for the target language, but replace each input step on a by the DFA transition over the whole word h a. After reading w, the new automaton is in exactly the state the old automaton would reach on w.flatMap h.

Regular Closure Under Inverse String Homomorphism

This file proves that regular languages are closed under inverse string homomorphism. Given a DFA M recognising L and a string homomorphism h : β → List α, we construct a DFA for h⁻¹(L) = {w ∈ β* | h*(w) ∈ L} by composing h into the transition function.

Main results

• inverseHomDFA — the DFA for the preimage under a string homomorphism.
• inverseHomDFA_correct — correctness of the construction.
• Language.IsRegular.inverseStringHomomorphism — if L is regular then {w | w.flatMap h ∈ L} is regular.

noncomputable def inverseHomDFA {α : Type u_1} {β : Type u_2} {σ : Type u_3} (M : DFA α σ) (h : β → List α) : DFA β σ

DFA for the inverse homomorphism h⁻¹(L).

Given a DFA M over α and a string homomorphism h : β → List α, the new DFA has the same state set but transitions via M.evalFrom q (h b) — it processes the entire image h(b) in one step.

Equations

• inverseHomDFA M h = { step := fun (q : σ) (b : β) => M.evalFrom q (h b), start := M.start, accept := M.accept }

theorem inverseHomDFA_eval {α : Type u_1} {β : Type u_2} {σ : Type u_3} (M : DFA α σ) (h : β → List α) (w : List β) : (inverseHomDFA M h).eval w = M.eval (List.flatMap h w)

@[simp]

theorem inverseHomDFA_accept {α : Type u_1} {β : Type u_2} {σ : Type u_3} (M : DFA α σ) (h : β → List α) : (inverseHomDFA M h).accept = M.accept

theorem inverseHomDFA_correct {α : Type u_1} {β : Type u_2} {σ : Type u_3} (M : DFA α σ) (h : β → List α) : (inverseHomDFA M h).accepts = {w : List β | List.flatMap h w ∈ M.accepts}

theorem Language.IsRegular.inverseStringHomomorphism {α : Type u_1} {β : Type u_2} {L : Language α} (hL : L.IsRegular) (h : β → List α) : IsRegular {w : List β | List.flatMap h w ∈ L}

Regular languages are closed under inverse string homomorphism.

theorem RG_closedUnderInverseHomomorphism : ClosedUnderInverseHomomorphism fun {α : Type} [Fintype α] => is_RG

The class of regular languages is closed under inverse string homomorphism.