The syntactic semigroup of a language

The syntactic semigroup of a language L is the quotient of the free semigroup, whose elements are the nonempty words, by the syntactic congruence of L restricted to those words. It embeds in the syntactic monoid, which adds to it at most the class of the empty word.

The definite, reverse definite and locally trivial pseudovarieties consist of semigroups, and their languages are read off the syntactic semigroup. A monoid satisfying the defining condition of any of the three is trivial, because the condition applies to the idempotent 1.

Main definitions

• Language.syntacticSemigroupCon: the syntactic congruence on FreeSemigroup α.
• Language.SyntacticSemigroup: the quotient semigroup.
• Language.toSyntacticSemigroup: the projection, as a MulHom.
• Language.RecognizesSemigroup: recognition of a language by a homomorphism to a semigroup.

Main results

• Language.syntacticSemigroupToMonoid_injective: the syntactic semigroup embeds in the syntactic monoid.
• Language.isRegular_iff_finite_syntacticSemigroup: a language is regular exactly when its syntactic semigroup is finite.
• Language.recognizesSemigroup_iff_ker_le: a homomorphism recognizes L exactly when its kernel refines the syntactic congruence.
• Language.syntacticSemigroupCon_insert_nil: adjoining the empty word leaves the syntactic semigroup unchanged.

Implementation notes

A homomorphism η out of the free semigroup recognizes L when its extension FreeMonoid.mapWithOne η to the free monoid does, so that the kernel characterization follows from the one for monoids. Language.recognizesSemigroup_iff restates the condition on nonempty words.

References

• [Eil76]
• [Pin]

The syntactic congruence and semigroup

def Language.syntacticSemigroupCon {α : Type u_1} (L : Language α) : Con (FreeSemigroup α)

The syntactic congruence of L identifies two nonempty words when no two-sided context distinguishes them as L-members.

Equations

• L.syntacticSemigroupCon = Con.comap ⇑FreeSemigroup.toFreeMonoid ⋯ L.syntacticCon

@[reducible, inline]

abbrev Language.SyntacticSemigroup {α : Type u_1} (L : Language α) : Type u_1

The syntactic semigroup of L is the quotient of FreeSemigroup α by the syntactic congruence.

Equations

• L.SyntacticSemigroup = L.syntacticSemigroupCon.Quotient

def Language.toSyntacticSemigroup {α : Type u_1} (L : Language α) : FreeSemigroup α →ₙ* L.SyntacticSemigroup

The syntactic morphism of L projects FreeSemigroup α onto the syntactic semigroup.

Equations

• L.toSyntacticSemigroup = L.syntacticSemigroupCon.mkMulHom

theorem Language.toSyntacticSemigroup_eq_iff {α : Type u_1} {L : Language α} {u v : FreeSemigroup α} : L.toSyntacticSemigroup u = L.toSyntacticSemigroup v ↔ L.syntacticSemigroupCon u v

theorem Language.toSyntacticSemigroup_surjective {α : Type u_1} (L : Language α) : Function.Surjective ⇑L.toSyntacticSemigroup

theorem Language.ker_toSyntacticSemigroup {α : Type u_1} (L : Language α) : Con.ker L.toSyntacticSemigroup = L.syntacticSemigroupCon

Relation to the syntactic monoid

def Language.syntacticSemigroupToMonoid {α : Type u_1} (L : Language α) : L.SyntacticSemigroup →ₙ* L.SyntacticMonoid

The embedding of the syntactic semigroup into the syntactic monoid sends the class of a nonempty word to its class in the monoid.

Equations

• L.syntacticSemigroupToMonoid = L.syntacticSemigroupCon.liftMulHom ((↑L.toSyntacticMonoid).comp FreeSemigroup.toFreeMonoid) ⋯

@[simp]

theorem Language.syntacticSemigroupToMonoid_apply {α : Type u_1} (L : Language α) (u : FreeSemigroup α) : L.syntacticSemigroupToMonoid (L.toSyntacticSemigroup u) = L.toSyntacticMonoid (FreeSemigroup.toFreeMonoid u)

theorem Language.syntacticSemigroupToMonoid_mk {α : Type u_1} (L : Language α) (a : α) (l : List α) : L.syntacticSemigroupToMonoid (L.toSyntacticSemigroup { head := a, tail := l }) = L.syntacticClass (a :: l)

theorem Language.syntacticSemigroupToMonoid_injective {α : Type u_1} (L : Language α) : Function.Injective ⇑L.syntacticSemigroupToMonoid

instance Language.instFiniteSyntacticSemigroupOfSyntacticMonoid {α : Type u_1} {L : Language α} [Finite L.SyntacticMonoid] : Finite L.SyntacticSemigroup

theorem Language.eq_one_or_mem_range_syntacticSemigroupToMonoid {α : Type u_1} (L : Language α) (s : L.SyntacticMonoid) : s = 1 ∨ s ∈ Set.range ⇑L.syntacticSemigroupToMonoid

Every element of the syntactic monoid is the class of the empty word or the image of an element of the syntactic semigroup.

theorem Language.finite_syntacticMonoid_of_finite_syntacticSemigroup {α : Type u_1} (L : Language α) [Finite L.SyntacticSemigroup] : Finite L.SyntacticMonoid

Myhill–Nerode

theorem Language.IsRegular.finite_syntacticSemigroup {α : Type u_1} {L : Language α} (h : L.IsRegular) : Finite L.SyntacticSemigroup

theorem Language.IsRegular.of_finite_syntacticSemigroup {α : Type u_1} {L : Language α} (h : Finite L.SyntacticSemigroup) : L.IsRegular

theorem Language.isRegular_iff_finite_syntacticSemigroup {α : Type u_1} {L : Language α} : L.IsRegular ↔ Finite L.SyntacticSemigroup

A language is regular exactly when its syntactic semigroup is finite.

Boolean combinations

theorem Language.syntacticSemigroupCon_compl {α : Type u_1} {L : Language α} : Lᶜ.syntacticSemigroupCon = L.syntacticSemigroupCon

theorem Language.inf_syntacticSemigroupCon_le_syntacticSemigroupCon_inf {α : Type u_1} {L L' : Language α} : L.syntacticSemigroupCon ⊓ L'.syntacticSemigroupCon ≤ (L ⊓ L').syntacticSemigroupCon

Quotients

theorem Language.syntacticSemigroupCon_le_leftQuotient {α : Type u_1} (L : Language α) (u : List α) : L.syntacticSemigroupCon ≤ (L.leftQuotient u).syntacticSemigroupCon

theorem Language.syntacticSemigroupCon_le_rightQuotient {α : Type u_1} (L : Language α) (u : List α) : L.syntacticSemigroupCon ≤ (L.rightQuotient u).syntacticSemigroupCon

theorem Language.syntacticSemigroupCon_congr {α : Type u_1} {L L' : Language α} (h : ∀ (w : List α), w ≠ [] → (w ∈ L ↔ w ∈ L')) : L.syntacticSemigroupCon = L'.syntacticSemigroupCon

The syntactic congruence on nonempty words depends on L only through its nonempty words.

theorem Language.syntacticSemigroupCon_insert_nil {α : Type u_1} {L : Language α} : (insert [] L).syntacticSemigroupCon = L.syntacticSemigroupCon

Adjoining the empty word leaves the syntactic congruence unchanged, since the congruence quantifies only over nonempty words.

Recognition by a semigroup

def Language.RecognizesSemigroup {α : Type u_1} {T : Type u_2} [Semigroup T] (η : FreeSemigroup α →ₙ* T) (L : Language α) : Prop

η recognizes L when its unitization FreeMonoid.mapWithOne η recognizes L. Equivalently, membership of a nonempty word in L is decided by its η-image (recognizesSemigroup_iff).

Equations

• Language.RecognizesSemigroup η L = Language.Recognizes (FreeMonoid.mapWithOne η) L

theorem Language.recognizesSemigroup_iff {α : Type u_1} {L : Language α} {T : Type u_2} [Semigroup T] {η : FreeSemigroup α →ₙ* T} : RecognizesSemigroup η L ↔ ∃ (P : Set T), ∀ (w : FreeSemigroup α), FreeMonoid.toList (FreeSemigroup.toFreeMonoid w) ∈ L ↔ η w ∈ P

theorem Language.RecognizesSemigroup.comap {α : Type u_1} {L : Language α} {T : Type u_2} [Semigroup T] {η : FreeSemigroup α →ₙ* T} {β : Type u_3} (hrec : RecognizesSemigroup η L) (ψ : FreeSemigroup β →ₙ* FreeSemigroup α) : RecognizesSemigroup (η.comp ψ) {w : List β | ∃ (u : FreeSemigroup β), FreeMonoid.toList (FreeSemigroup.toFreeMonoid u) = w ∧ FreeMonoid.toList (FreeSemigroup.toFreeMonoid (ψ u)) ∈ L}

If η recognizes L, then η.comp ψ recognizes the inverse image of L under ψ.

theorem Language.ker_le_syntacticSemigroupCon_of_recognizes {α : Type u_1} {L : Language α} {T : Type u_2} [Semigroup T] {η : FreeSemigroup α →ₙ* T} (hrec : RecognizesSemigroup η L) : Con.ker η ≤ L.syntacticSemigroupCon

theorem Language.recognizesSemigroup_of_ker_le {α : Type u_1} {L : Language α} {T : Type u_2} [Semigroup T] {η : FreeSemigroup α →ₙ* T} (h : Con.ker η ≤ L.syntacticSemigroupCon) : RecognizesSemigroup η L

theorem Language.recognizesSemigroup_iff_ker_le {α : Type u_1} {L : Language α} {T : Type u_2} [Semigroup T] {η : FreeSemigroup α →ₙ* T} : RecognizesSemigroup η L ↔ Con.ker η ≤ L.syntacticSemigroupCon

theorem Language.recognizesSemigroup_toSyntacticSemigroup {α : Type u_1} (L : Language α) : RecognizesSemigroup L.toSyntacticSemigroup L