Brzozowski's algorithm
Determinized reversal
DefinitionDeterminized reversal of a DFA#✓fully proved
For a DFA \(M\) with finitely many states, the determinized reversal of \(M\) is the subset construction applied to the reversal of \(M\): its states are the sets of states of \(M\); reading a letter \(a\) from a set \(S\) leads to the set of states \(q\) whose \(a\)-successor in \(M\) lies in \(S\); its start state is the set of accepting states of \(M\); and it accepts exactly the sets that contain the start state of \(M\).
def revDet : DFA α (Finset σ) where
step S a := Finset.univ.filter fun q => M.step q a ∈ S
start := Finset.univ.filter (· ∈ M.accept)
accept := {S | M.start ∈ S}Used by 11
TheoremStates reached in the determinized reversal#✓fully proved
Let \(M\) be a DFA with finitely many states and \(w\) a word. On input \(w\), the determinized reversal of \(M\) reaches the set of states \(q\) of \(M\) from which \(M\), reading \(w\) backwards starting at \(q\), ends in an accepting state.
theorem revDet_eval (w : List α) :
M.revDet.eval w = Finset.univ.filter fun q => M.evalFrom q w.reverse ∈ M.acceptUses 1 · Used by 2
TheoremThe determinized reversal accepts the reversed language#✓fully proved
Let \(M\) be a DFA with finitely many states and \(L\) its language, and write \(w^R\) for the word \(w\) read backwards. The determinized reversal of \(M\) accepts exactly the reversed language \(L^R = \{w \mid w^R \in L\}\).
theorem revDet_accepts : M.revDet.accepts = M.accepts.reverseUses 2 · Used by 2
TheoremBrzozowski's lemma#✓fully proved
Let \(M\) be a DFA with finitely many states in which every state is reached from the start state by some word, and let \(L\) be its language. Write \(u^R\) for the word \(u\) read backwards, \(L^R = \{u \mid u^R \in L\}\) for the reversed language, and \(w^{-1}K = \{v \mid wv \in K\}\) for the left quotient of a language \(K\) by a word \(w\). Then two words \(w\) and \(w'\) lead the determinized reversal of \(M\) from its start state to the same set of states if and only if \(w^{-1}L^R = w'^{-1}L^R\).
theorem revDet_eval_eq_iff (hacc : ∀ q, ∃ u, M.eval u = q) {w w' : List α} :
M.revDet.eval w = M.revDet.eval w' ↔
M.accepts.reverse.leftQuotient w = M.accepts.reverse.leftQuotient w'Uses 2 · Used by 1
Brzozowski's algorithm
AbbreviationStates of the intermediate Brzozowski automaton#✓fully proved
For a deterministic finite automaton \(M\) over a finite alphabet with finite state set \(Q\), the subsets of \(Q\) reachable from the start state in the subset construction of the reversal of \(M\).
They are found by a reachability search of at most \(2^{|Q|}\) rounds, the number of subsets, which stops as soon as a round adds nothing.
abbrev MidState : Type _ :=
{S // S ∈ M.revDet.reachableWithin (2 ^ Fintype.card σ) ∅}Uses 2 · Used by 7
AbbreviationThe intermediate Brzozowski automaton#✓fully proved
For a deterministic finite automaton \(M\) over a finite alphabet with finitely many states, the subset construction of the reversal of \(M\), restricted to the subsets reachable from its start state.
abbrev brzozowskiMid : DFA α M.MidState :=
M.revDet.accessiblePartWithin (2 ^ Fintype.card σ) Fintype.card_finset.leUses 3 · Used by 6
AbbreviationStates of Brzozowski's automaton#✓fully proved
For a deterministic finite automaton \(M\) over a finite alphabet with finitely many states, the subsets of states of the intermediate Brzozowski automaton of \(M\) that are reachable from the start state in the subset construction of its reversal.
abbrev BrzozowskiState : Type _ :=
{S // S ∈ M.brzozowskiMid.revDet.reachableWithin (2 ^ Fintype.card M.MidState) ∅}Uses 5 · Used by 7
DefinitionBrzozowski's automaton#✓fully proved
For a deterministic finite automaton \(M\) over a finite alphabet with finitely many states, the subset construction of the reversal of the intermediate Brzozowski automaton of \(M\), restricted to the subsets reachable from its start state. Equivalently: reverse, determinize by the subset construction and keep the reachable subsets, twice.
def brzozowski : DFA α M.BrzozowskiState :=
M.brzozowskiMid.revDet.accessiblePartWithin (2 ^ Fintype.card M.MidState)
Fintype.card_finset.leUses 6 · Used by 6
TheoremEvery state of the intermediate Brzozowski automaton is reachable#✓fully proved
For a deterministic finite automaton \(M\) over a finite alphabet with finitely many states, every state of the intermediate Brzozowski automaton of \(M\) (the subset construction of the reversal of \(M\) restricted to its reachable subsets) is reached from its start state by some word.
theorem brzozowskiMid_surjective (p : M.MidState) : ∃ w, M.brzozowskiMid.eval w = pUses 4 · Used by 1
TheoremEvery state of Brzozowski's automaton is reachable#✓fully proved
For a deterministic finite automaton \(M\) over a finite alphabet with finitely many states, every state of Brzozowski's automaton of \(M\) is reached from its start state by some word.
theorem brzozowski_surjective (p : M.BrzozowskiState) : ∃ w, M.brzozowski.eval w = pUses 8 · Used by 3
TheoremBrzozowski's automaton accepts the language of the original automaton#✓fully proved
For a deterministic finite automaton \(M\) over a finite alphabet with finitely many states, Brzozowski's automaton of \(M\) accepts exactly the language of \(M\).
theorem brzozowski_accepts : M.brzozowski.accepts = M.acceptsUses 8 · Used by 1
TheoremBrzozowski's automaton identifies exactly the Nerode equivalent words#✓fully proved
For a deterministic finite automaton \(M\) over a finite alphabet with finitely many states and words \(w\) and \(w'\), Brzozowski's automaton of \(M\) reaches the same state on \(w\) as on \(w'\) if and only if \(w\) and \(w'\) are Nerode equivalent for the language of \(M\), that is, have the same left quotient.
theorem brzozowski_eval_eq_iff {w w' : List α} :
M.brzozowski.eval w = M.brzozowski.eval w' ↔ nerodeRel M.accepts w w'def nerodeRel (L : Language Symbol) (x y : List Symbol) : Prop :=
L.leftQuotient x = L.leftQuotient yCSLibExt/Computability/Languages/Congruences/Nerode.lean:56
Uses 11 · Used by 2
DefinitionResidual language of a state of Brzozowski's automaton#✓fully proved
For a deterministic finite automaton \(M\) over a finite alphabet with finitely many states, the map that sends a state \(p\) of Brzozowski's automaton of \(M\) to the language accepted by \(M\) from the state that \(M\) reaches on \(w\), where \(w\) is a chosen word leading Brzozowski's automaton from its start state to \(p\); this language is one of the residual languages of the reachable states of \(M\).
noncomputable def brzozowskiResidual (p : M.BrzozowskiState) : reachableResiduals M :=
minimizedState M (M.brzozowski_surjective p).choosedef reachableResiduals (M : DFA Symbol State) : Set (Language Symbol) :=
Set.range (M.acceptsFrom ∘ M.eval)CSLibExt/Computability/Languages/Congruences/Minimality.lean:96
def minimizedState (M : DFA Symbol State) (x : List Symbol) : reachableResiduals M :=
⟨M.acceptsFrom (M.eval x), ⟨x, rfl⟩⟩CSLibExt/Computability/Languages/Congruences/Minimization.lean:49
Uses 5 · Used by 2
DefinitionStates of Brzozowski's automaton as residual languages#✓fully proved
For a deterministic finite automaton \(M\) over a finite alphabet with finitely many states, the bijection from the states of Brzozowski's automaton of \(M\) to the residual languages of the reachable states of \(M\) that sends each state \(p\) to the language accepted by \(M\) from the state that \(M\) reaches on \(w\), where \(w\) is a chosen word leading Brzozowski's automaton from its start state to \(p\).
noncomputable def brzozowskiEquiv : M.BrzozowskiState ≃ reachableResiduals M :=
Equiv.ofBijective _ M.brzozowskiResidual_bijectivedef reachableResiduals (M : DFA Symbol State) : Set (Language Symbol) :=
Set.range (M.acceptsFrom ∘ M.eval)CSLibExt/Computability/Languages/Congruences/Minimality.lean:96
Uses 10 · Used by 1
TheoremBrzozowski's automaton is the minimal automaton#✓fully proved
Let \(M\) be a DFA over a finite alphabet with finitely many states, and let \(L\) be its language. For a language \(K\) and a word \(w\), write \(w^{-1}K = \{v \mid wv \in K\}\) for the left quotient of \(K\) by \(w\). Every state of Brzozowski's automaton of \(M\) is reached by some word \(w\); rename that state to \(w^{-1}L\), which does not depend on the choice of \(w\). The renamed automaton is exactly the minimized DFA of \(M\): its states are the left quotients of \(L\) by words, its start state is \(L\), reading a letter \(a\) (a word of length one) sends \(K\) to \(a^{-1}K\), and it accepts the \(K\) that contain the empty word.
theorem reindex_brzozowski : DFA.reindex M.brzozowskiEquiv M.brzozowski = minimizedDFA Mnoncomputable def minimizedDFA (M : DFA Symbol State) : DFA Symbol (reachableResiduals M) :=
DFA.reindex (leftQuotientEquivReachableResiduals M) M.accepts.toDFACSLibExt/Computability/Languages/Congruences/Minimization.lean:98
Uses 16
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.