Introduction

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.

Try It: Nerode Classes in Action

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>Language:
    <select id="lang-select">
      <option value="ends01">Binary strings ending in "01"</option>
      <option value="evenA">Binary strings with an even number of 0s</option>
      <option value="aabb">Strings of form a*b* (zero or more a’s then b’s)</option>
    </select>
  </label>
  <div class="input-row">
    <input id="str-input" type="text" maxlength="20" placeholder="Type a string (e.g. 101)" spellcheck="false" autocomplete="off"/>
    <button id="add-btn" type="button">Add string</button>
    <button id="reset-btn" type="button" class="ghost">Reset</button>
  </div>
</div>
<div class="panels">
  <div class="panel">
    <div class="panel-title">Nerode Classes Found</div>
    <div id="classes-list" class="classes-list"></div>
  </div>
  <div class="panel">
    <div class="panel-title">Minimal DFA States</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; } }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Myhill-Nerode theorem demo.
// Each language defines a classOf(string) function that returns
// the Nerode equivalence class index for that string.
// Two strings x, y are Nerode-equivalent iff for ALL suffixes z:
//   (xz in L) <=> (yz in L)
// The class index is a compact representation of "which future behavior."

const COLORS = ['#1d6fa5','#c05a00','#0a7d33','#8b3a8f','#b5500a','#1a6060'];
const LANGS = {
  ends01: {
    name: `Ends in "01"`,
    alphabet: '01',
    // States: 0=neither, 1=last was ’0’, 2=last two were ’01’ (accept)
    classOf(s) {
      // Simulate DFA: q0=0, q1=1, q2=2
      let q = 0;
      for (const c of s) {
        if (q === 0) q = (c === '0') ? 1 : 0;
        else if (q === 1) q = (c === '1') ? 2 : (c === '0' ? 1 : 0);
        else q = (c === '0') ? 1 : 0; // q2, saw ’1’->q0, ’0’->q1 (need fresh 0)
      }
      return q;
    },
    classNames: [`Start / other`, `Last char was "0"`, `Ended in "01" ✓`],
    classDesc: [`Strings not ending in 0 or 01`, `Last char is 0 — one step from accepting`, `Accepted: last two chars are "01"`],
    accepting: new Set([2]),
    totalClasses: 3,
  },
  evenA: {
    name: `Even number of 0s`,
    alphabet: '01',
    classOf(s) {
      let count = 0;
      for (const c of s) if (c === '0') count++;
      return count % 2; // 0=even(accept), 1=odd
    },
    classNames: [`Even 0s ✓`, `Odd 0s`],
    classDesc: [`Accepted: count of 0s is even (including 0)`, `Odd number of 0s seen — one 0 away from accepting`],
    accepting: new Set([0]),
    totalClasses: 2,
  },
  aabb: {
    name: `a*b* (a’s then b’s)`,
    alphabet: 'ab',
    // States: 0=only a’s so far (or empty), 1=seen at least one b, 2=error (b then a)
    classOf(s) {
      let state = 0;
      for (const c of s) {
        if (state === 0) { if (c === 'b') state = 1; }
        else if (state === 1) { if (c === 'a') state = 2; }
        // state 2 is a dead state
      }
      return state;
    },
    classNames: [`Only a’s (or empty) ✓`, `In b-section ✓`, `Invalid (b before a)`],
    classDesc: [`Accepted: pure a-prefix — still valid`, `Accepted: in b-section — still valid`, `Dead: saw an a after a b`],
    accepting: new Set([0, 1]),
    totalClasses: 3,
  }
};

let currentLang = LANGS.ends01;
let foundClasses = []; // array of {idx, reps:[string]}
let lastClassIdx = null;

function getLang() { return LANGS[document.getElementById('lang-select').value]; }

function classColor(idx) { return COLORS[idx % COLORS.length]; }

function renderClasses() {
  const el = document.getElementById('classes-list');
  if (foundClasses.length === 0) { el.innerHTML = '<span style="color:#888;font-size:.82rem">No strings added yet.</span>'; return; }
  el.innerHTML = foundClasses.map(fc => {
    const lang = currentLang;
    return fmt(`<div class="class-item">
      <div class="class-badge" style="background:%classColor%">%idx%</div>
      <div class="class-info">
        <div class="class-label">%v%</div>
        <div class="class-rep">e.g. "%map%"</div>
      </div>
    </div>`, { classColor: classColor(fc.idx), idx: fc.idx, v: lang.classNames[fc.idx], map: fc.reps.slice(0,3).map(s=>s===''?'ε':s).join('", "') });
  }).join('');
}

function renderDFA() {
  const el = document.getElementById('dfa-view');
  if (foundClasses.length === 0) { el.innerHTML = '<span style="color:#888;font-size:.82rem">Add strings to see states emerge.</span>'; return; }
  const lang = currentLang;
  el.innerHTML = foundClasses.map(fc => {
    const isAccepting = lang.accepting.has(fc.idx);
    const isCurrent = fc.idx === lastClassIdx;
    return fmt(`<div class="dfa-state%v%%v2%">
      <div class="state-circle" style="background:%classColor%">%idx%</div>
      <div>
        <div class="state-label">State %idx%%v3%</div>
        <div class="state-desc">%v4%</div>
      </div>
    </div>`, { v: isAccepting?' accepting':'', v2: isCurrent?' current':'', classColor: classColor(fc.idx), idx: fc.idx, v3: isAccepting ? ' (accepting)' : '', v4: lang.classDesc[fc.idx] });
  }).join('');
}

function addString() {
  const input = document.getElementById('str-input');
  const s = input.value.trim();
  const lang = currentLang;
  const msgEl = document.getElementById('result-msg');

  // Validate alphabet
  const alpha = lang.alphabet;
  for (const c of s) {
    if (!alpha.includes(c)) {
      msgEl.textContent = fmt(`"%c%" is not in the alphabet {%split%}.`, { c: c, split: alpha.split('').join(', ') });
      msgEl.className = 'result-msg info'; return;
    }
  }

  const idx = lang.classOf(s);
  lastClassIdx = idx;
  const display = s === '' ? `ε (empty string)` : `"${s}"`;
  const alreadyFound = foundClasses.some(fc => fc.idx === idx);
  if (!alreadyFound) {
    foundClasses.push({ idx, reps: [s] });
    foundClasses.sort((a, b) => a.idx - b.idx);
    msgEl.textContent = fmt(`New class discovered! %display% → State %idx%: %v%`, { display: display, idx: idx, v: lang.classNames[idx] });
    msgEl.className = 'result-msg new';
    if (foundClasses.length === lang.totalClasses) {
      setTimeout(()=>{ msgEl.textContent = fmt(`All %totalClasses% Nerode classes found — this is the complete minimal DFA!`, { totalClasses: lang.totalClasses }); msgEl.className='result-msg ok'; }, 800);
    }
  } else {
    foundClasses.find(fc => fc.idx === idx).reps.push(s);
    msgEl.textContent = fmt(`%display% → State %idx%: %v% (class already known)`, { display: display, idx: idx, v: lang.classNames[idx] });
    msgEl.className = 'result-msg info';
  }

  renderClasses();
  renderDFA();
  input.value = '';
  input.focus();
}

function reset() {
  foundClasses = [];
  lastClassIdx = null;
  document.getElementById('str-input').value = '';
  document.getElementById('result-msg').textContent = '';
  document.getElementById('result-msg').className = 'result-msg';
  renderClasses();
  renderDFA();
}

document.getElementById('lang-select').addEventListener('change', () => {
  currentLang = getLang();
  reset();
});
document.getElementById('add-btn').addEventListener('click', addString);
document.getElementById('str-input').addEventListener('keydown', e => { if (e.key === 'Enter') addString(); });
document.getElementById('reset-btn').addEventListener('click', reset);

// Seed with empty string
currentLang = getLang();
renderClasses();
renderDFA();
document.getElementById('result-msg').textContent = `Try: type "0", "1", "01", "001", "10" and press Add.`;
document.getElementById('result-msg').className = 'result-msg info';
Result
Console

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 Real Depth

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 anbna^{n}b^{n} (equal numbers of as then bs): the strings a, aa, aaa, … are all pairwise distinguishable because the suffix that accepts ana^{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(nlog⁡n)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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/myhill-nerode/Content licensed under CC BY-NC 4.0.