Myhill-Nerode Theorem

Let l be a language on an alphabet α. The Nerode congruence (referred to as c_l in comments below) of a language l is a right congruence on strings where two strings are related iff all their right extensions are either both in the language or both not in it.

The Myhill-Nerode theorem has three parts [Wik26]:

(1) l is regular iff c_l has a finite number N of equivalence classes.

(2) N is the number of states of the minimal DFA accepting l.

(3) The minimal DFA is unique up to unique isomorphism. That is, for any minimal DFA accepting l, there exists exactly an isomorphism from it to the canonical DFA whose states are the equivalence classses of c_l, whose state transitions are of the form ⟦ x ⟧ → ⟦ x ++ [a] ⟧ (where a : α and x : List α), whose initial state is ⟦ [] ⟧, and whose accepting states are { ⟦ x ⟧ | x ∈ l }.

References

• J. E. Hopcroft, R. Motwani, J. D. Ullman, Introduction to Automata Theory, Languages, and Computation
• T. Malkin, COMS W3261: Computer Science Theory, Handout 3: The Myhill-Nerode Theorem and Implications
• Wikipedia contributors, Myhill–Nerode theorem

@[implicit_reducible]

def Language.NerodeCongruence {α : Type} (l : Language α) : Cslib.RightCongruence α

The Nerode congruence (henceforth called c_l) of a language l is a right congruence on strings where two strings are related iff all their right extensions are either both in the language or both not in it.

Equations

• l.NerodeCongruence = { r := fun (x y : List α) => ∀ (z : List α), x ++ z ∈ l ↔ y ++ z ∈ l, iseqv := ⋯, right_cov := ⋯ }

@[reducible, inline]

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

The quotient type of a Nerode congruence.

Equations

• l.NerodeQuotient = Quotient l.NerodeCongruence.eq

def Language.NerodeCongruenceDA {α : Type} (l : Language α) : Cslib.Automata.DA.FinAcc l.NerodeQuotient α

The Nerode congruence of a language l gives rise to a DFA where each state corresponds to an equivalence class of the language under the Nerode congruence. Note that this is simply the DFA given rise to by the underlying right congruence with only the accept states specified here as {⟦ x ⟧ | x ∈ l}.

Equations

• l.NerodeCongruenceDA = { toDA := Cslib.RightCongruence.toDA, accept := (fun (x : List α) => ⟦x⟧) '' l }

@[simp]

theorem Language.nerodeCongruenceDA_language_eq {α : Type} (l : Language α) : Cslib.Automata.Acceptor.language l.NerodeCongruenceDA = l

The DFA constructed from the Nerode congruence c_l on l accepts l.

theorem Language.da_nerodeCongruence_iff {α : Type} {State : Type u_1} (M : Cslib.Automata.DA.FinAcc State α) (x y : List α) : (Cslib.Automata.Acceptor.language M).NerodeCongruence.eq x y ↔ ∀ (z : List α), M.mtr (M.mtr M.start x) z ∈ M.accept ↔ M.mtr (M.mtr M.start y) z ∈ M.accept

The statement (two strings are related by the Nerode congruence c_l on l iff all their right extensions are either both in the language or both not in it) is equivalent to stating that (all their right extensions are either both accepted or rejected by the DFA given rise to by c_l.)

theorem Language.IsRegular.finite_nerodeQuotient {α : Type} {l : Language α} (h : l.IsRegular) : Finite l.NerodeQuotient

If l is regular then the Nerode congruence on l has finitely many equivalence classes.

theorem Language.IsRegular.iff_finite_nerodeQuotient {α : Type} {l : Language α} : l.IsRegular ↔ Finite l.NerodeQuotient

l is regular iff the Nerode congruence on l has finitely many equivalence classes.

theorem Language.dfa_num_state_ge {α : Type} {l : Language α} {ws : Set (List α)} [Finite ↑ws] (hws : ws.Pairwise fun (x1 x2 : List α) => ¬l.NerodeCongruence.eq x1 x2) {State : Type u_1} [Finite State] {M : Cslib.Automata.DA.FinAcc State α} (hm : Cslib.Automata.Acceptor.language M = l) : Nat.card State ≥ Nat.card ↑ws

Given a set of strings all distinguishable by l (i.e., not related to each other by the Nerode congruence on l), the number of states in the DFA accepting l is at least the number of strings in the set.

theorem Language.dfa_num_state_min {α State : Type} {M : Cslib.Automata.DA.FinAcc State α} [Finite State] : Nat.card State ≥ Nat.card (Cslib.Automata.Acceptor.language M).NerodeQuotient

All DFAs accepting l must have at least as many states as the number of equivalence classes of the Nerode congruence on l.

def Cslib.Automata.DA.FinAcc.IsMinimalAutomaton {α : Type} {State : Type u_1} (M : FinAcc State α) (l : Language α) : Prop

The minimal DFA accepting l has the same number of states as the number of equivalence classes of the Nerode congruence on l.

Equations

• M.IsMinimalAutomaton l = (Cslib.Automata.Acceptor.language M = l ∧ Nat.card State = Nat.card l.NerodeQuotient)

@[implicit_reducible]

def Cslib.Automata.DA.FinAcc.StateCongruence {α : Type} {State : Type u_1} (M : FinAcc State α) : RightCongruence α

Given a DFA M, two strings are related iff they reach the same state under when run through M. The Nerode congruence is the state congruence with respect to the minimal DFA accepting l.

Equations

• M.StateCongruence = { r := fun (x y : List α) => ∀ (z : List α), M.mtr M.start (x ++ z) = M.mtr M.start (y ++ z), iseqv := ⋯, right_cov := ⋯ }

theorem Cslib.Automata.DA.FinAcc.stateCongruence_le_nerodeCongruence {State : Type u_1} {α : Type} {M : FinAcc State α} {x y : List α} (h : M.StateCongruence.eq x y) : (Acceptor.language M).NerodeCongruence.eq x y

The Nerode congruence is the most coarse state congruence given a language.

theorem Cslib.Automata.DA.FinAcc.unique_minimal {State : Type u_1} {α : Type} {M : FinAcc State α} [Finite State] (l : Language α) (hr : l.IsRegular) (hm : M.IsMinimalAutomaton l) : ∃! φ : State ≃ l.NerodeQuotient, ∀ (x : List α), φ (M.mtr M.start x) = ⟦x⟧

The minimal DFA M accepting the language l is unique up to unique isomorphism.