Documentation

Cslib.Computability.Languages.RegularLanguage

Regular languages #

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

A characterization of Language.IsRegular in terms of DA. This is the only theorem in Cslib in which Mathlib's definition of Language.IsRegular is used.

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

A characterization of Language.IsRegular in terms of NA.

source
theorem Cslib.Language.IsRegular.compl {Symbol : Type u_1} {l : Language Symbol} (h : l.IsRegular) :
lᶜ.IsRegular

The complementation of a regular language is regular.

source
@[simp]
theorem Cslib.Language.IsRegular.zero {Symbol : Type u_1} :
Language.IsRegular 0

The empty language is regular.

source
@[simp]
theorem Cslib.Language.IsRegular.one {Symbol : Type u_1} :
Language.IsRegular 1

The language containing only the empty word is regular.

source
@[simp]
theorem Cslib.Language.IsRegular.top {Symbol : Type u_1} :
⊤.IsRegular

The language of all finite words is regular.

source
@[simp]
theorem Cslib.Language.IsRegular.inf {Symbol : Type u_1} {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) :
(l1 ⊓ l2).IsRegular

The intersection of two regular languages is regular.

source
@[simp]
theorem Cslib.Language.IsRegular.add {Symbol : Type u_1} {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) :
(l1 + l2).IsRegular

The union of two regular languages is regular.

source
@[simp]
theorem Cslib.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

The intersection of any finite number of regular languages is regular.

source
@[simp]
theorem Cslib.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

The union of any finite number of regular languages is regular.

source
@[simp]
theorem Cslib.Language.IsRegular.mul {Symbol : Type u_1} [Inhabited Symbol] {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) :
(l1 * l2).IsRegular

The concatenation of two regular languages is regular.

source
@[simp]
theorem Cslib.Language.IsRegular.kstar {Symbol : Type u_1} [Inhabited Symbol] {l : Language Symbol} (h : l.IsRegular) :
(KStar.kstar l).IsRegular

The Kleene star of a regular language is regular.