Regular Closure Under Prefix

Proof idea: a word is a prefix of some word in L exactly when the DFA state reached after reading it can still reach an accepting state. Mark those co-reachable states as accepting in a new DFA.

Regular Closure Under Prefix

This file proves that regular languages are closed under the prefix operation and shows that the converse fails over any nontrivial alphabet.

Main declarations

• DFA.reachableAccept
• DFA.prefixDFA
• Language.IsRegular.prefixLang
• Language.not_iff_regular_prefix

def DFA.reachableAccept {α : Type u_1} {σ : Type u_2} (M : DFA α σ) : Set σ

The set of states from which some accepting state is reachable.

Equations

• M.reachableAccept = {s : σ | ∃ (x : List α), M.evalFrom s x ∈ M.accept}

def DFA.prefixDFA {α : Type u_1} {σ : Type u_2} (M : DFA α σ) : DFA α σ

A DFA accepting the prefix language of the original DFA's language.

Equations

• M.prefixDFA = { step := M.step, start := M.start, accept := M.reachableAccept }

theorem DFA.evalFrom_prefixDFA {α : Type u_1} {σ : Type u_2} (M : DFA α σ) (s : σ) (x : List α) : M.prefixDFA.evalFrom s x = M.evalFrom s x

theorem DFA.mem_prefixDFA_accept {α : Type u_1} {σ : Type u_2} (M : DFA α σ) (s : σ) : s ∈ M.prefixDFA.accept ↔ ∃ (x : List α), M.evalFrom s x ∈ M.accept

theorem DFA.prefixDFA_accepts {α : Type u_1} {σ : Type u_2} (M : DFA α σ) : M.prefixDFA.accepts = M.accepts.prefixLang

The prefix DFA accepts exactly the prefix language of the original DFA.

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

Regular languages are closed under the prefix operation.

theorem Language.not_iff_regular_prefix {α : Type u_1} [Nontrivial α] : ¬∀ (L : Language α), L.prefixLang.IsRegular ↔ L.IsRegular

The converse of prefix closure fails over any nontrivial alphabet.