Regular Closure Under Kleene Star

Proof idea: build an epsilon-NFA with a fresh accepting start state and a copy of the automaton for L. Epsilon transitions start a new L block and return from accepting states to the start, so accepting runs correspond exactly to finite concatenations of words from L.

Regular Closure Under Kleene Star

This file proves that the class of regular languages is closed under Kleene star by constructing an ε-NFA from a DFA.

Main results

• Language.IsRegular.kstar' — if L is regular, then L∗ is regular.

noncomputable def Language.starεNFA {α : Type u_1} {σ : Type u_2} (M : DFA α σ) : εNFA α (σ ⊕ Unit)

ε-NFA for the Kleene star of a DFA.

States are σ ⊕ Unit. The fresh state Sum.inr () is both the start and the sole accepting state. It has an ε-transition into the DFA's start state. Accepting states of the DFA have an ε-transition back to the fresh state.

Equations

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

theorem Language.starεNFA_correct {α : Type u_1} {σ : Type u_2} (M : DFA α σ) : (starεNFA M).accepts = KStar.kstar M.accepts

The Kleene star ε-NFA accepts exactly the Kleene star of the DFA language.

theorem Language.IsRegular.kstar' {α : Type u_1} {L : Language α} (hL : L.IsRegular) : (KStar.kstar L).IsRegular

Regular languages are closed under Kleene star.

theorem RG_closedUnderKleeneStar {α : Type} [Fintype α] : ClosedUnderKleeneStar is_RG

The class of regular languages is closed under Kleene star.