Documentation

Cslib.Computability.Languages.RegularLanguage

Regular languages #

source
theorem Language.IsRegular.iff_cslib_dfa {Symbol : Type u_1} {l : Language Symbol} :
l.IsRegular ↔ ∃ (State : Type) (_ : Finite State) (dfa : Cslib.Automata.DA.FinAcc State Symbol), Cslib.Automata.Acceptor.language dfa = l

A characterization of Language.IsRegular using Cslib.DA

source
theorem Language.IsRegular.iff_cslib_nfa {Symbol : Type u_1} {l : Language Symbol} :
l.IsRegular ↔ ∃ (State : Type) (_ : Finite State) (nfa : Cslib.Automata.NA.FinAcc State Symbol), Cslib.Automata.Acceptor.language nfa = l

A characterization of Language.IsRegular using Cslib.NA

source
@[simp]
theorem Language.IsRegular.compl {Symbol : Type u_1} {l : Language Symbol} (h : l.IsRegular) :
lᶜ.IsRegular
source
@[simp]
theorem Language.IsRegular.zero {Symbol : Type u_1} :
IsRegular 0
source
@[simp]
theorem Language.IsRegular.one {Symbol : Type u_1} :
IsRegular 1
source
@[simp]
theorem Language.IsRegular.top {Symbol : Type u_1} :
⊤.IsRegular
source
@[simp]
theorem Language.IsRegular.inf {Symbol : Type u_1} {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) :
(l1 ⊓ l2).IsRegular
source
@[simp]
theorem Language.IsRegular.add {Symbol : Type u_1} {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) :
(l1 + l2).IsRegular
source
@[simp]
theorem Language.IsRegular.iInf {Symbol : Type u_1} {I : Type u_2} [Finite I] {s : Set I} {l : I → Language Symbol} (h : ∀ i ∈ s, (l i).IsRegular) :
(⨅ i ∈ s, l i).IsRegular
source
@[simp]
theorem Language.IsRegular.iSup {Symbol : Type u_1} {I : Type u_2} [Finite I] {s : Set I} {l : I → Language Symbol} (h : ∀ i ∈ s, (l i).IsRegular) :
(⨆ i ∈ s, l i).IsRegular