Thompson's construction

11 fully proved

Basic automata

DefinitionThe ε-NFA with no states#✓fully proved

Over an alphabet \(\alpha\), this is the ε-NFA whose set of states is empty; consequently it has no start states, no accepting states and no transitions.

def zeroAut : εNFA α Empty := ⟨fun s => s.elim, ∅, ∅⟩

Used by 2

Used byCorrectness of Thompson's construction · Thompson's construction

DefinitionOne-state automaton#✓fully proved

The ε-NFA over the alphabet \(\alpha\) with a single state, which is both its start state and its accepting state, and no moves at all (neither letter moves nor ε-moves).

def oneAut : εNFA α Unit := ⟨fun _ _ => ∅, {()}, {()}⟩

Used by 2

Used byCorrectness of Thompson's construction · Thompson's construction

DefinitionSingle-letter automaton#✓fully proved

For a letter \(a\) of the alphabet \(\alpha\), this is the ε-NFA over \(\alpha\) with two states, a start state and an accepting state, and a single move, which reads \(a\) and goes from the start state to the accepting state; it has no other moves and no ε-moves.

def charAut (a : α) : εNFA α Bool :=
  ⟨fun s c => {t | s = false ∧ c = some a ∧ t = true}, {false}, {true}⟩

Used by 2

Used byCorrectness of Thompson's construction · Thompson's construction

Union

DefinitionUnion of ε-NFAs#✓fully proved

Given ε-NFAs \(M\) with state set \(\sigma\) and \(N\) with state set \(\tau\) over the same alphabet, their union is the ε-NFA on the disjoint union \(\sigma \sqcup \tau\) whose moves are the moves of \(M\) and the moves of \(N\), whose start states are the start states of \(M\) and of \(N\), and whose accepting states are the accepting states of \(M\) and of \(N\).

def union : εNFA α (σ ⊕ τ) where
  step
    | .inl s, c => .inl '' M.step s c
    | .inr t, c => .inr '' N.step t c
  start := .inl '' M.start ∪ .inr '' N.start
  accept := .inl '' M.accept ∪ .inr '' N.accept

Used by 2

Used byCorrectness of Thompson's construction · Thompson's construction

Concatenation

DefinitionConcatenation of ε-NFAs#✓fully proved

Given ε-NFAs \(M\) with state set \(\sigma\) and \(N\) with state set \(\tau\) over the same alphabet, their concatenation is the ε-NFA on the disjoint union \(\sigma \sqcup \tau\) whose moves are the moves of \(M\), the moves of \(N\), and an ε-move from every accepting state of \(M\) to every start state of \(N\). Its start states are the start states of \(M\) and its accepting states are the accepting states of \(N\).

def concat : εNFA α (σ ⊕ τ) where
  step
    | .inl s, c => .inl '' M.step s c ∪ {u | c = none ∧ s ∈ M.accept ∧ ∃ q ∈ N.start, u = .inr q}
    | .inr t, c => .inr '' N.step t c
  start := .inl '' M.start
  accept := .inr '' N.accept

Used by 2

Used byCorrectness of Thompson's construction · Thompson's construction

Kleene star

DefinitionKleene star of an ε-NFA#✓fully proved

Given an ε-NFA \(M\) with state set \(\sigma\), its star automaton has the states of \(M\) together with one new state \(q_0\), which is its only start state and its only accepting state. Its moves are the moves of \(M\), an ε-move from \(q_0\) to every start state of \(M\), and an ε-move from every accepting state of \(M\) to \(q_0\).

def star : εNFA α (Option σ) where
  step
    | none, c => {u | c = none ∧ ∃ q ∈ M.start, u = some q}
    | some s, c => some '' M.step s c ∪ {u | c = none ∧ s ∈ M.accept ∧ u = none}
  start := {none}
  accept := {none}

Used by 2

Used byCorrectness of Thompson's construction · Thompson's construction

The construction

DefinitionStates of Thompson's automaton#✓fully proved

The state set \(S(r)\) of Thompson's automaton of a regular expression \(r\) is defined by structural recursion: \(S(0)\) is empty, \(S(\varepsilon)\) has one element, \(S(a)\) has two elements for a letter \(a\), both \(S(P + Q)\) and \(S(PQ)\) are the disjoint union \(S(P) \sqcup S(Q)\), and \(S(P^*)\) is \(S(P)\) together with one new element.

def State : RegularExpression α → Type
  | .zero => Empty
  | .epsilon => Unit
  | .char _ => Bool
  | .plus P Q => State P ⊕ State Q
  | .comp P Q => State P ⊕ State Q
  | .star P => Option (State P)

Used by 4

Used byShort distinguishing words · Correctness of Thompson's construction · Number of states of Thompson's automaton · Thompson's construction

DefinitionThompson's construction#✓fully proved

To each regular expression \(r\) over an alphabet \(\alpha\) it assigns an ε-NFA over \(\alpha\) with state set \(S(r)\), the states of Thompson's automaton of \(r\), by structural recursion: \(0\) goes to the automaton with no states, \(\varepsilon\) to the one-state automaton, a letter \(a\) to the single-letter automaton of \(a\), \(P + Q\) to the union of the automata of \(P\) and \(Q\), \(PQ\) to their concatenation, and \(P^*\) to the star automaton of the automaton of \(P\).

def toεNFA : (r : RegularExpression α) → εNFA α (State r)
  | .zero => zeroAut
  | .epsilon => oneAut
  | .char a => charAut a
  | .plus P Q => union (toεNFA P) (toεNFA Q)
  | .comp P Q => concat (toεNFA P) (toεNFA Q)
  | .star P => star (toεNFA P)

Uses 7 · Used by 2

Statement usesStates of Thompson's automaton · Single-letter automaton · Concatenation of ε-NFAs · One-state automaton · Kleene star of an ε-NFA · Union of ε-NFAs · The ε-NFA with no states

Used byShort distinguishing words · Correctness of Thompson's construction

TheoremCorrectness of Thompson's construction#✓fully proved

The automaton accepts exactly the words the regular expression matches.

theorem accepts_toεNFA (r : RegularExpression α) : (toεNFA r).accepts = r.matches'

Uses 8 · Used by 1

Statement usesStates of Thompson's automaton · Thompson's construction

Proof usesSingle-letter automaton · Concatenation of ε-NFAs · One-state automaton · Kleene star of an ε-NFA · Union of ε-NFAs · The ε-NFA with no states

Used byShort distinguishing words

DefinitionThompson state count#✓fully proved

The state count \(n(r)\) of a regular expression \(r\) is defined by structural recursion: \(n(0) = 0\), \(n(\varepsilon) = 1\), \(n(a) = 2\) for a letter \(a\), \(n(P + Q) = n(P) + n(Q)\), \(n(PQ) = n(P) + n(Q)\) and \(n(P^*) = n(P) + 1\).

It is the number of states of Thompson's automaton of \(r\).

def numStates : RegularExpression α → ℕ
  | .zero => 0
  | .epsilon => 1
  | .char _ => 2
  | .plus P Q => numStates P + numStates Q
  | .comp P Q => numStates P + numStates Q
  | .star P => numStates P + 1

Used by 5

Used byThe pass computes the Thompson state count of every node · Short distinguishing words · Short distinguishing words for encoded regular expressions · The pass counts the states of Thompson's automaton · Number of states of Thompson's automaton

TheoremNumber of states of Thompson's automaton#✓fully proved

For every regular expression \(r\), the number of states of Thompson's automaton of \(r\) is \(n(r)\), the Thompson state count of \(r\): \(n(0) = 0\), \(n(\varepsilon) = 1\), \(n(a) = 2\) for a letter \(a\), \(n(P + Q) = n(P) + n(Q)\), \(n(PQ) = n(P) + n(Q)\) and \(n(P^*) = n(P) + 1\).

theorem card_state (r : RegularExpression α) : Fintype.card (State r) = numStates r

Uses 2 · Used by 1

Statement usesStates of Thompson's automaton · Thompson state count

Used byShort distinguishing words

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.