Documentation

Linglib.Core.Computability.StarFree

Star-free languages #

A language is star-free when it is regular with an aperiodic syntactic monoid ([Sch65]) — the algebraic characterization of the star-free regular expressions (built from finite sets by ∪, ·, complement, no Kleene star), equivalently the counter-free / FO[<]-definable stringsets ([McNP71]). Taking the syntactic-monoid characterization as the definition mirrors the project's treatment of regularity (Language.isRegular_iff_finite_syntacticMonoid).

Star-free is the V = Monoid.aperiodicVariety instance of the Eilenberg correspondence: it is defined as aperiodicVariety.langs, so its closure properties are corollaries of the general keystone (Monoid.Pseudovariety.langs_*) rather than hand-written syntactic-monoid arguments.

Main definitions #

Main results #

source
def Language.IsStarFree {α : Type u_1} (L : Language α) :
Prop

A language is star-free ([Sch65]): the Monoid.aperiodicVariety instance of Monoid.Pseudovariety.langs — regular with an aperiodic syntactic monoid (isStarFree_iff). Star-free = FO[<]-definable = counter-free ([McNP71]).

Equations
Instances For
    source
    theorem Language.isStarFree_iff {α : Type u_1} {L : Language α} :
    L.IsStarFree ↔ L.IsRegular ∧ Monoid.IsAperiodic L.syntacticMonoid

    Star-free unfolds to: regular with an aperiodic syntactic monoid.

    source
    theorem Language.IsStarFree.isRegular {α : Type u_1} {L : Language α} (h : L.IsStarFree) :
    L.IsRegular
    source
    theorem Language.IsStarFree.isAperiodic {α : Type u_1} {L : Language α} (h : L.IsStarFree) :
    Monoid.IsAperiodic L.syntacticMonoid
    source
    theorem Language.IsStarFree.compl {α : Type u_1} {L : Language α} (h : L.IsStarFree) :
    Lᶜ.IsStarFree

    Star-free languages are closed under complement.

    source
    theorem Language.IsStarFree.inter {α : Type u_1} {L M : Language α} (hL : L.IsStarFree) (hM : M.IsStarFree) :
    (L ⊓ M).IsStarFree

    Star-free languages are closed under intersection.

    source
    theorem Language.IsStarFree.union {α : Type u_1} {L M : Language α} (hL : L.IsStarFree) (hM : M.IsStarFree) :
    (L ⊔ M).IsStarFree

    Star-free languages are closed under union.

    source
    theorem Language.IsStarFree.of_recognizes {α : Type u_1} {L : Language α} {M : Type u_2} [Monoid M] [Finite M] (hM : Monoid.IsAperiodic M) (η : FreeMonoid α →* M) (P : Set M) (hL : ∀ (w : List α), w ∈ L ↔ η (FreeMonoid.ofList w) ∈ P) :
    L.IsStarFree

    A language recognized by a finite aperiodic monoid is star-free — the algebraic characterization of star-free ([Sch65]). The engine for placing a constraint class inside SF: exhibit a finite aperiodic recognizer. Stays universe-polymorphic in the recognizer M (the keystone Monoid.Pseudovariety.langs_of_recognizes is its fixed-universe form).

    source
    theorem Language.IsStarFree.comap {α : Type u_2} {β : Type u_3} {L : Language β} (h : L.IsStarFree) (φ : FreeMonoid α →* FreeMonoid β) :
    IsStarFree {w : List α | φ (FreeMonoid.ofList w) ∈ L}

    Star-free languages are closed under inverse homomorphism. The engine for transferring a star-free upper bound across a string-rewriting projection (e.g. tier erasure: TSL ⊆ SF).

    source
    theorem Language.isStarFree_univ {α : Type u_1} :
    IsStarFree Set.univ

    The full language is star-free — recognized by the trivial monoid.