The ε-NA of a regular expression

Thompson's construction [Tho68]: every regular expression is sent to an εNA with finitely many states that accepts exactly its language, by assembling the automata of Cslib.Computability.Automata.EpsilonNA.ThompsonConstruction.

Main definitions

• RegularExpression.State r: the states of the automaton of r.
• RegularExpression.toEpsilonNA r: the automaton of r.

Main statements

• RegularExpression.language_toEpsilonNA: the automaton of r accepts exactly r.matches'.

References

• K. Thompson, Regular expression search algorithm

def RegularExpression.State {α : Type u_1} : RegularExpression α → Type

The states of the automaton of a regular expression.

Equations

• RegularExpression.zero.State = Unit
• RegularExpression.epsilon.State = Unit
• (RegularExpression.char a).State = Bool
• (P.plus Q).State = (Bool ⊕ P.State ⊕ Q.State)
• (P.comp Q).State = (P.State ⊕ Q.State)
• P.star.State = (Unit ⊕ P.State)

instance RegularExpression.instFiniteState {α : Type u_1} (r : RegularExpression α) : Finite r.State

The automaton of a regular expression has finitely many states.

def RegularExpression.toEpsilonNA {α : Type u_1} (r : RegularExpression α) : Cslib.Automata.εNA.FinAcc r.State α

Thompson's construction: the εNA of a regular expression.

Equations

• RegularExpression.zero.toEpsilonNA = Cslib.Automata.εNA.FinAcc.zero
• RegularExpression.epsilon.toEpsilonNA = Cslib.Automata.εNA.FinAcc.epsilon
• (RegularExpression.char a).toEpsilonNA = Cslib.Automata.εNA.FinAcc.char a
• (P.plus Q).toEpsilonNA = P.toEpsilonNA.union Q.toEpsilonNA
• (P.comp Q).toEpsilonNA = P.toEpsilonNA.concat Q.toEpsilonNA
• P.star.toEpsilonNA = P.toEpsilonNA.star

@[simp]

theorem RegularExpression.language_toEpsilonNA {α : Type u_1} (r : RegularExpression α) : Cslib.Automata.Acceptor.language r.toEpsilonNA = r.matches'

The automaton of a regular expression accepts exactly its language.