Regular Closure Under Concatenation

Proof idea: build an epsilon-NFA with a copy of the automaton for L₁ and a copy of the automaton for L₂. It starts in the L₁ copy, follows L₁ on a prefix, and may take an epsilon transition from an accepting L₁ state into the L₂ start state; acceptance then records a split w = u ++ v.

Regular Closure Under Concatenation

This file proves that the class of regular languages is closed under concatenation by constructing an ε-NFA from two DFAs.

Main results

• Language.IsRegular.mul' — if L₁ and L₂ are regular, then L₁ * L₂ is regular.

noncomputable def Language.concatεNFA {α : Type u_1} {σ₁ : Type u_2} {σ₂ : Type u_3} (M₁ : DFA α σ₁) (M₂ : DFA α σ₂) : εNFA α (σ₁ ⊕ σ₂)

ε-NFA for the concatenation of two DFAs.

States are σ₁ ⊕ σ₂. On the left side we simulate M₁; on the right, M₂. Accepting states of M₁ get an ε-transition to M₂'s start state.

Equations

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

theorem Language.concatεNFA_correct {α : Type u_1} {σ₁ : Type u_2} {σ₂ : Type u_3} [Fintype σ₁] [Fintype σ₂] (M₁ : DFA α σ₁) (M₂ : DFA α σ₂) : (concatεNFA M₁ M₂).accepts = M₁.accepts * M₂.accepts

The concatenation ε-NFA accepts exactly the concatenation of the two DFA languages.

theorem Language.IsRegular.mul' {α : Type u_1} {L₁ L₂ : Language α} (h₁ : L₁.IsRegular) (h₂ : L₂.IsRegular) : (L₁ * L₂).IsRegular

Regular languages are closed under concatenation.

theorem RG_closedUnderConcatenation {α : Type} [Fintype α] : ClosedUnderConcatenation is_RG

The class of regular languages is closed under concatenation.