Synchronizing words for DFAs

A synchronizing word (or reset word) for a DFA M = (Q, Σ, δ) is a word w ∈ Σ* such that reading w from any state always leads to the same single state. A DFA is synchronizing if it admits at least one synchronizing word.

These notions support the Černý conjecture (see FormalConjectures.Wikipedia.CernyConjecture).

def DFA.IsSynchronizingWord {α : Type u_1} {σ : Type u_2} (M : DFA α σ) (w : List α) : Prop

A word w is a synchronizing word (or reset word) for a DFA M if reading w from any state leads to the same single state.

Equations

• M.IsSynchronizingWord w = ∃ (p : σ), ∀ (q : σ), M.evalFrom q w = p

def DFA.IsSynchronizing {α : Type u_1} {σ : Type u_2} (M : DFA α σ) : Prop

A DFA M is synchronizing if it has at least one synchronizing word.

Equations

• M.IsSynchronizing = ∃ (w : List α), M.IsSynchronizingWord w

@[simp]

theorem DFA.isSynchronizingWord_nil {α : Type u_1} {σ : Type u_2} (M : DFA α σ) : M.IsSynchronizingWord [] ↔ ∃ (p : σ), ∀ (q : σ), q = p

The empty word is a synchronizing word for M exactly when all states of M collapse to a single one (equivalently, σ is a nonempty subsingleton).

theorem DFA.IsSynchronizingWord.append {α : Type u_1} {σ : Type u_2} {M : DFA α σ} {w : List α} (hw : M.IsSynchronizingWord w) (v : List α) : M.IsSynchronizingWord (w ++ v)

Appending any word v to a synchronizing word w yields a synchronizing word: reading w already drives every state to a single state p, and reading v afterwards sends p to M.evalFrom p v regardless of the starting state.

theorem DFA.isSynchronizing_of_subsingleton {α : Type u_1} {σ : Type u_2} [Nonempty σ] [Subsingleton σ] (M : DFA α σ) : M.IsSynchronizing

A DFA whose state type is a nonempty subsingleton (i.e. a single-state DFA) is trivially synchronizing: the empty word already synchronizes it.