The syntactic semigroup of a language

The syntactic semigroup of L : Language α is the quotient of the free semigroup FreeSemigroup α — the nonempty words — by the syntactic congruence: the pullback of Language.syntacticCon along FreeSemigroup.toFreeMonoid. The two quotients are related by M_A = S_A ∪ {1} ([Eil76]), a union that is disjoint exactly when no nonempty word is equivalent to the empty one.

It is the primary invariant for varieties: D, K, LI and N are varieties of semigroups, not of monoids. Over the free monoid they collapse, since the definite condition applied to the idempotent 1 forces triviality; stating them on FreeSemigroup α is what avoids the collapse.

Main definitions

• Language.syntacticSemigroupCon: the syntactic congruence on FreeSemigroup α
• Language.SyntacticSemigroup: the quotient semigroup
• Language.toSyntacticSemigroup: the projection, as a MulHom
• Language.RecognizesSemigroup: recognition by the unitization FreeMonoid.mapWithOne

Main results

• Language.syntacticSemigroupToMonoid_injective: the syntactic semigroup embeds in the syntactic monoid
• Language.isRegular_iff_finite_syntacticSemigroup: Myhill–Nerode in semigroup form
• Language.recognizesSemigroup_iff: the pointwise characterization of recognition
• Language.recognizesSemigroup_iff_ker_le: the syntactic congruence is the coarsest one recognizing L
• Language.syntacticSemigroupCon_insert_nil: the syntactic semigroup does not see the empty word

Implementation notes

The projection is Con.mkMulHom, mathlib's MulHom-valued quotient map for a Con over a plain Mul (the monoid-valued Con.mk' would not apply). The word underlying a free-semigroup element is (FreeSemigroup.toFreeMonoid u).toList; there is no semigroup-level analogue of the preimage equation defining Language.Recognizes, since FreeSemigroup α omits the empty word, so recognition is defined through the unitization FreeMonoid.mapWithOne and characterized pointwise by recognizesSemigroup_iff.

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

theorem Language.syntacticSemigroupCon_iff {α : Type u_1} {L : Language α} {u v : FreeSemigroup α} : L.syntacticSemigroupCon u v ↔ L.syntacticCon (FreeSemigroup.toFreeMonoid u) (FreeSemigroup.toFreeMonoid v)

@[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.syntacticClassMulHom {α : Type u_1} (L : Language α) : FreeSemigroup α →ₙ* L.SyntacticMonoid

The syntactic class of the underlying nonempty word, as a homomorphism on the free semigroup.

Equations

• L.syntacticClassMulHom = (↑L.toSyntacticMonoid).comp FreeSemigroup.toFreeMonoid

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

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

The syntactic semigroup embeds into the syntactic monoid: a nonempty word is sent to its class in the monoid.

Equations

• L.syntacticSemigroupToMonoid = L.syntacticSemigroupCon.liftMulHom L.syntacticClassMulHom ⋯

@[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_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

The syntactic monoid is the syntactic semigroup with an identity adjoined: every element is the class of the empty word or the image of one of the semigroup.

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

A finite syntactic semigroup forces a finite syntactic monoid: WithOne of the semigroup covers the monoid.

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

L is regular iff L.SyntacticSemigroup 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

theorem Language.ker_prod_toSyntacticSemigroup {α : Type u_1} {L L' : Language α} : Con.ker (L.toSyntacticSemigroup.prod L'.toSyntacticSemigroup) = L.syntacticSemigroupCon ⊓ 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.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