Documentation

Cslib.Computability.Languages.OmegaRegularLanguage

ω-Regular languages #

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

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

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

Equations
Instances For
    source
    theorem Cslib.ωLanguage.isRegular_iff {Symbol : Type u} {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.

    source
    theorem Cslib.ωLanguage.IsRegular.of_da_buchi {Symbol : Type u} {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.

    source
    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.

    source
    @[simp]
    theorem Cslib.ωLanguage.IsRegular.regular_omegaLim {Symbol : Type u} {l : Language Symbol} (h : l.IsRegular) :
    l↗ω.IsRegular

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

    source
    @[simp]
    theorem Cslib.ωLanguage.IsRegular.bot {Symbol : Type u} :
    ⊥.IsRegular

    The empty language is ω-regular.

    source
    @[simp]
    theorem Cslib.ωLanguage.IsRegular.sup {Symbol : Type u} {p1 p2 : ωLanguage Symbol} (h1 : p1.IsRegular) (h2 : p2.IsRegular) :
    (p1 ⊔ p2).IsRegular

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

    source
    @[simp]
    theorem Cslib.ωLanguage.IsRegular.iSup {Symbol : Type u} {I : Type u_1} [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.