The syntactic monoid of a language

The syntactic monoid of a language L : Language α is the quotient of the free monoid FreeMonoid α by the syntactic congruence: two words are identified when no two-sided context distinguishes them as L-members, ∀ x y, x ++ u ++ y ∈ L ↔ x ++ v ++ y ∈ L.

The syntactic congruence is defined directly as this two-sided context equivalence, and identified with the kernel of the minimal DFA's transition action (the transition monoid of L.toDFA, see Linglib.Core.Computability.TransitionMonoid) via Language.syntacticCon_eq_ker_transitionHom. This is the two-sided refinement of Mathlib.Computability.MyhillNerode, which builds the one-sided right-Nerode quotient (Language.leftQuotient) and proves regularity ↔ finitely many left quotients. It carries a monoid structure rather than just a set of states, and its Myhill–Nerode theorem reads L.IsRegular ↔ Finite L.syntacticMonoid.

Main definitions

• Language.syntacticCon L : Con (FreeMonoid α): the syntactic congruence (two-sided context equivalence).
• Language.syntacticMonoid L: the quotient monoid (syntacticCon L).Quotient.
• Language.toSyntacticMonoid L: the projection FreeMonoid α →* L.syntacticMonoid.
• Language.syntacticClass L w: the syntactic class of a word w : List α.
• Language.Recognizes φ L: φ recognizes L, i.e. L is a union of φ-fibres.

Main results

• Language.syntacticClass_eq_iff: two words share a syntactic class iff no two-sided context distinguishes them, ∀ x y, x ++ u ++ y ∈ L ↔ x ++ v ++ y ∈ L.
• Language.syntacticCon_eq_ker_transitionHom: the intrinsic congruence is the kernel of the transition action of L.toDFA.
• Language.ker_le_syntacticCon_of_recognizes: the syntactic congruence is the coarsest congruence recognizing L, so every recognizing hom factors through toSyntacticMonoid via Con.lift.
• Language.isRegular_iff_finite_syntacticMonoid: the Myhill–Nerode theorem in monoid form.

The syntactic congruence and monoid

def Language.syntacticCon {α : Type u_1} (L : Language α) : Con (FreeMonoid α)

The syntactic congruence of L: two words are congruent when no two-sided context distinguishes them as L-members.

Equations

• L.syntacticCon = { r := fun (u v : FreeMonoid α) => ∀ (x y : List α), x ++ FreeMonoid.toList u ++ y ∈ L ↔ x ++ FreeMonoid.toList v ++ y ∈ L, iseqv := ⋯, mul' := ⋯ }

theorem Language.syntacticCon_iff {α : Type u_1} (L : Language α) {u v : FreeMonoid α} : L.syntacticCon u v ↔ ∀ (x y : List α), x ++ FreeMonoid.toList u ++ y ∈ L ↔ x ++ FreeMonoid.toList v ++ y ∈ L

The syntactic congruence is two-sided context equivalence — by definition.

theorem Language.mem_iff_of_syntacticCon {α : Type u_1} {L : Language α} {u v : FreeMonoid α} (h : L.syntacticCon u v) : u ∈ L ↔ v ∈ L

Words congruent under the syntactic congruence agree on membership of L: L is saturated by syntacticCon L (take the empty two-sided context).

def Language.syntacticMonoid {α : Type u_1} (L : Language α) : Type u_1

The syntactic monoid of L: the quotient of FreeMonoid α by the syntactic congruence.

Equations

• L.syntacticMonoid = L.syntacticCon.Quotient

@[implicit_reducible]

instance Language.instMonoidSyntacticMonoid {α : Type u_1} (L : Language α) : Monoid L.syntacticMonoid

Equations

• One or more equations did not get rendered due to their size.

def Language.toSyntacticMonoid {α : Type u_1} (L : Language α) : FreeMonoid α →* L.syntacticMonoid

The canonical projection sending each word to its syntactic class; the underlying Con.mk'.

Equations

• L.toSyntacticMonoid = L.syntacticCon.mk'

theorem Language.toSyntacticMonoid_eq_iff {α : Type u_1} (L : Language α) {u v : FreeMonoid α} : L.toSyntacticMonoid u = L.toSyntacticMonoid v ↔ L.syntacticCon u v

The syntactic projection identifies two words iff they are syntactically congruent.

The syntactic class of a word

def Language.syntacticClass {α : Type u_1} (L : Language α) (w : List α) : L.syntacticMonoid

The syntactic class of a word w: its image in the syntactic monoid (the literature's η(w), applied to a List α rather than a bundled FreeMonoid α).

Equations

• L.syntacticClass w = L.toSyntacticMonoid (FreeMonoid.ofList w)

@[simp]

theorem Language.syntacticClass_nil {α : Type u_1} (L : Language α) : L.syntacticClass [] = 1

@[simp]

theorem Language.syntacticClass_append {α : Type u_1} (L : Language α) (u v : List α) : L.syntacticClass (u ++ v) = L.syntacticClass u * L.syntacticClass v

theorem Language.syntacticClass_surjective {α : Type u_1} (L : Language α) : Function.Surjective L.syntacticClass

theorem Language.syntacticClass_eq_iff {α : Type u_1} {L : Language α} {u v : List α} : L.syntacticClass u = L.syntacticClass v ↔ ∀ (x y : List α), x ++ u ++ y ∈ L ↔ x ++ v ++ y ∈ L

Word-level form of syntacticCon_iff: two words share a syntactic class iff no two-sided context distinguishes them as L-members.

theorem Language.mem_iff_of_syntacticClass_eq {α : Type u_1} {L : Language α} {u v : List α} (h : L.syntacticClass u = L.syntacticClass v) : u ∈ L ↔ v ∈ L

L is saturated by syntactic class: equal class implies equal membership.

theorem Language.syntacticClass_reverse_eq_iff {α : Type u_1} {L : Language α} {u v : List α} : L.reverse.syntacticClass u = L.reverse.syntacticClass v ↔ L.syntacticClass u.reverse = L.syntacticClass v.reverse

Reverse duality: a syntactic-class equality in L.reverse is the same as the reversed-word equality in L. The syntactic monoid of L.reverse is L's, opposite.

Universal property

def Language.Recognizes {α : Type u_1} {M : Type u_2} [Monoid M] (φ : FreeMonoid α →* M) (L : Language α) : Prop

φ recognizes L when L is a union of φ-fibres, i.e. L = φ ⁻¹' S for some S ⊆ M.

Equations

• Language.Recognizes φ L = ∃ (S : Set M), L = ⇑φ ⁻¹' S

theorem Language.ker_le_syntacticCon_of_recognizes {α : Type u_1} {L : Language α} {M : Type u_2} [Monoid M] {φ : FreeMonoid α →* M} (hrec : Recognizes φ L) : Con.ker φ ≤ L.syntacticCon

An L-recognizing hom's kernel lies below syntacticCon L, the coarsest such congruence.

theorem Language.recognizes_of_ker_le_syntacticCon {α : Type u_1} {L : Language α} {M : Type u_2} [Monoid M] {φ : FreeMonoid α →* M} (h : Con.ker φ ≤ L.syntacticCon) : Recognizes φ L

Conversely, any hom whose kernel refines syntacticCon L recognizes L (witness S = φ '' L).

theorem Language.recognizes_iff_ker_le_syntacticCon {α : Type u_1} {L : Language α} {M : Type u_2} [Monoid M] {φ : FreeMonoid α →* M} : Recognizes φ L ↔ Con.ker φ ≤ L.syntacticCon

Universal property of the syntactic monoid: a hom recognizes L exactly when its kernel refines the syntactic congruence — syntacticCon L is the coarsest L-recognizing congruence, so every recognizer factors through toSyntacticMonoid.

theorem Language.recognizes_toSyntacticMonoid {α : Type u_1} {L : Language α} : Recognizes L.toSyntacticMonoid L

The syntactic morphism is itself an L-recognizer (the canonical one).

Connection to the minimal DFA

theorem Language.evalFrom_toDFA {α : Type u_1} {L : Language α} (s : ↑(Set.range L.leftQuotient)) (w : List α) : ↑(L.toDFA.evalFrom s w) = (↑s).leftQuotient w

Evaluating the minimal DFA L.toDFA from a quotient state s along w lands on the left quotient of s by w.

theorem Language.syntacticCon_eq_ker_transitionHom {α : Type u_1} {L : Language α} : L.syntacticCon = Con.ker L.toDFA.transitionHom

The intrinsic syntactic congruence is the kernel of the minimal DFA's transition action — the two-sided context definition agrees with the transition-monoid quotient.

Regularity implies a finite syntactic monoid

theorem Language.finite_syntacticMonoid {α : Type u_1} {L : Language α} (h : L.IsRegular) : Finite L.syntacticMonoid

A regular language has a finite syntactic monoid (forward Myhill–Nerode).

A finite syntactic monoid implies regularity

theorem Language.isRegular_of_finite_syntacticMonoid {α : Type u_1} {L : Language α} (h : Finite L.syntacticMonoid) : L.IsRegular

A language with finite syntactic monoid is regular (reverse Myhill–Nerode). The left-quotient map factors through the syntactic monoid, so a finite quotient forces finitely many left quotients.

theorem Language.isRegular_iff_finite_syntacticMonoid {α : Type u_1} {L : Language α} : L.IsRegular ↔ Finite L.syntacticMonoid

Myhill–Nerode (syntactic-monoid form): L is regular iff L.syntacticMonoid is finite.

Complement- and intersection-invariance

Generic syntactic-monoid facts about boolean combinations, used by any class defined through the syntactic monoid (e.g. Language.IsStarFree, and Monoid.Pseudovariety.langs in general).

theorem Language.syntacticCon_compl {α : Type u_1} (L : Language α) : Lᶜ.syntacticCon = L.syntacticCon

The syntactic congruence is complement-invariant: a two-sided context distinguishes u from v for L exactly when it does for Lᶜ.

theorem Language.syntacticMonoid_compl {α : Type u_1} (L : Language α) : Lᶜ.syntacticMonoid = L.syntacticMonoid

The syntactic monoid is complement-invariant.

theorem Language.inf_syntacticCon_le_syntacticCon_inf {α : Type u_1} (L M : Language α) : L.syntacticCon ⊓ M.syntacticCon ≤ (L ⊓ M).syntacticCon

The meet of the two syntactic congruences refines that of the intersection: if no L-context and no M-context distinguishes u from v, then no (L ⊓ M)-context does either.

theorem Language.ker_prod_toSyntacticMonoid {α : Type u_1} (L M : Language α) : Con.ker (L.toSyntacticMonoid.prod M.toSyntacticMonoid) = L.syntacticCon ⊓ M.syntacticCon

The kernel of the pairing of the two syntactic morphisms is exactly the meet of the two syntactic congruences (a word's class in the product is the pair of its classes).