The Myhill-Nerode Theorem

Imagine you are building a machine to recognize a pattern — say, all binary strings that end in 01. The machine reads one character at a time and must remember just enough history to decide, at the end, whether the string belongs to the language.

How much memory does it need? The answer depends entirely on how many distinguishable situations the machine can be in. Two strings put the machine in the same situation if every possible continuation has identical outcomes: either both strings, extended by any suffix, land in the language, or neither does. When two strings are truly interchangeable like this, there is no reason to keep them in separate states.

This idea — grouping strings by their future behavior — is the Nerode equivalence relation, published by Anil Nerode in 1958 (and closely related to earlier work by John Myhill). The theorem that carries both names states something striking: a language is regular if and only if its Nerode equivalence has finitely many classes — and the number of classes is exactly the number of states in the smallest possible DFA for that language.

There is no wiggle room. The theorem is not an approximation. It gives you a precise lower bound, and it hands you the minimal automaton explicitly: each equivalence class becomes one state.

Choose a language below and enter a string. The demo computes its Nerode equivalence class — the set of suffixes that distinguish it from the empty string — and shows which DFA state it maps to. Feed several strings and watch the states emerge one by one as new classes appear.

<div class="controls">
  <label>{{label_language}}
    <select id="lang-select">
      <option value="ends01">{{opt_ends01}}</option>
      <option value="evenA">{{opt_evenA}}</option>
      <option value="aabb">{{opt_aabb}}</option>
    </select>
  </label>
  <div class="input-row">
    <input id="str-input" type="text" maxlength="20" placeholder="{{placeholder}}" spellcheck="false" autocomplete="off"/>
    <button id="add-btn" type="button">{{btn_add}}</button>
    <button id="reset-btn" type="button" class="ghost">{{btn_reset}}</button>
  </div>
</div>
<div class="panels">
  <div class="panel">
    <div class="panel-title">{{panel_classes}}</div>
    <div id="classes-list" class="classes-list"></div>
  </div>
  <div class="panel">
    <div class="panel-title">{{panel_dfa}}</div>
    <div id="dfa-view" class="dfa-view"></div>
  </div>
</div>
<div id="result-msg" class="result-msg"></div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }
.controls { display: flex; flex-direction: column; gap: .5rem; margin-bottom: .7rem; }
label { font-weight: 600; font-size: .85rem; color: #444; }
select { margin-left: .4rem; font: inherit; padding: .25rem .4rem; border: 1px solid #bbb; border-radius: 6px; background: #fff; cursor: pointer; }
.input-row { display: flex; gap: .4rem; flex-wrap: wrap; align-items: center; }
input[type=text] { font: inherit; padding: .3rem .6rem; border: 1px solid #bbb; border-radius: 6px; width: 160px; }
button { font: 600 13px system-ui; padding: .35rem .8rem; border: 1px solid #1d3557; background: #1d3557; color: #fff; border-radius: 7px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.panels { display: grid; grid-template-columns: 1fr 1fr; gap: .7rem; margin-bottom: .5rem; }
.panel { background: #f4f6f8; border-radius: 10px; padding: .6rem .8rem; min-height: 160px; }
.panel-title { font-weight: 700; font-size: .8rem; text-transform: uppercase; letter-spacing: .05em; color: #5a7088; margin-bottom: .4rem; }
.classes-list { display: flex; flex-direction: column; gap: .3rem; }
.class-item { display: flex; align-items: flex-start; gap: .4rem; font-size: .82rem; }
.class-badge { min-width: 24px; height: 24px; border-radius: 50%; display: flex; align-items: center; justify-content: center; font-weight: 700; font-size: .75rem; color: #fff; flex-shrink: 0; }
.class-info { line-height: 1.35; }
.class-label { font-weight: 600; }
.class-rep { color: #666; font-size: .78rem; font-family: ui-monospace, monospace; }
.dfa-view { display: flex; flex-direction: column; gap: .35rem; }
.dfa-state { display: flex; align-items: center; gap: .5rem; font-size: .82rem; padding: .25rem .4rem; border-radius: 7px; background: #e8eef3; border: 1px solid #cdd9e3; }
.dfa-state.accepting { background: #d4edda; border-color: #74c28a; }
.dfa-state.current { outline: 2px solid #e63946; outline-offset: 1px; }
.state-circle { width: 26px; height: 26px; border-radius: 50%; display: flex; align-items: center; justify-content: center; font-weight: 700; font-size: .78rem; color: #fff; flex-shrink: 0; }
.state-label { font-weight: 600; }
.state-desc { color: #555; font-size: .78rem; }
.result-msg { font-size: .88rem; font-weight: 600; min-height: 1.4em; padding: .2rem 0; }
.result-msg.ok { color: #0a7d33; }
.result-msg.info { color: #1d3557; }
.result-msg.new { color: #c05a00; }
@media (max-width: 500px) { .panels { grid-template-columns: 1fr; } }

// Code not found

Notice that once you have seen enough distinct classes, new strings stop creating new states — they fall into classes already found. For strings ending in 01, exactly three classes suffice: "the last two chars seen were neither 0 nor 01", "the last char was 0", and "the last two chars were 01 (accepting)". That is three states — and it is provably impossible to do it with fewer.

The Myhill-Nerode theorem is a characterization — an if-and-only-if — not just a sufficient condition. That makes it unusually powerful.

What it proves in one direction: if a language has finitely many Nerode classes, you can build a DFA directly from the class structure. The transitions are forced: reading character a from class [x] leads to class [xa]. The accepting states are exactly the classes of strings already in the language. This DFA is minimal by construction — removing any state would merge two distinct classes and break correctness.

What it proves in the other direction: if a language is regular, its Nerode relation has only finitely many classes. In particular, any DFA for the language defines a refinement of the Nerode relation (every pair of strings distinguishable by Nerode is also distinguishable by the DFA), so the number of DFA states is at least the number of Nerode classes. The minimal DFA has exactly as many states as classes.

Proving non-regularity. The contrapositive is just as important: if you can exhibit an infinite family of strings that are pairwise Nerode-distinguishable, the language is not regular and cannot be recognized by any finite automaton. The classic example is $a^{n}b^{n}$ (equal numbers of as then bs): the strings a, aa, aaa, … are all pairwise distinguishable because the suffix that accepts $a^{n}$ rejects aᵐ for m ≠ n. Therefore no finite automaton can recognize this language — a result also captured by the Pumping Lemma, but with more information.

Minimization algorithm. Given any DFA, you can compute the minimal equivalent DFA in polynomial time by iteratively merging states that are not distinguishable (Hopcroft's algorithm does it in $O(n \log n)$). Myhill-Nerode provides the theoretical foundation that guarantees the result is unique and optimal.

Status: proven, classical, constructive. The result is from 1958 and is a cornerstone of formal language theory alongside the Pumping Lemma and Kleene's theorem.

The Myhill-Nerode theorem is not just a mathematical curiosity. It underpins a wide range of practical tools:

• Lexer and scanner generation: tools like Lex and Flex generate minimal DFAs from regular expressions. Myhill-Nerode guarantees the result is optimal — no token recognizer can be smaller without changing what it accepts.
• Protocol verification: network protocols specify legal message sequences with regular languages. Minimal DFAs let model checkers compare protocol implementations against specifications efficiently.
• Text search and pattern matching: regular expression engines compile patterns into minimal automata. Smaller automata mean faster searches across large text corpora.
• Hardware design: finite-state machines in digital circuits are routinely minimized before synthesis. Fewer states mean fewer transistors and lower power consumption.
• Proving impossibility: whenever a language looks regular but is not, Myhill-Nerode gives the cleanest proof — exhibit infinitely many distinguishable strings. This is used constantly in formal verification to identify what finite-memory systems cannot do.
• Learning automata: the Angluin L* algorithm, the standard algorithm for learning an unknown regular language from a teacher, is essentially guided by the Myhill-Nerode structure: each equivalence class that gets discovered becomes a new state in the hypothesis DFA.

In short, every time a compiler, a verifier, or a search engine works with regular expressions, it relies — directly or indirectly — on what Myhill and Nerode proved in 1958.

The Myhill-Nerode theorem closes a circle that might seem open: given a language, how many states does the smallest recognizer need? The answer is the number of ways strings can behave differently in the future — the Nerode equivalence classes. Not an approximation, not a bound: the exact number.

This is what makes the theorem so satisfying. It turns an engineering question ("how small can I make this automaton?") into a mathematical one ("how many distinguishable futures does this language have?"), and the two questions turn out to have the same answer.

When a language has infinitely many distinguishable futures, no finite automaton can recognize it — and the theorem tells you so just as cleanly. The boundary between what finite machines can and cannot do is drawn by equivalence, and the counting is exact.

For a deeper look at minimization algorithms and their complexity, see Automata Minimization. For the broader picture of what regular languages can and cannot express, the Halting Problem and P vs NP show what happens when you remove the finite-memory constraint entirely.