Documentation

Linglib.Core.Computability.StarFree

Star-free languages #

This file defines the star-free languages as the regular languages with an aperiodic syntactic monoid. By Schützenberger's theorem these are the languages of the star-free regular expressions, built from finite sets by union, concatenation and complement without Kleene star; McNaughton and Papert show that they are also the counter-free and the first-order definable languages. Star-free is the instance Monoid.aperiodicVariety of the languages of a pseudovariety, so its closure properties are corollaries of Monoid.Pseudovariety.langs.

Main definitions #

Main results #

References #

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

A language is star-free when its syntactic monoid is finite and aperiodic, that is, when it is a language of the pseudovariety of aperiodic monoids.

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

    A language is star-free exactly when it is 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. Unlike Monoid.Pseudovariety.langs_of_recognizes, the recognizer may live in any universe.

    source
    theorem Language.IsStarFree.of_factorsThrough {α : Type u_1} {L : Language α} {β : Type u_2} {g : List α → β} {n : ℕ} (hL : Function.FactorsThrough (fun (x : List α) => x ∈ L) g) (hg : ∀ ⦃u u' v v' : List α⦄, g u = g u' → g v = g v' → g (u ++ v) = g (u' ++ v')) (hfin : (Set.range g).Finite) (hpow : ∀ (w : List α), g (List.replicate (n + 1) w).flatten = g (List.replicate n w).flatten) :
    L.IsStarFree

    A language is star-free when membership factors through a map g with finite range that respects concatenation and takes the same value on n + 1 copies of a word as on n.

    source
    theorem Language.IsStarFree.exists_flatten_replicate_succ_mem_iff {α : Type u_1} {L : Language α} (h : L.IsStarFree) :
    ∃ (n : ℕ), ∀ (w : List α), (List.replicate (n + 1) w).flatten ∈ L ↔ (List.replicate n w).flatten ∈ L

    A star-free language cannot tell n + 1 copies of a word from n copies, for some n.

    source
    theorem Language.not_isStarFree_setOf_even_length {α : Type u_1} [Nonempty α] :
    ¬IsStarFree {w : List α | Even w.length}

    The words of even length do not form a star-free language.

    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 homomorphisms of free monoids.

    source
    theorem Language.IsStarFree.preimage_filter {α : Type u_1} {L : Language α} (h : L.IsStarFree) (p : α → Bool) :
    IsStarFree {w : List α | List.filter p w ∈ L}

    Star-free languages are closed under preimage by erasure, the instance of IsStarFree.comap for FreeMonoid.filter p, which erases the letters failing p.

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

    The full language is star-free.

    source
    theorem Language.IsStarFree.iInter {α : Type u_1} {ι : Type u_2} [Finite ι] {f : ι → Set (List α)} (h : ∀ (i : ι), IsStarFree (f i)) :
    IsStarFree (⋂ (i : ι), f i)

    Star-free languages are closed under finitely-indexed intersections.