Thompson's construction

Thompson's construction turns a regular expression into an εNA with a single initial state and at most one accepting state [Tho68]. This file defines the automata it is assembled from, with their languages.

Main definitions

• εNA.FinAcc.zero, εNA.FinAcc.epsilon, εNA.FinAcc.char x: automata for the empty language, the empty word and the word [x].
• εNA.FinAcc.sum a b: the states and transitions of a and b side by side, through LTS.unionSum.
• εNA.FinAcc.union a b: sum a b with a single initial and a single accepting state, through toSingleStartAccept.
• εNA.FinAcc.concat a b: ε-transitions from the accepting states of a to the initial states of b.
• εNA.FinAcc.star a: a fresh hub state, initial and accepting, with ε-transitions to the initial states of a and from its accepting states.

Main statements

• εNA.FinAcc.language_zero, εNA.FinAcc.language_epsilon, εNA.FinAcc.language_char, εNA.FinAcc.language_sum, εNA.FinAcc.language_union, εNA.FinAcc.language_concat and εNA.FinAcc.language_star.

References

• K. Thompson, Regular expression search algorithm

def Cslib.Automata.εNA.FinAcc.zero {Symbol : Type u_1} : FinAcc Unit Symbol

An automaton with a single state, initial but not accepting, and no transitions.

Equations

• Cslib.Automata.εNA.FinAcc.zero = { Tr := fun (x : Unit) (x_1 : Option Symbol) (x_2 : Unit) => False, start := {()}, accept := ∅ }

def Cslib.Automata.εNA.FinAcc.epsilon {Symbol : Type u_1} : FinAcc Unit Symbol

An automaton with a single state, initial and accepting, and no transitions.

Equations

• Cslib.Automata.εNA.FinAcc.epsilon = { Tr := fun (x : Unit) (x_1 : Option Symbol) (x_2 : Unit) => False, start := {()}, accept := {()} }

def Cslib.Automata.εNA.FinAcc.char {Symbol : Type u_1} (x : Symbol) : FinAcc Bool Symbol

An automaton with two states, false initial and true accepting, joined by an x-transition.

Equations

• Cslib.Automata.εNA.FinAcc.char x = { Tr := fun (s : Bool) (μ : Option Symbol) (s' : Bool) => s = false ∧ μ = some x ∧ s' = true, start := {false}, accept := {true} }

@[simp]

theorem Cslib.Automata.εNA.FinAcc.language_zero {Symbol : Type u_1} : Acceptor.language zero = 0

@[simp]

theorem Cslib.Automata.εNA.FinAcc.language_epsilon {Symbol : Type u_1} : Acceptor.language epsilon = 1

@[simp]

theorem Cslib.Automata.εNA.FinAcc.language_char {Symbol : Type u_1} (x : Symbol) : Acceptor.language (char x) = {[x]}

def Cslib.Automata.εNA.FinAcc.sum {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (a : FinAcc S₁ Symbol) (b : FinAcc S₂ Symbol) : FinAcc (S₁ ⊕ S₂) Symbol

The disjoint sum of a and b: their states and transitions side by side (LTS.unionSum), with the initial and the accepting states of both.

Equations

• a.sum b = { toLTS := a.unionSum b.toLTS, start := Sum.inl '' a.start ∪ Sum.inr '' b.start, accept := Sum.inl '' a.accept ∪ Sum.inr '' b.accept }

@[simp]

theorem Cslib.Automata.εNA.FinAcc.language_sum {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (a : FinAcc S₁ Symbol) (b : FinAcc S₂ Symbol) : Acceptor.language (a.sum b) = Acceptor.language a + Acceptor.language b

def Cslib.Automata.εNA.FinAcc.union {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (a : FinAcc S₁ Symbol) (b : FinAcc S₂ Symbol) : FinAcc (Bool ⊕ S₁ ⊕ S₂) Symbol

The union of a and b: their disjoint sum, with a single initial state and a single accepting state added by toSingleStartAccept.

Equations

• a.union b = (a.sum b).toSingleStartAccept

@[simp]

theorem Cslib.Automata.εNA.FinAcc.language_union {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (a : FinAcc S₁ Symbol) (b : FinAcc S₂ Symbol) : Acceptor.language (a.union b) = Acceptor.language a + Acceptor.language b

inductive Cslib.Automata.εNA.FinAcc.ConcatTr {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (a : FinAcc S₁ Symbol) (b : FinAcc S₂ Symbol) : S₁ ⊕ S₂ → Option Symbol → S₁ ⊕ S₂ → Prop

The transitions of concat a b, whose states are those of a followed by those of b.

• left {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} {a : FinAcc S₁ Symbol} {b : FinAcc S₂ Symbol} {s : S₁} {μ : Option Symbol} {s' : S₁} : a.Tr s μ s' → a.ConcatTr b (Sum.inl s) μ (Sum.inl s')
• right {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} {a : FinAcc S₁ Symbol} {b : FinAcc S₂ Symbol} {s : S₂} {μ : Option Symbol} {s' : S₂} : b.Tr s μ s' → a.ConcatTr b (Sum.inr s) μ (Sum.inr s')
• bridge {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} {a : FinAcc S₁ Symbol} {b : FinAcc S₂ Symbol} {s : S₁} {s' : S₂} : s ∈ a.accept → s' ∈ b.start → a.ConcatTr b (Sum.inl s) none (Sum.inr s')

def Cslib.Automata.εNA.FinAcc.concat {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (a : FinAcc S₁ Symbol) (b : FinAcc S₂ Symbol) : FinAcc (S₁ ⊕ S₂) Symbol

The concatenation of a and b: ε-transitions lead from the accepting states of a to the initial states of b.

Equations

• a.concat b = { Tr := a.ConcatTr b, start := Sum.inl '' a.start, accept := Sum.inr '' b.accept }

theorem Cslib.Automata.εNA.FinAcc.concat_mTr_inr {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} {a : FinAcc S₁ Symbol} {b : FinAcc S₂ Symbol} {s t : S₂} {μs : List (Option Symbol)} (h : (a.concat b).MTr (Sum.inr s) μs (Sum.inr t)) : b.MTr s μs t

A run of concat a b between two states of b is a run of b.

theorem Cslib.Automata.εNA.FinAcc.concat_mTr_inl {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} {a : FinAcc S₁ Symbol} {b : FinAcc S₂ Symbol} {s : S₁} {t : S₂} {μs : List (Option Symbol)} (h : (a.concat b).MTr (Sum.inl s) μs (Sum.inr t)) : ∃ s₁ ∈ a.accept, ∃ s₂ ∈ b.start, ∃ (μs₁ : List (Option Symbol)) (μs₂ : List (Option Symbol)), a.MTr s μs₁ s₁ ∧ b.MTr s₂ μs₂ t ∧ μs = μs₁ ++ none :: μs₂

A run of concat a b from a state of a to a state of b is a run of a to an accepting state, an ε-transition to an initial state of b, and a run of b.

@[simp]

theorem Cslib.Automata.εNA.FinAcc.language_concat {Symbol : Type u_1} {S₁ : Type u_2} {S₂ : Type u_3} (a : FinAcc S₁ Symbol) (b : FinAcc S₂ Symbol) : Acceptor.language (a.concat b) = Acceptor.language a * Acceptor.language b

inductive Cslib.Automata.εNA.FinAcc.StarTr {Symbol : Type u_1} {S₁ : Type u_2} (a : FinAcc S₁ Symbol) : Unit ⊕ S₁ → Option Symbol → Unit ⊕ S₁ → Prop

The transitions of star a, whose states are a fresh hub inl () and the states of a.

• inner {Symbol : Type u_1} {S₁ : Type u_2} {a : FinAcc S₁ Symbol} {s : S₁} {μ : Option Symbol} {s' : S₁} : a.Tr s μ s' → a.StarTr (Sum.inr s) μ (Sum.inr s')
• enter {Symbol : Type u_1} {S₁ : Type u_2} {a : FinAcc S₁ Symbol} {s : S₁} : s ∈ a.start → a.StarTr (Sum.inl ()) none (Sum.inr s)
• exit {Symbol : Type u_1} {S₁ : Type u_2} {a : FinAcc S₁ Symbol} {s : S₁} : s ∈ a.accept → a.StarTr (Sum.inr s) none (Sum.inl ())

def Cslib.Automata.εNA.FinAcc.star {Symbol : Type u_1} {S₁ : Type u_2} (a : FinAcc S₁ Symbol) : FinAcc (Unit ⊕ S₁) Symbol

The Kleene star of a: a fresh hub state, initial and accepting, with ε-transitions to the initial states of a and from its accepting states.

Equations

• a.star = { Tr := a.StarTr, start := {Sum.inl ()}, accept := {Sum.inl ()} }

theorem Cslib.Automata.εNA.FinAcc.star_mTr_inr {Symbol : Type u_1} {S₁ : Type u_2} {a : FinAcc S₁ Symbol} {s : S₁} {μs : List (Option Symbol)} (h : a.star.MTr (Sum.inr s) μs (Sum.inl ())) : ∃ t ∈ a.accept, ∃ (μs₁ : List (Option Symbol)) (μs₂ : List (Option Symbol)), a.MTr s μs₁ t ∧ a.star.MTr (Sum.inl ()) μs₂ (Sum.inl ()) ∧ μs = μs₁ ++ none :: μs₂

A run of star a from a state of a to the hub is a run of a to an accepting state, an ε-transition to the hub, and a run from the hub back to the hub.

theorem Cslib.Automata.εNA.FinAcc.reduceOption_mem_kstar_of_star_mTr {Symbol : Type u_1} {S₁ : Type u_2} {a : FinAcc S₁ Symbol} {μs : List (Option Symbol)} (h : a.star.MTr (Sum.inl ()) μs (Sum.inl ())) : μs.reduceOption ∈ KStar.kstar (Acceptor.language a)

A run of star a from the hub back to the hub reads a word of (language a)∗.

theorem Cslib.Automata.εNA.FinAcc.exists_star_mTr_of_mem_kstar {Symbol : Type u_1} {S₁ : Type u_2} {a : FinAcc S₁ Symbol} {xs : List Symbol} (hxs : xs ∈ KStar.kstar (Acceptor.language a)) : ∃ (μs : List (Option Symbol)), μs.reduceOption = xs ∧ a.star.MTr (Sum.inl ()) μs (Sum.inl ())

Every word of (language a)∗ is read by a run of star a from the hub back to the hub.

@[simp]

theorem Cslib.Automata.εNA.FinAcc.language_star {Symbol : Type u_1} {S₁ : Type u_2} (a : FinAcc S₁ Symbol) : Acceptor.language a.star = KStar.kstar (Acceptor.language a)