Myhill–Nerode theorem
In the theory of formal languages, the Myhill–Nerode theorem provides a necessary and sufficient condition for a language to be regular. The theorem is named for John Myhill and Anil Nerode, who proved it at the University of Chicago in 1958 (Nerode 1958).
Given a language L, and a pair of strings x and y, define a distinguishing extension to be a string z such that exactly one of the two strings xz and yz belongs to L. Define a relation RL on strings by the rule that x RL y if there is no distinguishing extension for x and y. It is easy to show that RL is an equivalence relation on strings, and thus it divides the set of all strings into equivalence classes.
The Myhill–Nerode theorem states that L is regular if and only if RL has a finite number of equivalence classes, and moreover that the number of states in the smallest deterministic finite automaton (DFA) recognizing L is equal to the number of equivalence classes in RL. In particular, this implies that there is a unique minimal DFA with minimum number of states (Hopcroft & Ullman 1979).
If L is a regular language, then by definition there is a DFA A that recognizes it, with only finitely many states. If there are n states, then partition the set of all finite strings into n subsets, where subset Si is the set of strings that, when given as input to automaton A, cause it to end in state i. For every two strings x and y that belong to the same state, and for every choice of a third string z, automaton A reaches the same state on input xz as it reaches on input yz, and therefore must either accept both of the inputs xz and yz or reject both of them. Therefore, no string z can be a distinguishing extension for x and y, so they must be related by RL. Thus, Si is a subset of an equivalence class of RL. Combining this fact with the fact that every member of one of these equivalence classes belongs to one of the sets Si, this gives a many-to-one relation from states of A to equivalence classes, implying that the number of equivalence classes is finite and at most n.
...
Wikipedia