Myhill–Nerode theorem

DefinitionNerode equivalence#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). Two words \(x, y \in \Sigma^*\) are Nerode equivalent for \(L\) when they have the same left quotient, that is, \(\{z \in \Sigma^* \mid xz \in L\} = \{z \in \Sigma^* \mid yz \in L\}\).

def nerodeRel (L : Language Symbol) (x y : List Symbol) : Prop :=
  L.leftQuotient x = L.leftQuotient y

Used by 19

Used byStates of Brzozowski's automaton as residual languages · Brzozowski's automaton identifies exactly the Nerode equivalent words · Brzozowski's automaton is the minimal automaton · The Nerode congruence relates words with equal left quotients · Nerode classes are the residual languages · The residual language of a Nerode class · Distinguishable words reach different DFA states · Nerode equivalent words agree on membership · Bijection between Nerode classes and left quotients · Appending the empty word preserves the Nerode class · Nerode equivalence is a right congruence · Appending a symbol preserves Nerode equivalence · Continuation characterization of Nerode equivalence · Nerode equivalence is equivalence of the reached states · Words reaching the same DFA state are Nerode equivalent · The Nerode setoid · Distinct Nerode classes reach distinct states · Equal syntactic classes give equal Nerode classes · Syntactic equivalence refines Nerode equivalence

DefinitionThe Nerode setoid#✓fully proved

For a language \(L\) over an alphabet \(\Sigma\), the Nerode setoid of \(L\) is the set \(\Sigma^*\) of words equipped with Nerode equivalence for \(L\), which is reflexive, symmetric and transitive.

def nerodeSetoid (L : Language Symbol) : Setoid (List Symbol) where
  r := nerodeRel L
  iseqv := ⟨nerodeRel_refl L, nerodeRel_symm, nerodeRel_trans⟩

Uses 1 · Used by 10

Statement usesNerode equivalence

Used byAccepting Nerode classes · Residual map on Nerode classes · Nerode classes · Nerode class of a word · Bijection between Nerode classes and left quotients · Every state of the Nerode automaton is reachable · Representative of a Nerode class · Transition on Nerode classes · Distinct Nerode classes reach distinct states · Equal syntactic classes give equal Nerode classes

AbbreviationNerode classes#✓fully proved

For a language \(L\) over an alphabet \(\Sigma\), the Nerode classes of \(L\) are the elements of the quotient of the set of words over \(\Sigma\) by Nerode equivalence for \(L\), under which two words \(x\) and \(y\) are equivalent when they have the same left quotient, that is, when for every word \(z\) we have \(xz \in L\) if and only if \(yz \in L\).

abbrev NerodeClass (L : Language Symbol) := Quotient (nerodeSetoid L)

Uses 1 · Used by 24

Statement usesThe Nerode setoid

Used byWhen finite, the minimized DFA has as many states as there are Nerode classes · Reachable residuals of the minimized DFA · Nerode classes and reachable residuals · Moore's automaton has one state per Nerode class · Accepting Nerode classes · The Nerode automaton recognizes its language · Equality case of the Nerode state bound · Nerode classes bound the number of DFA states · Strict Nerode state bound · Residual map on Nerode classes · Finitely many Nerode classes iff finitely many left quotients · Myhill–Nerode theorem, quotient form · Myhill–Nerode lower bound via left quotients · Nerode class of a word · Nerode classes correspond to reachable residuals · Bijection between Nerode classes and left quotients · The Nerode automaton · Every state of the Nerode automaton is reachable · Representative of a Nerode class · Transition on Nerode classes · Nerode classes to DFA states · Distinct Nerode classes reach distinct states · Equal syntactic classes give equal Nerode classes · Regular languages have finite syntactic monoids

TheoremContinuation characterization of Nerode equivalence#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). Two words \(x, y \in \Sigma^*\) are Nerode equivalent for \(L\) if and only if, for every word \(z \in \Sigma^*\), \(xz \in L\) holds exactly when \(yz \in L\).

theorem nerodeRel_iff {x y : List Symbol} :
    nerodeRel L x y ↔ ∀ z, x ++ z ∈ L ↔ y ++ z ∈ L

Uses 1 · Used by 4

Statement usesNerode equivalence

Used byDistinguishable words reach different DFA states · Nerode equivalent words agree on membership · Words reaching the same DFA state are Nerode equivalent · Syntactic equivalence refines Nerode equivalence

TheoremNerode equivalent words agree on membership#✓fully proved

Let \(L\) be a language. If two words \(x\) and \(y\) are Nerode equivalent for \(L\), then \(x \in L\) if and only if \(y \in L\).

theorem nerodeRel.mem_iff {x y : List Symbol} (h : nerodeRel L x y) : x ∈ L ↔ y ∈ L

Uses 2 · Used by 1

Statement usesNerode equivalence

Proof usesContinuation characterization of Nerode equivalence

Used byAccepting Nerode classes

TheoremNerode equivalence is a right congruence#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). If two words \(x, y \in \Sigma^*\) are Nerode equivalent for \(L\), then for every word \(z \in \Sigma^*\) the words \(xz\) and \(yz\) are Nerode equivalent for \(L\).

theorem nerodeRel_append_right {x y : List Symbol} (h : nerodeRel L x y)
    (z : List Symbol) : nerodeRel L (x ++ z) (y ++ z)

Uses 1 · Used by 1

Statement usesNerode equivalence

Used byAppending a symbol preserves Nerode equivalence

TheoremAppending a symbol preserves Nerode equivalence#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). If two words \(x, y \in \Sigma^*\) are Nerode equivalent for \(L\), then for every symbol \(a \in \Sigma\) the words \(xa\) and \(ya\) are Nerode equivalent for \(L\).

theorem nerodeRel_append_singleton {x y : List Symbol} (h : nerodeRel L x y)
    (a : Symbol) : nerodeRel L (x ++ [a]) (y ++ [a])

Uses 2 · Used by 1

Statement usesNerode equivalence

Proof usesNerode equivalence is a right congruence

Used byTransition on Nerode classes

TheoremAppending the empty word preserves the Nerode class#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). For every word \(x \in \Sigma^*\), the word \(x\varepsilon\) obtained by appending the empty word \(\varepsilon\) is Nerode equivalent to \(x\) for \(L\).

@[simp]
theorem nerodeRel_append_nil (x : List Symbol) : nerodeRel L (x ++ []) x

Uses 1

Statement usesNerode equivalence

DefinitionNerode class of a word#✓fully proved

For a language \(L\) and a word \(x\), the Nerode class \([x]\) of \(x\) is the equivalence class of \(x\) under Nerode equivalence for \(L\).

def nerodeClass (L : Language Symbol) (x : List Symbol) : NerodeClass L :=
  Quotient.mk (nerodeSetoid L) x

Uses 2 · Used by 6

Statement usesNerode classes · The Nerode setoid

Used byThe Nerode automaton recognizes its language · Bijection between Nerode classes and left quotients · The Nerode automaton · Every state of the Nerode automaton is reachable · Distinct Nerode classes reach distinct states · Equal syntactic classes give equal Nerode classes

DefinitionResidual map on Nerode classes#✓fully proved

Let \(L\) be a language. The residual map sends the Nerode class \([x]\) of a word \(x\) to the left quotient \(x^{-1}L = \{ y \mid xy \in L \}\), viewed as an element of the set \(\{ w^{-1}L \mid w \text{ a word} \}\) of left quotients of \(L\). It is well-defined because Nerode equivalent words have the same left quotient.

def classResidual (L : Language Symbol) : NerodeClass L → Set.range L.leftQuotient :=
  Quotient.lift
    (fun x ↦ ⟨L.leftQuotient x, ⟨x, rfl⟩⟩)
    (fun _ _ h ↦ Subtype.ext h)

Uses 2 · Used by 1

Statement usesNerode classes · The Nerode setoid

Used byBijection between Nerode classes and left quotients

DefinitionBijection between Nerode classes and left quotients#✓fully proved

For every language \(L\), the map sending the Nerode class \([x]\) of a word \(x\) to the left quotient \(x^{-1}L = \{ y \mid xy \in L \}\) is a bijection from the set of Nerode classes of \(L\) onto the set \(\{ w^{-1}L \mid w \text{ a word} \}\) of left quotients of \(L\).

noncomputable def nerodeClassEquivResidual (L : Language Symbol) :
    NerodeClass L ≃ Set.range L.leftQuotient :=
  Equiv.ofBijective (classResidual L) ⟨classResidual_injective, classResidual_surjective⟩

Uses 5 · Used by 2

Statement usesNerode classes · Residual map on Nerode classes · Nerode class of a word · Nerode equivalence · The Nerode setoid

Used byFinitely many Nerode classes iff finitely many left quotients · Nerode classes correspond to reachable residuals

DefinitionTransition on Nerode classes#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\) and \(a \in \Sigma\) a symbol. Appending \(a\) sends the Nerode class of a word \(x\) to the Nerode class of \(xa\); this is well defined because Nerode equivalence is preserved by appending a symbol.

def NerodeClass.step (a : Symbol) : NerodeClass L → NerodeClass L :=
  Quotient.map (· ++ [a]) (fun _ _ h ↦ nerodeRel_append_singleton h a)

Uses 3 · Used by 1

Statement usesNerode classes · Appending a symbol preserves Nerode equivalence · The Nerode setoid

Used byThe Nerode automaton

DefinitionAccepting Nerode classes#✓fully proved

Let \(L\) be a language. The accepting Nerode classes of \(L\) are those whose words belong to \(L\): the Nerode class \([x]\) of a word \(x\) is accepting if and only if \(x \in L\). This is well-defined because Nerode equivalent words are either both in \(L\) or both outside \(L\).

def NerodeClass.Accepting (L : Language Symbol) : Set (NerodeClass L) :=
  {q | Quotient.lift (s := nerodeSetoid L) (fun x ↦ x ∈ L)
    (fun _ _ h ↦ propext (nerodeRel.mem_iff h)) q}

Uses 3 · Used by 2

Statement usesNerode classes · Nerode equivalent words agree on membership · The Nerode setoid

Used byThe Nerode automaton recognizes its language · The Nerode automaton

DefinitionThe Nerode automaton#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). The Nerode automaton of \(L\) is the deterministic automaton over \(\Sigma\), not necessarily finite, whose states are the Nerode classes of words for \(L\), whose start state is the class of the empty word, which on reading a symbol \(a \in \Sigma\) moves from the class of a word \(x\) to the class of \(xa\), and whose accepting states are the classes of the words in \(L\).

def nerodeDFA (L : Language Symbol) : DFA Symbol (NerodeClass L) where
  step q a := q.step a
  start := nerodeClass L []
  accept := NerodeClass.Accepting L

Uses 4 · Used by 3

Statement usesNerode classes · Accepting Nerode classes · Transition on Nerode classes · Nerode class of a word

Used byThe Nerode automaton recognizes its language · Every state of the Nerode automaton is reachable · Regular languages have finite syntactic monoids

TheoremThe Nerode automaton recognizes its language#✓fully proved

For every language \(L\), the language accepted by the Nerode automaton of \(L\) is exactly \(L\).

@[simp]
theorem accepts_nerodeDFA : (nerodeDFA L).accepts = L

Uses 4 · Used by 1

Statement usesNerode classes · The Nerode automaton

Proof usesAccepting Nerode classes · Nerode class of a word

Used byRegular languages have finite syntactic monoids

TheoremEvery state of the Nerode automaton is reachable#✓fully proved

For every language \(L\) and every Nerode class \(q\) of \(L\), there is a word \(x\) such that the Nerode automaton of \(L\), started in its start state and reading \(x\), ends in the state \(q\).

theorem nerodeDFA_state_reachable (q : NerodeClass L) :
    ∃ x, (nerodeDFA L).eval x = q

Uses 4

Statement usesNerode classes · The Nerode automaton

Proof usesNerode class of a word · The Nerode setoid

TheoremFinitely many Nerode classes iff finitely many left quotients#✓fully proved

For every language \(L\), writing \(x^{-1}L = \{ y \mid xy \in L \}\) for the left quotient of \(L\) by a word \(x\), there are finitely many Nerode classes of \(L\) if and only if the set \(\{ x^{-1}L \mid x \text{ a word} \}\) of left quotients of \(L\) is finite.

This is the quotient formulation of the Myhill--Nerode criterion.

theorem finite_nerodeClass_iff : Finite (NerodeClass L) ↔ (Set.range L.leftQuotient).Finite

Uses 2 · Used by 1

Statement usesNerode classes

Proof usesBijection between Nerode classes and left quotients

Used byMyhill–Nerode theorem, quotient form

TheoremMyhill–Nerode theorem, quotient form#✓fully proved

A language \(L\) is regular, that is, accepted by some deterministic finite automaton, if and only if \(L\) has finitely many Nerode classes.

theorem isRegular_iff_finite_nerodeClass : L.IsRegular ↔ Finite (NerodeClass L)

Uses 2 · Used by 1

Statement usesNerode classes

Proof usesFinitely many Nerode classes iff finitely many left quotients

Used byRegular languages have finite syntactic monoids

DefinitionDistinguishable words#✓fully proved

Let \(L\) be a language over an alphabet \(\Sigma\). Two words \(x\) and \(y\) over \(\Sigma\) are distinguishable by \(L\) when there is a word \(z\) over \(\Sigma\) such that exactly one of \(xz\) and \(yz\) belongs to \(L\).

def Distinguishable (L : Language Symbol) (x y : List Symbol) : Prop :=
  ∃ z, ¬(x ++ z ∈ L ↔ y ++ z ∈ L)

Used by 1

Used byDistinguishable words reach different DFA states

TheoremWords reaching the same DFA state are Nerode equivalent#✓fully proved

Let \(M\) be a DFA and let \(L\) be the language it accepts. If \(M\) reaches the same state from its start state on reading the words \(x\) and \(y\), then \(x\) and \(y\) are Nerode equivalent for \(L\).

theorem nerodeRel_of_eval_eq (M : DFA Symbol State) {x y : List Symbol}
    (hxy : M.eval x = M.eval y) : nerodeRel M.accepts x y

Uses 2 · Used by 2

Statement usesNerode equivalence

Proof usesContinuation characterization of Nerode equivalence

Used byDistinguishable words reach different DFA states · Distinct Nerode classes reach distinct states

TheoremDistinguishable words reach different DFA states#✓fully proved

Let \(L\) be a language and let \(M\) be a DFA that accepts exactly \(L\). If two words \(x\) and \(y\) are distinguishable by \(L\), then the states that \(M\) reaches from its start state on reading \(x\) and on reading \(y\) are different.

theorem eval_ne_of_distinguishable (M : DFA Symbol State) (hM : M.accepts = L)
    {x y : List Symbol} (hxy : Distinguishable L x y) : M.eval x ≠ M.eval y

Uses 4

Statement usesDistinguishable words

Proof usesNerode equivalence · Continuation characterization of Nerode equivalence · Words reaching the same DFA state are Nerode equivalent

DefinitionEquivalent states of a DFA#✓fully proved

Two states \(p\) and \(q\) of a DFA \(M\) are equivalent when they accept the same continuation language: for every word \(z\), running \(M\) from \(p\) on \(z\) ends in an accepting state if and only if running \(M\) from \(q\) on \(z\) does.

def StateEquivalent (M : DFA Symbol State) (p q : State) : Prop :=
  M.acceptsFrom p = M.acceptsFrom q

Used by 6

Used byStates of Brzozowski's automaton as residual languages · Brzozowski's automaton is the minimal automaton · Injectivity of the canonical residual map · State-separated DFA · Nerode equivalence is equivalence of the reached states · Syntactically equivalent words act identically

TheoremNerode equivalence is equivalence of the reached states#✓fully proved

Let \(M\) be a DFA and let \(L\) be the language it accepts. Two words \(x\) and \(y\) are Nerode equivalent for \(L\) if and only if the states that \(M\) reaches from its start state on reading \(x\) and on reading \(y\) are observationally equivalent, that is, \(M\) accepts the same language from both states.

theorem nerodeRel_iff_stateEquivalent (M : DFA Symbol State) {x y : List Symbol} :
    nerodeRel M.accepts x y ↔ StateEquivalent M (M.eval x) (M.eval y)

Uses 2 · Used by 2

Statement usesEquivalent states of a DFA · Nerode equivalence

Used byStates of Brzozowski's automaton as residual languages · Brzozowski's automaton is the minimal automaton

DefinitionResidual languages of reachable states#✓fully proved

For a DFA \(M\) and a state \(q\) of \(M\), let \(L_q\) be the language of words \(z\) such that running \(M\) from \(q\) on \(z\) ends in an accepting state. The reachable residuals of \(M\) form the set of the languages \(L_q\) over all states \(q\) that \(M\) reaches from its start state on some input word.

This semantic state space forgets duplicate DFA states that accept the same continuations.

def reachableResiduals (M : DFA Symbol State) : Set (Language Symbol) :=
  Set.range (M.acceptsFrom ∘ M.eval)

Used by 22

Used byStates of Brzozowski's automaton as residual languages · Residual language of a state of Brzozowski's automaton · Brzozowski's automaton is the minimal automaton · Left quotients as reachable residuals · Minimized DFA · The minimized DFA accepts the same language · The minimized DFA is accessible · When finite, the minimized DFA has as many states as there are Nerode classes · States reached in the minimized DFA · Evaluation in the minimized DFA agrees with the left-quotient automaton · Transitions of the minimized DFA on reached states · Transitions of the minimized DFA · Residual reached by a word · Reachable residuals of the minimized DFA · Nerode classes and reachable residuals · The canonical automaton of a DFA's language is its minimized DFA · Moore's automaton has one state per Nerode class · Moore classes are the reachable residuals · Continuation language of a Moore class · Moore's automaton is the minimal automaton · Myhill–Nerode lower bound via left quotients · Nerode classes correspond to reachable residuals

DefinitionNerode classes correspond to reachable residuals#✓fully proved

Let \(L\) be a language and let \(M\) be a DFA that accepts exactly \(L\). This is the bijection from the Nerode classes of \(L\) to the reachable residuals of \(M\), the languages accepted by \(M\) from states it reaches from its start state. It sends the Nerode class of a word \(x\) to the left quotient \(\{z \mid xz \in L\}\), which is the language \(M\) accepts from the state it reaches on reading \(x\).

noncomputable def nerodeClassEquivReachableResiduals (M : DFA Symbol State)
    (hM : M.accepts = L) : NerodeClass L ≃ reachableResiduals M :=
  (nerodeClassEquivResidual L).trans
    (Equiv.cast
      (congrArg (fun s : Set (Language Symbol) ↦ ↥s) (reachableResiduals_eq M hM).symm))

Uses 3 · Used by 3

Statement usesNerode classes · Bijection between Nerode classes and left quotients · Residual languages of reachable states

Used byReachable residuals of the minimized DFA · Nerode classes and reachable residuals · Myhill–Nerode lower bound via left quotients

DefinitionRepresentative of a Nerode class#✓fully proved

For a language \(L\) and a Nerode class \(q\) of \(L\), the representative of \(q\) is a word whose Nerode class is \(q\), chosen once and for all.

noncomputable def NerodeClass.representative (q : NerodeClass L) : List Symbol :=
  Quotient.out q

Uses 2 · Used by 2

Statement usesNerode classes · The Nerode setoid

Used byNerode classes to DFA states · Distinct Nerode classes reach distinct states

DefinitionNerode classes to DFA states#✓fully proved

For a language \(L\) and a DFA \(M\) over the same alphabet, this map sends each Nerode class \(q\) of \(L\) to the state that \(M\) reaches from its start state on the chosen representative of \(q\).

Unlike the canonical map from words to states, this does not claim that equivalent words reach equal states in a nonminimal DFA.

noncomputable def NerodeClass.toDFAState (M : DFA Symbol State) (q : NerodeClass L) : State :=
  M.eval q.representative

Uses 2 · Used by 5

Statement usesNerode classes · Representative of a Nerode class

Used byEquality case of the Nerode state bound · Nerode classes bound the number of DFA states · Strict Nerode state bound · Myhill–Nerode lower bound via left quotients · Distinct Nerode classes reach distinct states

TheoremDistinct Nerode classes reach distinct states#✓fully proved

Let \(M\) be a DFA that accepts exactly the language \(L\). Then the map sending each Nerode class of \(L\) to the state that \(M\) reaches from its start state on the chosen representative of the class is injective. In particular, \(M\) has at least one distinct state for each Nerode class.

theorem NerodeClass.toDFAState_injective (M : DFA Symbol State) (hM : M.accepts = L) :
    Function.Injective (NerodeClass.toDFAState (L := L) M)

Uses 7 · Used by 4

Statement usesNerode classes · Nerode classes to DFA states

Proof usesRepresentative of a Nerode class · Nerode class of a word · Nerode equivalence · Words reaching the same DFA state are Nerode equivalent · The Nerode setoid

Used byEquality case of the Nerode state bound · Nerode classes bound the number of DFA states · Strict Nerode state bound · Myhill–Nerode lower bound via left quotients

TheoremNerode classes bound the number of DFA states#✓fully proved

Let \(L\) be a language with finitely many Nerode classes, and let \(M\) be a DFA with a finite set of states \(Q\) that accepts exactly \(L\). Then the number of Nerode classes of \(L\) is at most \(|Q|\).

theorem card_nerodeClass_le_card_state [Fintype (NerodeClass L)] [Fintype State]
    (M : DFA Symbol State) (hM : M.accepts = L) :
    Fintype.card (NerodeClass L) ≤ Fintype.card State

Uses 3 · Used by 1

Statement usesNerode classes

Proof usesNerode classes to DFA states · Distinct Nerode classes reach distinct states

Used byMyhill–Nerode lower bound via left quotients

TheoremMyhill–Nerode lower bound via left quotients#✓fully proved

Let \(L\) be a language and let \(M\) be a DFA with a finite set of states \(Q\) that accepts exactly \(L\). For a word \(x\), the left quotient of \(L\) by \(x\) is the language \(\{z \mid xz \in L\}\). Then the number of distinct left quotients of \(L\) is at most \(|Q|\).

theorem natCard_range_leftQuotient_le_natCard_state [Finite State] (M : DFA Symbol State)
    (hM : M.accepts = L) :
    Nat.card (Set.range L.leftQuotient) ≤ Nat.card State

Uses 6

Proof usesNerode classes · Nerode classes to DFA states · Distinct Nerode classes reach distinct states · Nerode classes bound the number of DFA states · Nerode classes correspond to reachable residuals · Residual languages of reachable states

TheoremEquality case of the Nerode state bound#✓fully proved

Let \(L\) be a language with finitely many Nerode classes, and let \(M\) be a DFA with a finite set of states \(Q\) that accepts exactly \(L\). Send each Nerode class of \(L\) to the state that \(M\) reaches from its start state on the chosen representative word of the class. Then the number of Nerode classes of \(L\) equals \(|Q|\) if and only if every state in \(Q\) is the image of some Nerode class under this map.

theorem card_nerodeClass_eq_card_state_iff [Fintype (NerodeClass L)] [Fintype State]
    (M : DFA Symbol State) (hM : M.accepts = L) :
    Fintype.card (NerodeClass L) = Fintype.card State ↔
      Function.Surjective (NerodeClass.toDFAState (L := L) M)

Uses 3

Statement usesNerode classes · Nerode classes to DFA states

Proof usesDistinct Nerode classes reach distinct states

TheoremStrict Nerode state bound#✓fully proved

Let \(L\) be a language with finitely many Nerode classes, and let \(M\) be a DFA with a finite set of states \(Q\) that accepts exactly \(L\). Send each Nerode class of \(L\) to the state that \(M\) reaches from its start state on the chosen representative word of the class. If some state in \(Q\) is not the image of any Nerode class under this map, then the number of Nerode classes of \(L\) is strictly less than \(|Q|\).

theorem card_nerodeClass_lt_card_state [Fintype (NerodeClass L)] [Fintype State]
    (M : DFA Symbol State) (hM : M.accepts = L)
    (hred : ¬Function.Surjective (NerodeClass.toDFAState (L := L) M)) :
    Fintype.card (NerodeClass L) < Fintype.card State

Uses 3

Statement usesNerode classes · Nerode classes to DFA states

Proof usesDistinct Nerode classes reach distinct states

DefinitionReachable state of a DFA#✓fully proved

A state is reachable when some input word reaches it from the start state.

def ReachableState (M : DFA Symbol State) (q : State) : Prop :=
  ∃ x, M.eval x = q

Used by 7

Used byThe canonical residual map · Uniqueness of the canonical residual map · The minimized DFA is accessible · The residual-language DFA is accessible · Accessible DFA · The syntactic DFA is accessible · Syntactically equivalent words act identically

DefinitionAccessible DFA#✓fully proved

A DFA is accessible when every state is reachable.

def Accessible (M : DFA Symbol State) : Prop :=
  ∀ q, ReachableState M q

Uses 1 · Used by 13

Statement usesReachable state of a DFA

Used byThe canonical residual map · Injectivity of the canonical residual map · The canonical residual map is surjective · Uniqueness of the canonical residual map · The minimized DFA is accessible · States of an accessible, state-separated DFA correspond to residuals · The residual-language DFA is accessible · Action of the syntactic monoid on states · Image of the syntactic action · Syntactic congruence as a kernel · The syntactic DFA is accessible · Syntactic equivalence via transition actions · Syntactically equivalent words act identically

34 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.