Regularity from a finite invariant #
This file adds two consequences of the Myhill–Nerode theorem for languages. A language is regular when membership is decided by an invariant of the word that takes finitely many values and is preserved by appending on the right, and a regular language has only finitely many pairwise distinguishable words.
Main results #
Language.IsRegular.of_factorsThrough: a language whose membership factors through a map with finite range, compatible with appending on the right, is regular.Language.IsRegular.finite_of_injective_leftQuotient: a family of words with pairwise distinct left quotients by a regular language is finite.
References #
theorem
Language.IsRegular.of_factorsThrough
{α : Type u_1}
{β : Type u_2}
{L : Language α}
{g : List α → β}
(hL : Function.FactorsThrough (fun (x : List α) => x ∈ L) g)
(hg : ∀ ⦃u v : List α⦄ (x : List α), g u = g v → g (u ++ x) = g (v ++ x))
(hfin : (Set.range g).Finite)
:
L.IsRegular
A language is regular when membership factors through a map g with finite range such that
words with equal g-values still have equal g-values after appending the same word.
theorem
Language.IsRegular.finite_of_injective_leftQuotient
{α : Type u_1}
{L : Language α}
(h : L.IsRegular)
{ι : Type u_3}
{f : ι → List α}
(hf : Function.Injective (L.leftQuotient ∘ f))
:
Finite ι
A family of words with pairwise distinct left quotients by a regular language is finite.