Syntactic monoid

This file defines the syntactic monoid of a language l and shows that l is regular if and only if its syntactic monoid is finite.

References

[Hol82] Holcombe, W.M.L. (1982). Algebraic automata theory. Section 5.3

def Language.Congruence.toCon {α : Type} [c : Congruence α] : Con (FreeMonoid α)

Converting a (two-sided) congruence c on finite words to a congruence relation on the (multiplicative) free monoid.

Equations

• Language.Congruence.toCon = { toSetoid := c.eq, mul' := ⋯ }

@[reducible, inline]

abbrev Language.SyntacticMonoid {α : Type} (l : Language α) : Type

The syntactic monoid of a language l is the quotient of the free monoid by the Myhill congruence of l.

Equations

• l.SyntacticMonoid = Language.Congruence.toCon.Quotient

theorem Language.IsRegular.iff_finite_syntacticMonoid {α : Type} (l : Language α) : l.IsRegular ↔ Finite l.SyntacticMonoid

A language l is regular if and only if its syntactic monoid is finite.