Moore's algorithm

15 fully proved

State equivalence by refinement

DefinitionMoore refinement step#✓fully proved

Let \(M\) be a DFA with state set \(S\) and transition function \(\delta\). One round of Moore's refinement sends a set \(E \subseteq S \times S\) of pairs of states to the set of pairs \((p, q) \in S \times S\) such that \(p\) is accepting if and only if \(q\) is accepting and, for every letter \(a\), the pair \((\delta(p, a), \delta(q, a))\) lies in \(E\).

def mooreStep (E : Finset (σ × σ)) : Finset (σ × σ) :=
  Finset.univ.filter fun p =>
    (p.1 ∈ M.accept ↔ p.2 ∈ M.accept) ∧ ∀ a, (M.step p.1 a, M.step p.2 a) ∈ E

Used by 5

Used byCorrectness of Moore's refinement · Moore's minimal automaton · Stopping Moore iteration · Output of the stopping Moore iteration · Moore's relation contains every post-fixed point

DefinitionStopping Moore iteration#✓fully proved

Let \(M\) be a DFA over a finite alphabet with finitely many states, and write \(R\) for one round of Moore's refinement. For a set \(E\) of pairs of states of \(M\) and a budget \(n \in \mathbb{N}\), the stopping Moore iteration is defined by recursion on \(n\): with budget \(0\) it returns \(E\); with budget \(n + 1\) it returns \(E\) if \(R(E) = E\), and otherwise the stopping Moore iteration from \(R(E)\) with budget \(n\).

def mooreIter : ℕ → Finset (σ × σ) → Finset (σ × σ)
  | 0, E => E
  | n + 1, E =>
      let next := M.mooreStep E
      if next = E then E else mooreIter n next

Uses 1 · Used by 5

Statement usesMoore refinement step

Used byCorrectness of Moore's refinement · Moore's minimal automaton · Output of the stopping Moore iteration · Moore's relation · Moore's relation contains every post-fixed point

TheoremOutput of the stopping Moore iteration#✓fully proved

Let \(M\) be a DFA over a finite alphabet with finitely many states, and write \(R\) for one round of Moore's refinement. For every \(n \in \mathbb{N}\) and every set \(E\) of pairs of states of \(M\), there is \(k \le n\) such that the stopping Moore iteration from \(E\) with budget \(n\) returns \(R^k(E)\), and if \(k < n\) then \(R^k(E)\) is a fixed point of \(R\), that is, \(R(R^k(E)) = R^k(E)\).

theorem mooreIter_spec :
    ∀ (n : ℕ) (E : Finset (σ × σ)), ∃ k ≤ n, M.mooreIter n E = M.mooreStep^[k] E ∧
      (k < n → M.mooreStep (M.mooreStep^[k] E) = M.mooreStep^[k] E)

Uses 2 · Used by 3

Statement usesStopping Moore iteration · Moore refinement step

Used byCorrectness of Moore's refinement · Moore's minimal automaton · Moore's relation contains every post-fixed point

DefinitionMoore's relation#✓fully proved

For a DFA \(M\) over a finite alphabet with finite set of states \(Q\), Moore's relation is the set of pairs of states obtained from \(Q \times Q\) by repeating rounds of Moore's refinement until a round changes nothing, for at most \(|Q \times Q|\) rounds.

def mooreRel : Finset (σ × σ) :=
  M.mooreIter (Fintype.card (σ × σ)) Finset.univ

Uses 1 · Used by 7

Statement usesStopping Moore iteration

Used byHopcroft's partition is Moore's relation · Moore's automaton has one state per Nerode class · Correctness of Moore's refinement · Moore's minimal automaton · Continuation language of a Moore class · Moore equivalence on reachable states · Moore's relation contains every post-fixed point

TheoremMoore's relation contains every post-fixed point#✓fully proved

Let \(M\) be a DFA. If a set \(Z\) of pairs of states of \(M\) is contained in its image under one round of Moore's refinement, then \(Z\) is contained in Moore's relation of \(M\).

theorem subset_mooreRel {Z : Finset (σ × σ)} (hZ : Z ⊆ M.mooreStep Z) : Z ⊆ M.mooreRel

Uses 4 · Used by 1

Statement usesMoore's relation · Moore refinement step

Proof usesStopping Moore iteration · Output of the stopping Moore iteration

Used byCorrectness of Moore's refinement

TheoremCorrectness of Moore's refinement#✓fully proved

For a DFA \(M\) over a finite alphabet with finitely many states, two states \(p\) and \(q\) of \(M\) are related by Moore's relation if and only if they have the same continuation language: for every word \(w\), \(M\) started at \(p\) accepts \(w\) exactly when \(M\) started at \(q\) accepts \(w\).

theorem mem_mooreRel_iff {p q : σ} :
    (p, q) ∈ M.mooreRel ↔ M.acceptsFrom p = M.acceptsFrom q

Uses 6 · Used by 6

Statement usesMoore's relation

Proof usesStopping Moore iteration · Output of the stopping Moore iteration · Moore refinement step · Moore's relation contains every post-fixed point · Finite iteration from the whole type reaches a fixed point

Used byHopcroft's partition is Moore's relation · Moore classes are Hopcroft blocks · Moore's minimal automaton · Moore classes are the reachable residuals · Continuation language of a Moore class · Moore equivalence on reachable states

The quotient automaton

DefinitionMoore equivalence on reachable states#✓fully proved

For a DFA \(M\), two reachable states \(p\) and \(q\) of \(M\) are related when the pair \((p, q)\) lies in Moore's relation of \(M\); this relation is an equivalence relation on the reachable states of \(M\).

def mooreSetoid : Setoid {s // s ∈ M.reachable} where
  r p q := (p.1, q.1) ∈ M.mooreRel
  iseqv :=
    ⟨fun _ => M.mem_mooreRel_iff.2 rfl,
      fun h => M.mem_mooreRel_iff.2 (M.mem_mooreRel_iff.1 h).symm,
      fun h₁ h₂ => M.mem_mooreRel_iff.2 ((M.mem_mooreRel_iff.1 h₁).trans (M.mem_mooreRel_iff.1 h₂))⟩

Uses 3 · Used by 8

Statement usesCorrectness of Moore's refinement · Moore's relation · Reachable states of a DFA

Used byMoore classes are Hopcroft blocks · Moore's automaton has one state per Nerode class · Moore class of a reachable state · Moore's minimal automaton · Moore classes are the reachable residuals · Continuation language of a Moore class · States of Moore's automaton · Moore's automaton is the minimal automaton

DefinitionStates of Moore's automaton#✓fully proved

For a DFA \(M\), these are the equivalence classes of the reachable states of \(M\) under Moore equivalence, that is, under Moore's relation of \(M\) restricted to reachable states. They are the states of Moore's minimal automaton.

def MooreState : Type _ :=
  Quotient M.mooreSetoid

Uses 2 · Used by 8

Statement usesMoore equivalence on reachable states · Reachable states of a DFA

Used byMoore classes are Hopcroft blocks · Moore's automaton has one state per Nerode class · Moore class of a reachable state · Moore's minimal automaton · Moore's automaton accepts the same language · Moore classes are the reachable residuals · Continuation language of a Moore class · Moore's automaton is the minimal automaton

DefinitionMoore class of a reachable state#✓fully proved

Let \(M\) be a DFA over a finite alphabet with finitely many states. For a reachable state \(s\) of \(M\), its Moore class is the equivalence class of \(s\) among the reachable states of \(M\) under Moore's relation; it is a state of Moore's minimal automaton of \(M\).

def mooreClass (s : {s // s ∈ M.reachable}) : M.MooreState :=
  Quotient.mk M.mooreSetoid s

Uses 3 · Used by 5

Statement usesStates of Moore's automaton · Moore equivalence on reachable states · Reachable states of a DFA

Used byMoore classes are Hopcroft blocks · Moore's minimal automaton · Moore's automaton accepts the same language · Moore classes are the reachable residuals · Moore's automaton is the minimal automaton

DefinitionMoore's minimal automaton#✓fully proved

For a DFA \(M\) over a finite alphabet with finitely many states, Moore's minimal automaton of \(M\) has as states the classes of reachable states of \(M\) under Moore's relation. Its start state is the class of the start state of \(M\); reading a letter \(a\) sends the class of a reachable state \(s\) to the class of the state that \(M\) reaches from \(s\) on \(a\); and the class of \(s\) is accepting exactly when \(s\) is an accepting state of \(M\).

These do not depend on the chosen member \(s\), because Moore-related states agree on acceptance and their successors on each letter are again Moore-related.

def mooreDFA : DFA α M.MooreState where
  step c a := Quotient.lift (fun p => M.mooreClass ⟨M.step p.1 a, M.step_mem_reachable p.2 a⟩)
    (fun _ _ h => (M.mooreClass_eq_iff).2
      (M.mem_mooreRel_iff.1 (((M.mem_mooreRel_unfold).1 h).2 a))) c
  start := M.mooreClass ⟨M.start, M.start_mem_reachable⟩
  accept := {c | Quotient.lift (fun p : {s // s ∈ M.reachable} => decide (p.1 ∈ M.accept))
    (fun _ _ h => decide_eq_decide.2 ((M.mem_mooreRel_unfold).1 h).1) c = true}

Uses 12 · Used by 2

Statement usesStates of Moore's automaton · Correctness of Moore's refinement · Moore class of a reachable state · Stopping Moore iteration · Output of the stopping Moore iteration · Moore's relation · Moore equivalence on reachable states · Moore refinement step · Reachable states of a DFA · The start state is reachable · Reachable states are closed under transitions · Finite iteration from the whole type reaches a fixed point

Used byMoore's automaton accepts the same language · Moore's automaton is the minimal automaton

TheoremMoore's automaton accepts the same language#✓fully proved

For a DFA \(M\) over a finite alphabet with finitely many states, Moore's minimal automaton of \(M\) accepts exactly the language accepted by \(M\).

theorem mooreDFA_accepts : M.mooreDFA.accepts = M.accepts

Uses 6

Statement usesStates of Moore's automaton · Moore's minimal automaton

Proof usesA state is reachable exactly when some word leads to it · Moore class of a reachable state · Reachable states of a DFA · Reachable states are closed under transitions

Agreement with the semantic minimal automaton

DefinitionContinuation language of a Moore class#✓fully proved

Let \(M\) be a DFA over a finite alphabet with finitely many states. Each state of Moore's minimal automaton of \(M\), a class of reachable states of \(M\), is sent to the continuation language of any member \(s\), the set of words that \(M\) accepts when started at \(s\); this is a reachable residual language of \(M\). It does not depend on the choice of \(s\), because Moore-related states have the same continuation language.

def mooreResidual (c : M.MooreState) : reachableResiduals M :=
  Quotient.lift (fun p : {s // s ∈ M.reachable} => (⟨M.acceptsFrom p.1, by
      obtain ⟨w, hw⟩ := M.mem_reachable_iff.1 p.2
      exact ⟨w, by simp [hw]⟩⟩ : reachableResiduals M))
    (fun _ _ h => Subtype.ext (M.mem_mooreRel_iff.1 h)) c

Uses 7 · Used by 1

Statement usesResidual languages of reachable states · States of Moore's automaton · Correctness of Moore's refinement · A state is reachable exactly when some word leads to it · Moore's relation · Moore equivalence on reachable states · Reachable states of a DFA

Used byMoore classes are the reachable residuals

DefinitionMoore classes are the reachable residuals#✓fully proved

Let \(M\) be a DFA over a finite alphabet with finitely many states. The states of Moore's minimal automaton of \(M\) are in bijection with the reachable residual languages of \(M\): the bijection sends the class of a reachable state \(s\) to the continuation language of \(s\), the set of words that \(M\) accepts when started at \(s\).

noncomputable def mooreEquiv : M.MooreState ≃ reachableResiduals M :=
  Equiv.ofBijective _ M.mooreResidual_bijective

Uses 8 · Used by 2

Statement usesResidual languages of reachable states · States of Moore's automaton · Correctness of Moore's refinement · A state is reachable exactly when some word leads to it · Moore class of a reachable state · Continuation language of a Moore class · Moore equivalence on reachable states · Reachable states of a DFA

Used byMoore's automaton has one state per Nerode class · Moore's automaton is the minimal automaton

TheoremMoore's automaton is the minimal automaton#✓fully proved

Let \(M\) be a DFA. Renaming each state of Moore's minimal automaton of \(M\), a class of reachable states, to the continuation language accepted from its members turns Moore's automaton into exactly the minimized DFA of \(M\), whose states are the reachable continuation languages of \(M\).

theorem reindex_mooreDFA : DFA.reindex M.mooreEquiv M.mooreDFA = minimizedDFA M

Uses 14

Statement usesMinimized DFA · Residual languages of reachable states · States of Moore's automaton · Moore's minimal automaton · Moore classes are the reachable residuals

Proof usesLeft quotients as reachable residuals · Left quotients of continuation languages · States reached in the minimized DFA · Transitions of the minimized DFA · Residual reached by a word · Moore class of a reachable state · Moore equivalence on reachable states · Reachable states of a DFA · Reachable states are closed under transitions

TheoremMoore's automaton has one state per Nerode class#✓fully proved

For a DFA \(M\) over a finite alphabet with finitely many states, Moore's minimal automaton of \(M\) has exactly as many states as there are Nerode classes of the language accepted by \(M\).

theorem card_mooreState [Fintype (NerodeClass M.accepts)] :
    Fintype.card M.MooreState = Fintype.card (NerodeClass M.accepts)

Uses 8

Statement usesNerode classes · States of Moore's automaton · Moore's relation · Moore equivalence on reachable states · Reachable states of a DFA

Proof usesNerode classes and reachable residuals · Residual languages of reachable states · Moore classes are the reachable residuals

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.