Syntactic monoid

This file has two main results: (1) We define the syntactic monoid of a language l and show that l is regular if and only if its syntactic monoid is finite. (2) Using (1), we show that a language is regular if and only if it is the preimage of a subset of a finite monoid M under a monoid homomorphism from the free monoid on its alphabet to M

References

[Holcombe1982] 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

@[reducible, inline]

abbrev Language.homSyntacticMonoid {α : Type} (l : Language α) : FreeMonoid α →* Congruence.toCon.Quotient

The natural homomorphism from FreeMonoid α to l.SyntacticMonoid induced by the Myhill congruence of l.

Equations

• l.homSyntacticMonoid = Language.Congruence.toCon.mk'

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.

theorem Language.homSyntacticMonoid_iff_myhillCongruence {α : Type} {l : Language α} {x y : List α} : l.homSyntacticMonoid (FreeMonoid.ofList x) = l.homSyntacticMonoid (FreeMonoid.ofList y) ↔ l.MyhillCongruence.eq x y

The congruence induced by homSyntacticMonoid is exactly the Myhill congruence.

theorem Language.IsRegular.exists_finite_monoid {α : Type} {l : Language α} (h : l.IsRegular) : ∃ (M : Type) (x : Monoid M) (_ : Finite M) (f : FreeMonoid α →* M) (s : Set M), ⇑f ∘ ⇑FreeMonoid.ofList ⁻¹' s = l

Any regular language is the preimage of a subset of a finite monoid M under a monoid homomorphism from the free monoid on its alphabet to M.

@[implicit_reducible]

def Language.inducedCongr {α : Type} {M : Type u_1} [Monoid M] (f : FreeMonoid α →* M) : RightCongruence α

Given a monoid homomorphism f from FreeMonoid α to another monoid M, inducedCongr f is the language congruence induced by f.

Equations

• Language.inducedCongr f = { eq := Setoid.ker (⇑f ∘ ⇑FreeMonoid.ofList), right_cov := ⋯ }

instance Language.instFiniteQuotientListInducedCongr {α : Type} {M : Type u_1} [Monoid M] (f : FreeMonoid α →* M) [Finite M] : Finite (Quotient (inducedCongr f).eq)

theorem Language.inducedCongr_ofList {α : Type} {M : Type u_1} [Monoid M] (f : FreeMonoid α →* M) (x : List α) : ⇑f ∘ ⇑FreeMonoid.ofList ⁻¹' {(⇑f ∘ ⇑FreeMonoid.ofList) x} = RightCongruence.eqvCls ⟦x⟧

theorem Language.IsRegular.of_finite_monoid_singleton {α : Type} {M : Type u_1} [Monoid M] (f : FreeMonoid α →* M) [Finite M] (m : M) : IsRegular (⇑f ∘ ⇑FreeMonoid.ofList ⁻¹' {m})

The preimage of a singleton in a finite monoid M under a monoid homomorphism from the free monoid to M is regular.

theorem Language.IsRegular.of_finite_monoid {α : Type} {M : Type u_1} [Monoid M] (f : FreeMonoid α →* M) [Finite M] (s : Set M) : IsRegular (⇑f ∘ ⇑FreeMonoid.ofList ⁻¹' s)

The preimage of a subset of a finite monoid M under a monoid homomorphism from the free monoid to M is regular.

theorem Language.IsRegular.iff_finite_monoid {α : Type} {l : Language α} : l.IsRegular ↔ ∃ (M : Type) (x : Monoid M) (_ : Finite M) (f : FreeMonoid α →* M) (s : Set M), ⇑f ∘ ⇑FreeMonoid.ofList ⁻¹' s = l

A language is regular if and only if it is the preimage of a subset of a finite monoid M under a monoid homomorphism from the free monoid on its alphabet to M.