Myhill–Nerode theorem

This file proves the Myhill–Nerode theorem using left quotients.

Given a language L and a word x, the left quotient of L by x is the set of suffixes y such that x ++ y is in L. The Myhill–Nerode theorem shows that each left quotient, in fact, corresponds to the state of an automaton that matches L, and that L is regular if and only if there are finitely many such states.

References

• https://en.wikipedia.org/wiki/Syntactic_monoid#Myhill%E2%80%93Nerode_theorem

def Language.leftQuotient {α : Type u} (L : Language α) (x : List α) : Language α

The left quotient of x is the set of suffixes y such that x ++ y is in L.

@[simp]

theorem Language.leftQuotient_nil {α : Type u} (L : Language α) : L.leftQuotient [] = L

theorem Language.leftQuotient_append {α : Type u} (L : Language α) (x y : List α) : L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y

@[simp]

theorem Language.mem_leftQuotient {α : Type u} {L : Language α} (x y : List α) : y ∈ L.leftQuotient x ↔ x ++ y ∈ L

theorem Language.leftQuotient_accepts_apply {α : Type u} {σ : Type v} (M : DFA α σ) (x : List α) : M.accepts.leftQuotient x = M.acceptsFrom (M.eval x)

theorem Language.leftQuotient_accepts {α : Type u} {σ : Type v} (M : DFA α σ) : M.accepts.leftQuotient = M.acceptsFrom ∘ M.eval

theorem Language.IsRegular.finite_range_leftQuotient {α : Type u} {L : Language α} (h : L.IsRegular) : (Set.range L.leftQuotient).Finite

def Language.toDFA {α : Type u} (L : Language α) : DFA α ↑(Set.range L.leftQuotient)

The left quotients of a language are the states of an automaton that accepts the language.

@[simp]

theorem Language.mem_accept_toDFA {α : Type u} {L : Language α} (s : ↑(Set.range L.leftQuotient)) : s ∈ L.toDFA.accept ↔ [] ∈ ↑s

@[simp]

theorem Language.step_toDFA {α : Type u} {L : Language α} (s : ↑(Set.range L.leftQuotient)) (a : α) : ↑(L.toDFA.step s a) = (↑s).leftQuotient [a]

@[simp]

theorem Language.start_toDFA {α : Type u} (L : Language α) : ↑L.toDFA.start = L

@[simp]

theorem Language.accepts_toDFA {α : Type u} (L : Language α) : L.toDFA.accepts = L

theorem Language.IsRegular.of_finite_range_leftQuotient {α : Type u} {L : Language α} (h : (Set.range L.leftQuotient).Finite) : L.IsRegular

theorem Language.isRegular_iff_finite_range_leftQuotient {α : Type u} {L : Language α} : L.IsRegular ↔ (Set.range L.leftQuotient).Finite

Myhill–Nerode theorem. A language is regular if and only if the set of left quotients is finite.