Documentation

Linglib.Core.Computability.Variety.SemigroupLangs

The language-side operator of a semigroup pseudovariety #

For a pseudovariety V of finite semigroups, V.langs collects the regular languages whose syntactic semigroup lies in V. This is the +-variety half of the Eilenberg correspondence ([Eil76] Ch. VII), the counterpart of Monoid.Pseudovariety.langs.

The semigroup half is what the classes D, K, LI require: they are not monoid varieties, so they have no image under the monoid-side operator.

Main definitions #

Main results #

Together these are the four conditions of [Eil76] VII, Theorem 3.2.

source
def Semigroup.Pseudovariety.langs (V : Pseudovariety) {α : Type u} (L : Language α) :
Prop

The languages over α whose (necessarily finite) syntactic semigroup lies in V — the +-variety side of the Eilenberg correspondence.

Equations
Instances For
    source
    theorem Semigroup.Pseudovariety.langs_compl (V : Pseudovariety) {α : Type u} {L : Language α} (h : V.langs L) :
    V.langs Lᶜ

    Closure under complement — immediate from complement-invariance of the syntactic congruence (Language.syntacticSemigroupCon_compl).

    Closure under quotients #

    Eilenberg's axiom VII.3.3, on the + side. The argument is the monoid one: a quotient's syntactic congruence is coarser, so its syntactic semigroup is a quotient of the original's.

    source
    theorem Semigroup.Pseudovariety.langs_leftQuotient {V : Pseudovariety} {α : Type u} {L : Language α} (h : V.langs L) (u : List α) :
    V.langs (L.leftQuotient u)

    Closure under left quotient — Eilenberg's axiom VII.3.3.

    source
    theorem Semigroup.Pseudovariety.langs_rightQuotient {V : Pseudovariety} {α : Type u} {L : Language α} (h : V.langs L) (u : List α) :
    V.langs (L.rightQuotient u)

    Closure under right quotient — Eilenberg's axiom VII.3.3.

    source
    theorem Semigroup.Pseudovariety.langs_inf (V : Pseudovariety) {α : Type u} {L M : Language α} (hL : V.langs L) (hM : V.langs M) :
    V.langs (L ⊓ M)

    Closure under intersection — the syntactic semigroup of L ⊓ M is a quotient of a subsemigroup of L.SyntacticSemigroup × M.SyntacticSemigroup, which is in V by prod/sub/quot.

    source
    theorem Semigroup.Pseudovariety.langs_sup (V : Pseudovariety) {α : Type u} {L M : Language α} (hL : V.langs L) (hM : V.langs M) :
    V.langs (L ⊔ M)

    Closure under union — by De Morgan, L ⊔ M = (Lᶜ ⊓ Mᶜ)ᶜ.

    source
    theorem Semigroup.Pseudovariety.langs_of_recognizes (V : Pseudovariety) {α : Type u} {L : Language α} {T : Type u} [Semigroup T] [Finite T] (hT : V.mem T) (η : FreeSemigroup α →ₙ* T) (P : Set T) (hL : ∀ (w : FreeSemigroup α), FreeMonoid.toList (FreeSemigroup.toFreeMonoid w) ∈ L ↔ η w ∈ P) :
    V.langs L

    Engine. A language recognized by a finite semigroup in V lies in V.langs: the syntactic semigroup is a quotient of a subsemigroup of the recognizer.

    source
    theorem Semigroup.Pseudovariety.langs_univ (V : Pseudovariety) {α : Type u} :
    V.langs ⊤

    The full language — recognized by the trivial semigroup, which is in every pseudovariety.

    source
    theorem Semigroup.Pseudovariety.langs_bot (V : Pseudovariety) {α : Type u} :
    V.langs ⊥

    The empty language — ⊥ = ⊤ᶜ.

    source
    theorem Semigroup.Pseudovariety.langs_comap (V : Pseudovariety) {α β : Type u} {Lb : Language β} (h : V.langs Lb) (φ : FreeSemigroup α →ₙ* FreeSemigroup β) :
    V.langs {w : List α | ∃ (u : FreeSemigroup α), FreeMonoid.toList (FreeSemigroup.toFreeMonoid u) = w ∧ FreeMonoid.toList (FreeSemigroup.toFreeMonoid (φ u)) ∈ Lb}

    Closure under inverse homomorphism — Eilenberg's fourth axiom, on the + side. The morphism is between free semigroups: [Eil76] VII, Exercise 3.7 shows that the *-variety form of this axiom decomposes into a non-erasing morphism condition, and a free semigroup has no erasing morphisms.