Syntactic Monoid

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

This file is the two-sided dual of Mathlib.Computability.MyhillNerode, which constructs the right-Nerode quotient (Language.leftQuotient) and proves regularity ↔ finitely many left quotients. The syntactic monoid is a strictly more refined invariant: it carries a monoid structure (not just a setoid of states), and the bidirectional version of the Myhill–Nerode theorem is

L.IsRegular ↔ Finite L.syntacticMonoid

(Myhill 1957; see e.g. Pin's Mathematical Foundations of Automata Theory, Chapter I).

The empty word [] : FreeMonoid α becomes the identity of syntacticMonoid L. Some classical references (e.g. the Lambert (2026) phonology consumer of this file) work with the syntactic semigroup instead, omitting the empty word; the two characterisations coincide for the regularity ↔ finiteness statement, but the monoid version is mathlib-natural via Con (FreeMonoid α).

Main definitions

• Language.SyntacticEquiv L u v — the two-sided context-equivalence relation on words.
• Language.syntacticCon L : Con (FreeMonoid α) — the syntactic congruence, packaged as a multiplicative congruence on the free monoid (concatenation).
• Language.syntacticMonoid L — the quotient monoid (syntacticCon L).Quotient.
• Language.toSyntacticMonoid L : FreeMonoid α →* L.syntacticMonoid — the canonical projection ((syntacticCon L).mk').

Main results

• Language.SyntacticEquiv.leftQuotient_eq — the syntactic equivalence refines the right-Nerode equivalence (a syntactic-equivalent pair has the same left quotient). The reverse implication does not hold.
• Language.IsRegular.finite_syntacticMonoid — Myhill direction A: if L is regular then its syntactic monoid is finite. Proved via the injection [u] ↦ (Q ↦ Q.leftQuotient u) from syntacticMonoid L into the function space LQ → LQ where LQ = Set.range L.leftQuotient is finite by Language.IsRegular.finite_range_leftQuotient.

The reverse direction (finite syntactic monoid ⟹ regular) is classical and follows from the syntactic monoid acting on itself; it is left as a TODO since it needs additional substrate (a Finite-bounded DFA construction from a finite monoid action).

Implementation notes

FreeMonoid α is def-equal to List α, but Lean's typeclass elaborator does not unfold the def. The SyntacticEquiv predicate is stated on List α (so that ++ and Language.leftQuotient work without coercion gymnastics) and the Con (FreeMonoid α) upgrade reuses the Setoid via the definitional equality. Inside mul', the Mul-on-FreeMonoid operation is bridged to List.append by way of FreeMonoid.toList, which is an Equiv.refl _.

References

• Myhill (1957), Nerode (1958)
• Pin, Mathematical Foundations of Automata Theory, Chapter I.

Mathlib placement note

This file is structured to be promotable to mathlib as a sibling of Mathlib.Computability.MyhillNerode. The Language.SyntacticEquiv relation uses only ++ and Language membership; the Con packaging uses only Mathlib.GroupTheory.Congruence.Defs. The finite-syntactic-monoid theorem composes with mathlib's existing IsRegular.finite_range_leftQuotient and leftQuotient_append.

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

Two words u, v : List α are syntactically equivalent w.r.t. L iff no two-sided context (x, y) distinguishes them as L-members. The largest left- and right-concatenation-stable equivalence contained in (· ∈ L).

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 α} (h1 : L.SyntacticEquiv u v) (h2 : L.SyntacticEquiv v w) : L.SyntacticEquiv u w

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

Specialising the two-sided test to x = [] shows that the syntactic equivalence refines the right-Nerode equivalence: equivalent words have the same Language.leftQuotient.

def Language.syntacticSetoid {α : Type u_1} (L : Language α) : Setoid (FreeMonoid α)

The syntactic equivalence as a Setoid on FreeMonoid α. The underlying carrier is FreeMonoid α := List α definitionally, so SyntacticEquiv L : List α → List α → Prop reuses without coercion.

Equations

• L.syntacticSetoid = { r := L.SyntacticEquiv, iseqv := ⋯ }

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

The syntactic congruence of L: the syntactic equivalence, upgraded with the multiplicative-congruence law (closure under two-sided concatenation). The proof of mul' reassociates a two-sided context using List.append_assoc; FreeMonoid.toList (an Equiv.refl _) bridges *-on-FreeMonoid to ++-on-List.

Equations

• L.syntacticCon = { toSetoid := L.syntacticSetoid, mul' := ⋯ }

@[reducible, inline]

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

The syntactic monoid of L: the quotient of FreeMonoid α by the syntactic congruence. The abbrev is deliberate so Monoid typeclass search resolves through Con.Quotient.

Equations

• L.syntacticMonoid = L.syntacticCon.Quotient

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

The canonical monoid homomorphism from the free monoid to the syntactic monoid: each word is sent to its syntactic-equivalence class. A renamed alias of the underlying Con.mk'.

Equations

• L.toSyntacticMonoid = L.syntacticCon.mk'

@[simp]

theorem Language.toSyntacticMonoid_apply {α : Type u_1} (L : Language α) (u : FreeMonoid α) : L.toSyntacticMonoid u = ↑u

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

L is saturated by the syntactic congruence: if u ∈ L and u is syntactically equivalent to v, then v ∈ L. Direct specialisation of SyntacticEquiv to the trivial two-sided context (x = y = []). This is the core property of the syntactic congruence — it is the coarsest congruence on FreeMonoid α for which L is a union of classes.

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

A monoid hom φ : FreeMonoid α →* M recognises a language L when L is a union of φ-fibres: there is some accepting set S ⊆ M with L = φ⁻¹ S. Equivalently, membership in L depends only on the φ-image. The standard textbook definition (Pin, Mathematical Foundations of Automata Theory, Chapter I).

Equations

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

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

Universal property (kernel direction): every L-recognising hom's kernel is contained in the syntactic congruence. The syntactic congruence is the coarsest congruence on FreeMonoid α saturating L; any other saturating congruence (such as Con.ker φ for a recognising φ) is finer. Composing with mathlib's Con.lift then gives the factoring MonoidHom: (syntacticCon L).lift φ syntacticCon_ge_ker_of_recognises.

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

Myhill direction A: a regular language has a finite syntactic monoid. Proved by injecting syntacticMonoid L into the finite function space LQ → LQ, where LQ = Set.range L.leftQuotient (finite by IsRegular.finite_range_leftQuotient). The action [u] ↦ (Q ↦ Q.leftQuotient u) is well-defined on the syntactic congruence (by SyntacticEquiv.leftQuotient_eq lifted to all left contexts) and injective (because two u, v with the same action are syntactically equivalent — every two-sided test factors through some left quotient).

theorem Language.IsRegular.of_finite_syntacticMonoid {α : Type u_1} {L : Language α} [Finite L.syntacticMonoid] : L.IsRegular

Myhill direction B: a language with finite syntactic monoid is regular. Composes with mathlib's Language.IsRegular.of_finite_range_leftQuotient via the canonical factoring of L.leftQuotient through the syntactic monoid: L.leftQuotient is constant on syntactic-equivalence classes (by SyntacticEquiv.leftQuotient_eq), so it descends to a function f : L.syntacticMonoid → Language α whose range coincides with Set.range L.leftQuotient. Finiteness of L.syntacticMonoid then implies Set.Finite (Set.range f) = Set.Finite (Set.range L.leftQuotient) via Set.finite_range, closing the right-Nerode finiteness condition.

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

Myhill–Nerode (syntactic-monoid form): a language is regular iff its syntactic monoid is finite. The bidirectional bundling of IsRegular.finite_syntacticMonoid and IsRegular.of_finite_syntacticMonoid.