Regular Closure Under Substitution

Proof idea: replace each transition labeled by a symbol a with an epsilon-NFA for the regular language assigned to a, wiring copies of those NFAs between the source and target states of the original automaton. Runs therefore choose one substituted word for each input symbol.

Regular Closure Under Substitution

This file proves that the class of regular languages is closed under substitution by constructing an ε-NFA from a DFA and a family of DFAs.

Main results

• Language.IsRegular.subst' — if L is regular over a finite alphabet and each f a is regular, then L.subst f is regular.

noncomputable def Language.substεNFA {α β σ : Type} (M : DFA α σ) (τ : α → Type) (N : (a : α) → DFA β (τ a)) : εNFA β (σ ⊕ σ × (a : α) × τ a)

ε-NFA for the substitution of a DFA language by a family of DFA languages.

Equations

• One or more equations did not get rendered due to their size.

General εClosure / evalFrom helpers

evalFrom for Sum.inr states

Backward direction

Forward direction

theorem Language.substεNFA_correct {α β σ : Type} {M : DFA α σ} {τ : α → Type} {N : (a : α) → DFA β (τ a)} : (substεNFA M τ N).accepts = M.accepts.subst fun (a : α) => (N a).accepts

The substitution ε-NFA accepts exactly the substitution of the DFA language.

theorem Language.IsRegular.subst' {α β : Type} [Fintype α] {L : Language α} {f : α → Language β} (hL : L.IsRegular) (hf : ∀ (a : α), (f a).IsRegular) : (L.subst f).IsRegular

Regular languages are closed under substitution (requires finite source alphabet).

theorem RG_closedUnderSubstitution : ClosedUnderSubstitution fun {α : Type} [Fintype α] => is_RG