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.

It is the coarsest congruence saturating L, so the syntactic morphism factors through every recognizing homomorphism, and the quotient is finite exactly when L is regular. This is the two-sided refinement of the one-sided right-Nerode quotient Language.leftQuotient, carrying a monoid structure rather than a bare set of states.

Main definitions

• Language.syntacticCon: the syntactic congruence, two-sided context equivalence.
• Language.SyntacticMonoid: the quotient monoid (syntacticCon L).Quotient.
• Language.toSyntacticMonoid: the projection FreeMonoid α →* L.SyntacticMonoid.
• Language.syntacticClass: the syntactic class of a word.
• Language.Recognizes: φ recognizes L when L is a union of φ-fibres.
• Language.rightQuotient: the right-quotient dual of Language.leftQuotient.

Main results

• Language.recognizes_iff_ker_le: a homomorphism recognizes L exactly when its kernel refines the syntactic congruence.
• Language.syntacticMonoidEquivTransitionMonoid: the syntactic monoid is the transition monoid of the minimal DFA L.toDFA.
• Language.isRegular_iff_finite_syntacticMonoid: a language is regular exactly when its syntactic monoid is finite.

References

• [Pin]

Syntactic equivalence

def Language.SyntacticEquiv {α : Type u_1} (L : Language α) (u v : List α) : Prop

Two words are syntactically equivalent for L when no two-sided context distinguishes them as L-members.

Equations

• L.SyntacticEquiv u v = ∀ (x y : List α), x ++ u ++ y ∈ L ↔ x ++ v ++ y ∈ L

theorem Language.SyntacticEquiv.refl {α : Type u_1} {L : Language α} (u : List α) : L.SyntacticEquiv u u

theorem Language.SyntacticEquiv.symm {α : Type u_1} {L : Language α} {u v : List α} (h : L.SyntacticEquiv u v) : L.SyntacticEquiv v u

theorem Language.SyntacticEquiv.trans {α : Type u_1} {L : Language α} {u v w : List α} (h : L.SyntacticEquiv u v) (h' : L.SyntacticEquiv v w) : L.SyntacticEquiv u w

theorem Language.SyntacticEquiv.append {α : Type u_1} {L : Language α} {u u' v v' : List α} (h : L.SyntacticEquiv u u') (h' : L.SyntacticEquiv v v') : L.SyntacticEquiv (u ++ v) (u' ++ v')

theorem Language.SyntacticEquiv.mem_iff {α : Type u_1} {L : Language α} {u v : List α} (h : L.SyntacticEquiv u v) : u ∈ L ↔ v ∈ L

theorem Language.SyntacticEquiv.leftQuotient_eq {α : Type u_1} {L : Language α} {u v : List α} (h : L.SyntacticEquiv u v) : L.leftQuotient u = L.leftQuotient v

theorem Language.SyntacticEquiv.compl_iff {α : Type u_1} {L : Language α} {u v : List α} : Lᶜ.SyntacticEquiv u v ↔ L.SyntacticEquiv u v

theorem Language.SyntacticEquiv.reverse_iff {α : Type u_1} {L : Language α} {u v : List α} : L.reverse.SyntacticEquiv u v ↔ L.SyntacticEquiv u.reverse v.reverse

The syntactic congruence and monoid

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

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

Equations

• L.syntacticCon = { r := fun (u v : FreeMonoid α) => L.SyntacticEquiv (FreeMonoid.toList u) (FreeMonoid.toList v), iseqv := ⋯, mul' := ⋯ }

theorem Language.syntacticCon_iff {α : Type u_1} {L : Language α} {u v : FreeMonoid α} : L.syntacticCon u v ↔ L.SyntacticEquiv (FreeMonoid.toList u) (FreeMonoid.toList v)

theorem Language.syntacticCon_iff_leftQuotient {α : Type u_1} {L : Language α} {u v : FreeMonoid α} : L.syntacticCon u v ↔ ∀ (x : List α), L.leftQuotient (x ++ FreeMonoid.toList u) = L.leftQuotient (x ++ FreeMonoid.toList v)

Two words are syntactically congruent exactly when their left quotients agree in every left context.

@[reducible, inline]

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

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

Equations

• L.SyntacticMonoid = L.syntacticCon.Quotient

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

The syntactic morphism of L projects FreeMonoid α onto the syntactic monoid.

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

theorem Language.ker_toSyntacticMonoid {α : Type u_1} (L : Language α) : Con.ker L.toSyntacticMonoid = L.syntacticCon

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 is its image in the syntactic monoid.

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_flatten {α : Type u_1} (L : Language α) (ws : List (List α)) : L.syntacticClass ws.flatten = (List.map L.syntacticClass ws).prod

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 ↔ L.SyntacticEquiv u v

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

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

Universal property

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

φ recognizes L when L is the FreeMonoid.ofList-pullback of a union of φ-fibres.

Equations

• Language.Recognizes φ L = ∃ (S : Set M), L = ⇑FreeMonoid.ofList ⁻¹' ⇑φ ⁻¹' 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

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

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

theorem Language.Recognizes.comap {α : Type u_1} {L : Language α} {M : Type u_2} [Monoid M] {φ : FreeMonoid α →* M} {β : Type u_3} (hrec : Recognizes φ L) (ψ : FreeMonoid β →* FreeMonoid α) : Recognizes (φ.comp ψ) {w : List β | ψ (FreeMonoid.ofList w) ∈ L}

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

theorem Language.Recognizes.syntacticMonoid_isSubquotient {α : Type u_1} {L : Language α} {M : Type u_2} [Monoid M] {φ : FreeMonoid α →* M} (hrec : Recognizes φ L) : Monoid.IsSubquotient L.SyntacticMonoid M

The syntactic monoid divides every monoid recognizing L, since the image of φ surjects onto the syntactic quotient through the first isomorphism theorem.

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

Connection to the minimal DFA

theorem Language.recognizes_transitionHom {α : Type u_1} {σ : Type u_2} (M : DFA α σ) : Recognizes M.transitionHom M.accepts

A DFA's transition action recognizes the language it accepts.

@[simp]

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

theorem Language.ker_transitionHom_toDFA_iff {α : Type u_1} {L : Language α} {u v : FreeMonoid α} : (Con.ker L.toDFA.transitionHom) u v ↔ ∀ (x : List α), L.leftQuotient (x ++ FreeMonoid.toList u) = L.leftQuotient (x ++ FreeMonoid.toList v)

The kernel of the minimal DFA's transition action has the same left-quotient characterization as the syntactic congruence.

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.

noncomputable def Language.syntacticMonoidEquivTransitionMonoid {α : Type u_1} (L : Language α) : L.SyntacticMonoid ≃* ↥L.toDFA.transitionMonoid

The syntactic monoid of L is the transition monoid of its minimal DFA.

Equations

• L.syntacticMonoidEquivTransitionMonoid = (Con.congr (MulEquiv.refl (FreeMonoid α)) ⋯).trans (Con.quotientKerEquivRange L.toDFA.transitionHom)

Myhill–Nerode

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

theorem Language.IsRegular.of_finite_syntacticMonoid {α : Type u_1} {L : Language α} (h : Finite L.SyntacticMonoid) : L.IsRegular

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

L is regular iff L.SyntacticMonoid is finite.

Boolean combinations

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

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

Quotients

def Language.rightQuotient {α : Type u_1} (L : Language α) (u : List α) : Language α

The right quotient of L by u is the set of prefixes w such that w ++ u is in L.

Equations

• L.rightQuotient u = {w : List α | w ++ u ∈ L}

@[simp]

theorem Language.mem_rightQuotient {α : Type u_1} {L : Language α} {u w : List α} : w ∈ L.rightQuotient u ↔ w ++ u ∈ L

@[simp]

theorem Language.rightQuotient_nil {α : Type u_1} (L : Language α) : L.rightQuotient [] = L

theorem Language.rightQuotient_append {α : Type u_1} (L : Language α) (u v : List α) : L.rightQuotient (u ++ v) = (L.rightQuotient v).rightQuotient u

theorem Language.rightQuotient_eq_reverse_leftQuotient {α : Type u_1} (L : Language α) (u : List α) : L.rightQuotient u = (L.reverse.leftQuotient u.reverse).reverse

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

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