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, i.e. L is a union of φ-fibres
• Language.rightQuotient: the right-quotient dual of Language.leftQuotient

Main results

• Language.recognizes_iff_ker_le: the syntactic congruence is the coarsest congruence saturating L — a hom recognizes L exactly when its kernel refines it
• Language.syntacticCon_eq_ker_transitionHom: the intrinsic congruence is the kernel of the transition action of L.toDFA
• Language.isRegular_iff_finite_syntacticMonoid: the Myhill–Nerode theorem in monoid form

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.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)

The syntactic congruence refines the Nerode equivalence uniformly: u and v are related 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_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.syntacticMonoid_isSubquotient {α : Type u_1} {L : Language α} {M : Type u_2} [Monoid M] {φ : FreeMonoid α →* M} (hrec : Recognizes φ L) : Monoid.IsSubquotient L.SyntacticMonoid M

Minimality of the syntactic monoid: it divides every monoid recognising L — 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.

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

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