Kleene's Algorithm

Kleene's algorithm constructs a regular expression by induction on a bound that restricts which interior states an execution may pass through. It is used to prove a direction of Cslib.Language.IsRegular.iff_regex, that every language accepted by a DFA comprised of finite states is the language of a regular expression. We implement Kleene's algorithm for the more general case of an NFA instead of DFA, since Execution is developed for LTS but not FLTS. The main theorem is NA.FinAcc.nfa_eq_regex.

Main definitions

• LTS.bddLang start last bound: The language of finite words that are accepted by an execution of an LTS with state type Fin n, where the start state is start, the last state is last, and all states of the execution except for the first and last are less than bound.
• LTS.regex s t r: The regular expression for the executions of an LTS with state type Fin n from state s to state t, whose interior states are all under the bound r.

Main results

• NA.FinAcc.nfa_eq_regex: Any NFA has a matching regular expression.
• LTS.bddLang_eq_nfa: LTS.bddLang is equal to the language of an NFA when bound is greater than or equal to the total number of states.
• LTS.bddLang_eq_regex: LTS.regex s t r matches the language LTS.bddLang s t r.

References

• J. E. Hopcroft, R. Motwani, J. D. Ullman, Introduction to Automata Theory, Languages, and Computation

def List.AllButFirstLast {α : Type u_1} (p : α → Bool) (as : List α) : Prop

All but the first and last elements of the list as satisfy the predicate p.

Equations

• List.AllButFirstLast p as = ∀ x ∈ as.tail.dropLast, p x = true

theorem List.allButFirstLast_iff_getElem {α : Type u_1} (p : α → Bool) (as : List α) : AllButFirstLast p as ↔ ∀ (i : ℕ) (x : 0 < i ∧ i < as.length - 1), p as[i] = true

theorem List.allButFirstLast_imp {α : Type u_1} {p q : α → Bool} {as : List α} (h : ∀ (x : α), p x = true → q x = true) (hp : AllButFirstLast p as) : AllButFirstLast q as

theorem List.allButFirstLast_append {α : Type u_1} {p : α → Bool} {as bs : List α} (hlen : 0 < as.length) (ha_last : p as[as.length - 1] = true) (ha : AllButFirstLast p as) (hb : AllButFirstLast p bs) : AllButFirstLast p (as ++ bs.tail)

def List.findIdxButFirstLast? {α : Type u_1} (p : α → Bool) (as : List α) : Option ℕ

The index of the first element in a list as that satisfies a predicate p, excluding the first and last element.

Equations

• List.findIdxButFirstLast? p as = Option.map (fun (x : ℕ) => x + 1) (List.findIdx? p as.tail.dropLast)

theorem List.findIdxButFirstLast?_isSome {α : Type u_1} (p : α → Bool) (as : List α) : (findIdxButFirstLast? p as).isSome = true ↔ ∃ x ∈ as.tail.dropLast, p x = true

theorem List.findIdxButFirstLast?_eq {α : Type u_1} {p : α → Bool} {as : List α} {i : ℕ} : findIdxButFirstLast? p as = some i ↔ ∃ (x : 0 < i ∧ i < as.length - 1), p as[i] = true ∧ ∀ (j : ℕ) (x_1 : 0 < j ∧ j < i), p as[j] = false

def List.findIdxButFirstLastRev? {α : Type u_1} (p : α → Bool) (as : List α) : Option ℕ

The index of the last element in a list as that satisfies a predicate p, excluding the first and last element.

Equations

• List.findIdxButFirstLastRev? p as = Option.map (fun (x : ℕ) => as.length - 1 - x) (List.findIdxButFirstLast? p as.reverse)

theorem List.findIdxButFirstLastRev?_eq {α : Type u_1} {p : α → Bool} {as : List α} {i : ℕ} : findIdxButFirstLastRev? p as = some i ↔ ∃ (x : 0 < i ∧ i < as.length - 1), p as[i] = true ∧ ∀ (j : ℕ) (x : i < j ∧ j < as.length - 1), p as[j] = false

def Cslib.LTS.BddExec {Symbol : Type u_1} {n : ℕ} (lts : LTS (Fin n) Symbol) (start : Fin n) (xs : List Symbol) (last : Fin n) (ss : List (Fin n)) (bound : ℕ) : Prop

An execution of an LTS with state type Fin n, where all states of the execution except for the first and last are less than bound.

Equations

• lts.BddExec start xs last ss bound = (lts.Execution start xs last ss ∧ List.AllButFirstLast (fun (s : Fin n) => decide (↑s < bound)) ss)

def Cslib.LTS.bddLang {Symbol : Type u_1} {n : ℕ} (lts : LTS (Fin n) Symbol) (start last : Fin n) (bound : ℕ) : Language Symbol

The language of finite words that are accepted by a BddExec.

Equations

• lts.bddLang start last bound = {xs : List Symbol | ∃ (ss : List (Fin n)), lts.BddExec start xs last ss bound}

theorem Cslib.LTS.bddLang_bound_zero {Symbol : Type u_1} {n : ℕ} (lts : LTS (Fin n) Symbol) (s t : Fin n) {xs : List Symbol} (hxs : ¬xs = []) : xs ∈ lts.bddLang s t 0 ↔ ∃ (a : Symbol), lts.Tr s a t ∧ xs = [a]

theorem Cslib.LTS.bddLang_eq_nfa {Symbol : Type u_1} {n : ℕ} (lts : LTS (Fin n) Symbol) (s t : Fin n) {r : ℕ} : n ≤ r → lts.bddLang s t r = Automata.Acceptor.language { toLTS := lts, start := {s}, accept := {t} }

def Cslib.LTS.splitFirstTake {Symbol : Type u_1} {n : ℕ} (xs : List Symbol) (ss : List (Fin n)) (r : Fin n) : List Symbol

With an execution of the string xs through states ss, splitFirstTake xs ss r returns a prefix of xs which ends at the FIRST occurrence (excluding the first and last state) of state r in ss. When no such occurrence of r exists, splitFirstTake returns the empty string; however, the current file does not use the splitFirstTake in such situation. The actual definition does not require an execution, just the string xs and the states ss.

Equations

• Cslib.LTS.splitFirstTake xs ss r = match List.findIdxButFirstLast? (fun (x : Fin n) => decide (x = r)) ss with | none => [] | some i => List.take i xs

def Cslib.LTS.splitFirstDrop {Symbol : Type u_1} {n : ℕ} (xs : List Symbol) (ss : List (Fin n)) (r : Fin n) : List Symbol

With an execution of the string xs through states ss, splitFirstDrop xs ss r returns a suffix of xs which starts at the FIRST occurrence (excluding the first and last state) of state r in ss. When no such occurrence of r exists, splitFirstDrop returns the full string; however, the current file does not use the splitFirstDrop in such situation. The actual definition does not require an execution, just the string xs and the states ss.

Equations

• Cslib.LTS.splitFirstDrop xs ss r = match List.findIdxButFirstLast? (fun (x : Fin n) => decide (x = r)) ss with | none => xs | some i => List.drop i xs

theorem Cslib.LTS.splitFirst_mem {Symbol : Type u_1} {n : ℕ} {lts : LTS (Fin n) Symbol} {s t r : Fin n} {xs : List Symbol} {ss : List (Fin n)} (hex : lts.Execution s xs t ss) (hbdd : List.AllButFirstLast (fun (x : Fin n) => decide (x ≤ r)) ss) (hbdd' : ¬List.AllButFirstLast (fun (x : Fin n) => decide (x < r)) ss) : splitFirstTake xs ss r ∈ lts.bddLang s r ↑r ∧ splitFirstDrop xs ss r ∈ lts.bddLang r t (↑r + 1)

theorem Cslib.LTS.bddLang_splitFirst {Symbol : Type u_1} {n : ℕ} (lts : LTS (Fin n) Symbol) (s t r : Fin n) : lts.bddLang s t (↑r + 1) = lts.bddLang s t ↑r + lts.bddLang s r ↑r * lts.bddLang r t (↑r + 1)

Part of the recursion step of Kleene's algorithm. A run from s to t whose interior states are ≤ r either has all interior states < r, or it splits at its first visit to r into an execution from s to r with all interior states < r, followed by an execution from r to t with all interior states ≤ r.

def Cslib.LTS.splitLastTake {Symbol : Type u_1} {n : ℕ} (xs : List Symbol) (ss : List (Fin n)) (r : Fin n) : List Symbol

With an execution of the string xs through states ss, splitLastTake xs ss r returns a prefix of xs which ends at the LAST occurrence (excluding the first and last state) of state r in ss. When no such occurrence of r exists, splitLastTake returns the empty string. The actual definition does not require an execution, just the string xs and the states ss.

Equations

• Cslib.LTS.splitLastTake xs ss r = match List.findIdxButFirstLastRev? (fun (x : Fin n) => decide (x = r)) ss with | none => [] | some i => List.take i xs

def Cslib.LTS.splitLastDrop {Symbol : Type u_1} {n : ℕ} (xs : List Symbol) (ss : List (Fin n)) (r : Fin n) : List Symbol

With an execution of the string xs through states ss, splitLastDrop xs ss r returns a prefix of xs which ends at the LAST occurrence (excluding the first and last state) of state r in ss. When no such occurrence of r exists, splitLastDrop returns the full string. The actual definition does not require an execution, just the string xs and the states ss.

Equations

• Cslib.LTS.splitLastDrop xs ss r = match List.findIdxButFirstLastRev? (fun (x : Fin n) => decide (x = r)) ss with | none => xs | some i => List.drop i xs

theorem Cslib.LTS.splitLast_mem {Symbol : Type u_1} {n : ℕ} {lts : LTS (Fin n) Symbol} {t r : Fin n} {xs : List Symbol} {ss : List (Fin n)} (hex : lts.Execution r xs t ss) (hbdd : List.AllButFirstLast (fun (x : Fin n) => decide (x ≤ r)) ss) : splitLastTake xs ss r ∈ lts.bddLang r r (↑r + 1) ∧ splitLastDrop xs ss r ∈ lts.bddLang r t ↑r

theorem Cslib.LTS.splitLastDrop_mem_nonempty {Symbol : Type u_1} {n : ℕ} {lts : LTS (Fin n) Symbol} {t r : Fin n} {xs : List Symbol} {ss : List (Fin n)} (hxs : xs ≠ []) (hex : lts.Execution r xs t ss) (hbdd : List.AllButFirstLast (fun (x : Fin n) => decide (x ≤ r)) ss) : splitLastDrop xs ss r ∈ lts.bddLang r t ↑r - 1

theorem Cslib.LTS.bddLang_splitLast {Symbol : Type u_1} {n : ℕ} (lts : LTS (Fin n) Symbol) (t r : Fin n) : lts.bddLang r t (↑r + 1) = lts.bddLang r r (↑r + 1) * lts.bddLang r t ↑r

Part of the recursion step of Kleene's algorithm. An execution from r to t whose interior states are ≤ r splits at its last visit to r into an execution from r to r with all interior states ≤ r, followed by an execution from r to t with all interior states < r.

theorem Cslib.LTS.bddLang_kstar {Symbol : Type u_1} {n : ℕ} (lts : LTS (Fin n) Symbol) (r : Fin n) : lts.bddLang r r (↑r + 1) = KStar.kstar (lts.bddLang r r ↑r)

Part of the recursion step of Kleene's algorithm. An execution from r to r whose interior states are ≤ r is a concatenation of executions from r to r whose interior states are all ≤ r.

noncomputable def Cslib.LTS.regex {Symbol : Type u_1} {n : ℕ} [Finite Symbol] (lts : LTS (Fin n) Symbol) (s t : Fin n) : ℕ → RegularExpression Symbol

regex s t r is the regular expression for the path from state s to t passing through states < r. When r = 0, s = t, the regex is empty string ε union all characters from state s to s. When r = 0, s ≠ t, the regex is all characters from state s to t. For r + 1, the regex is the union of regex s t r and (regex s r r) (regex r r r)∗ (regex r t r).

Equations

• lts.regex s t 0 = if s = t then 1 + (List.map RegularExpression.char ⋯.toFinset.toList).sum else (List.map RegularExpression.char ⋯.toFinset.toList).sum
• lts.regex s t r.succ = if h : n ≤ r then lts.regex s t r else have rFin := ⟨r, ⋯⟩; lts.regex s t r + lts.regex s rFin r * (lts.regex rFin rFin r).star * lts.regex rFin t r

theorem Cslib.LTS.bddLang_eq_regex {Symbol : Type u_1} {n : ℕ} [Finite Symbol] {r : ℕ} {lts : LTS (Fin n) Symbol} {s t : Fin n} : lts.bddLang s t r = (lts.regex s t r).matches'

LTS.regex s t r matches the language LTS.bddLang s t r.

theorem Cslib.LTS.fin_nfa_single_start_accept_eq_regex {Symbol : Type u_1} {n : ℕ} [Finite Symbol] (lts : LTS (Fin n) Symbol) (s t : Fin n) : Automata.Acceptor.language { toLTS := lts, start := {s}, accept := {t} } = (lts.regex s t n).matches'

An NFA with state type Fin n and with exactly one start state s and exactly one accept state t has a matching regular expression given by LTS.regex s t n.

theorem Cslib.Automata.NA.FinAcc.nfa_single_start_accept_reindex {Symbol : Type u_1} {State : Type u_2} {State' : Type u_3} (nfa : FinAcc State Symbol) (e : State ≃ State') {s t : State} (hstart : nfa.start = {s}) (haccept : nfa.accept = {t}) : Acceptor.language nfa = Acceptor.language { toLTS := nfa.reindex e, start := {e s}, accept := {e t} }

theorem Cslib.Automata.NA.FinAcc.nfa_single_start_accept_eq_regex {Symbol : Type u_1} {State : Type u_2} [Finite Symbol] [Finite State] (nfa : FinAcc State Symbol) (s t : State) (hstart : nfa.start = {s}) (haccept : nfa.accept = {t}) : ∃ (r : RegularExpression Symbol), Acceptor.language nfa = r.matches'

An NFA with exactly one start state and exactly one accept state has a matching regular expression.

theorem Cslib.Automata.NA.FinAcc.nfa_eq_regex {Symbol : Type u_1} {State : Type u_2} [Finite Symbol] [Finite State] (nfa : FinAcc State Symbol) : ∃ (r : RegularExpression Symbol), Acceptor.language nfa = r.matches'

Any NFA has a matching regular expression.