Regular Closure Under Right Quotient

Proof idea: after reading the candidate prefix u, accept if there exists a suffix from the quotient language that can take the original DFA from the current state to an accepting state. This existential set of good states is used as the accepting predicate of a new DFA.

Regular Closure Under Right Quotient

This file proves that regular languages are closed under right quotient with any language. This generalises closure under prefix (which is the special case R = Set.univ).

Given a DFA M accepting L and an arbitrary language R, the quotient DFA keeps the same transition function and start state but changes the accepting states to those from which some word in R can drive M to an original accepting state.

Main declarations

• DFA.quotientAccept
• DFA.quotientDFA
• Language.IsRegular.rightQuotient

def DFA.quotientAccept {α : Type u_1} {σ : Type u_2} (M : DFA α σ) (R : Language α) : Set σ

The set of states from which some word in R leads to an accepting state of M.

Equations

• M.quotientAccept R = {s : σ | ∃ v ∈ R, M.evalFrom s v ∈ M.accept}

def DFA.quotientDFA {α : Type u_1} {σ : Type u_2} (M : DFA α σ) (R : Language α) : DFA α σ

A DFA accepting the right quotient of M's language by R.

Equations

• M.quotientDFA R = { step := M.step, start := M.start, accept := M.quotientAccept R }

theorem DFA.evalFrom_quotientDFA {α : Type u_1} {σ : Type u_2} (M : DFA α σ) (R : Language α) (s : σ) (x : List α) : (M.quotientDFA R).evalFrom s x = M.evalFrom s x

theorem DFA.mem_quotientDFA_accept {α : Type u_1} {σ : Type u_2} (M : DFA α σ) (R : Language α) (s : σ) : s ∈ (M.quotientDFA R).accept ↔ ∃ v ∈ R, M.evalFrom s v ∈ M.accept

theorem DFA.quotientDFA_accepts {α : Type u_1} {σ : Type u_2} (M : DFA α σ) (R : Language α) : (M.quotientDFA R).accepts = M.accepts / R

The quotient DFA accepts exactly the right quotient of the original language by R.

theorem Language.IsRegular.rightQuotient {α : Type u_1} {L : Language α} (hL : L.IsRegular) (R : Language α) : (L / R).IsRegular

Regular languages are closed under right quotient with any language.

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

prefixLang as a special case of rightQuotient for regular languages.

theorem RG_closedUnderRightQuotient {α : Type} [Fintype α] : ClosedUnderRightQuotient is_RG

The class of regular languages is closed under right quotient with any language.

theorem RG_closedUnderRightQuotientWithRegular {α : Type} [Fintype α] : ClosedUnderRightQuotientWithRegular is_RG

The class of regular languages is closed under right quotient with regular languages.