ω-Regular languages

This file defines ω-regular languages and proves some properties of them.

def Cslib.ωLanguage.IsRegular {Symbol : Type u_1} (p : ωLanguage Symbol) : Prop

An ω-language is ω-regular iff it is accepted by a finite-state nondeterministic Buchi automaton.

Equations

• p.IsRegular = ∃ (State : Type) (_ : Finite State) (na : Cslib.Automata.NA.Buchi State Symbol), Cslib.Automata.ωAcceptor.language na = p

theorem Cslib.ωLanguage.isRegular_iff {Symbol : Type u_1} {p : ωLanguage Symbol} : p.IsRegular ↔ ∃ (σ : Type v) (_ : Finite σ) (na : Automata.NA.Buchi σ Symbol), Automata.ωAcceptor.language na = p

The state space of the accepting finite-state nondeterministic Buchi automaton can in fact be universe-polymorphic.

theorem Cslib.ωLanguage.IsRegular.of_da_buchi {Symbol : Type u_1} {State : Type} [Finite State] (da : Automata.DA.Buchi State Symbol) : (Automata.ωAcceptor.language da).IsRegular

The ω-language accepted by a finite-state deterministic Buchi automaton is ω-regular.

theorem Cslib.ωLanguage.IsRegular.not_da_buchi : ∃ (Symbol : Type) (p : ωLanguage Symbol), p.IsRegular ∧ ¬∃ (State : Type) (da : Automata.DA.Buchi State Symbol), Automata.ωAcceptor.language da = p

There is an ω-regular language that is not accepted by any deterministic Buchi automaton, where the automaton is not even required to be finite-state.

@[simp]

theorem Cslib.ωLanguage.IsRegular.regular_omegaLim {Symbol : Type u_1} {l : Language Symbol} (h : l.IsRegular) : l↗ω.IsRegular

The ω-limit of a regular language is ω-regular.

@[simp]

theorem Cslib.ωLanguage.IsRegular.bot {Symbol : Type u_1} : ⊥.IsRegular

The empty language is ω-regular.

@[simp]

theorem Cslib.ωLanguage.IsRegular.top {Symbol : Type u_1} : ⊤.IsRegular

The language of all ω-sequences is ω-regular.

@[simp]

theorem Cslib.ωLanguage.IsRegular.sup {Symbol : Type u_1} {p1 p2 : ωLanguage Symbol} (h1 : p1.IsRegular) (h2 : p2.IsRegular) : (p1 ⊔ p2).IsRegular

The union of two ω-regular languages is ω-regular.

@[simp]

theorem Cslib.ωLanguage.IsRegular.inf {Symbol : Type u_1} {p1 p2 : ωLanguage Symbol} (h1 : p1.IsRegular) (h2 : p2.IsRegular) : (p1 ⊓ p2).IsRegular

The intersection of two ω-regular languages is ω-regular.

@[simp]

theorem Cslib.ωLanguage.IsRegular.iSup {Symbol : Type u_1} {I : Type u_2} [Finite I] {s : Set I} {p : I → ωLanguage Symbol} (h : ∀ i ∈ s, (p i).IsRegular) : (⨆ i ∈ s, p i).IsRegular

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

@[simp]

theorem Cslib.ωLanguage.IsRegular.iInf {Symbol : Type u_1} {I : Type u_2} [Finite I] {s : Set I} {p : I → ωLanguage Symbol} (h : ∀ i ∈ s, (p i).IsRegular) : (⨅ i ∈ s, p i).IsRegular

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

@[simp]

theorem Cslib.ωLanguage.IsRegular.hmul {Symbol : Type u_1} {l : Language Symbol} {p : ωLanguage Symbol} (h1 : l.IsRegular) (h2 : p.IsRegular) : (l * p).IsRegular

The concatenation of a regular language and an ω-regular language is ω-regular.

@[simp]

theorem Cslib.ωLanguage.IsRegular.omegaPow {Symbol : Type u_1} [Inhabited Symbol] {l : Language Symbol} (h : l.IsRegular) : l^ω.IsRegular

The ω-power of a regular language is an ω-regular language.

theorem Cslib.ωLanguage.IsRegular.eq_fin_iSup_hmul_omegaPow {Symbol : Type u_1} [Inhabited Symbol] (p : ωLanguage Symbol) : p.IsRegular ↔ ∃ (n : ℕ) (l : Fin n → Language Symbol) (m : Fin n → Language Symbol), (∀ (i : Fin n), (l i).IsRegular ∧ (m i).IsRegular) ∧ p = ⨆ (i : Fin n), l i * (m i)^ω

An ω-language is regular iff it is the finite union of ω-languages of the form L * M^ω, where all Ls and Ms are regular languages.

theorem Cslib.ωLanguage.IsRegular.fin_cover_saturates {Symbol : Type u_1} {I : Type u_2} [Finite I] {p : I → ωLanguage Symbol} {q : ωLanguage Symbol} (hs : Set.Saturates p q) (hc : ⨆ (i : I), p i = ⊤) (hr : ∀ (i : I), (p i).IsRegular) : q.IsRegular

If an ω-language has a finite saturating cover made of ω-regular languages, then it is an ω-regular language.

theorem Cslib.ωLanguage.IsRegular.fin_cover_saturates_compl {Symbol : Type u_1} {I : Type u_2} [Finite I] {p : I → ωLanguage Symbol} {q : ωLanguage Symbol} (hs : Set.Saturates p q) (hc : ⨆ (i : I), p i = ⊤) (hr : ∀ (i : I), (p i).IsRegular) : qᶜ.IsRegular

If an ω-language has a finite saturating cover made of ω-regular languages, then its complement is an ω-regular language.