Skip to content

Decision procedures for finite automata

DefinitionSymmetric difference of two DFAs#✓fully proved

For DFAs \(M\) and \(N\) over the same alphabet, with sets of states \(\sigma\) and \(\sigma'\), this is the product DFA with set of states \(\sigma \times \sigma'\) whose start state is the pair of the start states of \(M\) and \(N\), whose transition takes \((p, q)\) on a letter \(a\) to the pair of the state to which \(M\) moves from \(p\) on \(a\) and the state to which \(N\) moves from \(q\) on \(a\), and whose accepting states are the pairs \((p, q)\) such that \(p\) is an accepting state of \(M\) or \(q\) is an accepting state of \(N\), but not both.

It accepts exactly the words on which \(M\) and \(N\) disagree.

def symmDiff : DFA α (σ × σ') where
  step p a := (M.step p.1 a, N.step p.2 a)
  start := (M.start, N.start)
  accept := {p | ¬ (p.1 ∈ M.accept ↔ p.2 ∈ N.accept)}
Used by 3
Used byEquivalence test for DFAs · Correctness of the equivalence test for DFAs · Short distinguishing words

DefinitionOne round of the DFA reachability search#✓fully proved

Let \(M\) be a DFA over a finite alphabet \(\alpha\). The round sends a finite set \(S\) of states of \(M\) to the set consisting of the start state of \(M\) and of every state that the transition function of \(M\) takes some \(s \in S\) to on some letter \(a \in \alpha\).

def reachStep (S : Finset σ) : Finset σ :=
  {M.start} ∪ S.biUnion fun s => Finset.univ.image (M.step s)
Used by 4
Used byA state is reachable exactly when some word leads to it · Reachable states of a DFA · Early-stopping DFA reachability search · The early-stopping search finds exactly the reachable states

DefinitionReachable states of a DFA#✓fully proved

Let \(M\) be a DFA over a finite alphabet whose set of states \(\sigma\) is finite and has decidable equality. The reachable states of \(M\) form the finite set obtained from the empty set by applying one round of the DFA reachability search for \(M\) exactly \(|\sigma|\) times, where \(|\sigma|\) is the number of states of \(M\).

Since the round is monotone, this set is its least fixed point, and a state lies in it exactly when \(M\) reaches it from its start state on some word.

def reachable : Finset σ :=
  Finset.lfpFin M.reachStep
Uses 2 · Used by 18
Statement usesOne round of the DFA reachability search · Least fixed point of a finset map by finite iteration
Used byAccessible part of a DFA, by a bounded search · Every state of the accessible part is reached · Emptiness test for DFAs · The emptiness test decides emptiness of DFAs · A state is reachable exactly when some word leads to it · The early-stopping search finds exactly the reachable states · The start state is reachable · Reachable states are closed under transitions · Moore 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 equivalence on reachable states · States of Moore's automaton · Moore's automaton is the minimal automaton

TheoremA state is reachable exactly when some word leads to it#✓fully proved

Let \(M\) be a DFA over a finite alphabet with finitely many states. A state \(s\) of \(M\) is in the set of reachable states of \(M\) if and only if there is a word \(w\) such that running \(M\) on \(w\) from its start state ends in \(s\).

theorem mem_reachable_iff {s : σ} : s ∈ M.reachable ↔ ∃ w, M.eval w = s
Uses 5 · Used by 8
Statement usesReachable states of a DFA
Proof usesOne round of the DFA reachability search · Least fixed point of a finset map by finite iteration · Finite iteration from the empty set reaches a fixed point · The finite least fixed point lies in every pre-fixed point
Used byAccessible part of a DFA, by a bounded search · Every state of the accessible part is reached · The emptiness test decides emptiness of DFAs · The start state is reachable · Reachable states are closed under transitions · Moore's automaton accepts the same language · Moore classes are the reachable residuals · Continuation language of a Moore class

TheoremThe start state is reachable#✓fully proved

For a DFA \(M\) over a finite alphabet with finitely many states, the start state of \(M\) belongs to the reachable states of \(M\).

theorem start_mem_reachable : M.start ∈ M.reachable
Uses 2 · Used by 1
Statement usesReachable states of a DFA
Proof usesA state is reachable exactly when some word leads to it
Used byMoore's minimal automaton

TheoremReachable states are closed under transitions#✓fully proved

Let \(M\) be a DFA over a finite alphabet whose set of states is finite and has decidable equality. If a state \(s\) of \(M\) is reachable from the start state, then for every letter \(a\) the state to which \(M\) moves from \(s\) on \(a\) is also reachable from the start state.

theorem step_mem_reachable {s : σ} (hs : s ∈ M.reachable) (a : α) :
    M.step s a ∈ M.reachable
Uses 2 · Used by 3
Statement usesReachable states of a DFA
Proof usesA state is reachable exactly when some word leads to it
Used byMoore's minimal automaton · Moore's automaton accepts the same language · Moore's automaton is the minimal automaton

DefinitionEarly-stopping DFA reachability search#✓fully proved

Let \(M\) be a DFA over a finite alphabet whose set of states has decidable equality. For a natural number \(n\) and a finite set \(S\) of states of \(M\), the reachability search from \(S\) with at most \(n\) rounds returns \(S\) when \(n = 0\). When \(n = k + 1\), it returns \(S\) if one round of the reachability search for \(M\) sends \(S\) to \(S\) itself, and otherwise it returns the search from the image of \(S\) under that round with at most \(k\) rounds.

def reachableWithin : ℕ → Finset σ → Finset σ
  | 0, S => S
  | n + 1, S => if M.reachStep S = S then S else reachableWithin n (M.reachStep S)
Uses 1 · Used by 10
Statement usesOne round of the DFA reachability search
Used byAccessible part of a DFA · Accessible part of a DFA, by a bounded search · Every state of the accessible part is reached · The early-stopping search finds exactly the reachable states · Brzozowski's automaton · Brzozowski's automaton accepts the language of the original automaton · Brzozowski's automaton identifies exactly the Nerode equivalent words · States of Brzozowski's automaton · Every state of Brzozowski's automaton is reachable · States of the intermediate Brzozowski automaton

TheoremThe early-stopping search finds exactly the reachable states#✓fully proved

Let \(M\) be a DFA over a finite alphabet with finitely many states. For every natural number \(n\) at least the number of states of \(M\), the early-stopping reachability search for \(M\) from the empty set with at most \(n\) rounds returns the set of reachable states of \(M\).

Since the search stops once a round changes nothing, a generous bound costs nothing.

theorem reachableWithin_eq_reachable {n : ℕ} (hn : Fintype.card σ ≤ n) :
    M.reachableWithin n ∅ = M.reachable
Uses 5 · Used by 2
Statement usesReachable states of a DFA · Early-stopping DFA reachability search
Proof usesOne round of the DFA reachability search · Least fixed point of a finset map by finite iteration · Finite iteration from the empty set reaches a fixed point
Used byAccessible part of a DFA, by a bounded search · Every state of the accessible part is reached

DefinitionAccessible part of a DFA, by a bounded search#✓fully proved

Let \(M\) be a DFA over a finite alphabet \(\alpha\) with a finite state set \(\sigma\) with decidable equality, and let \(n \ge |\sigma|\). The accessible part of \(M\) found with \(n\) rounds is the DFA over \(\alpha\) whose states are the states found by the reachability search from the empty set with at most \(n\) rounds, whose start state is the start state of \(M\), whose transition function is that of \(M\) restricted to these states, and whose accepting states are those of them that \(M\) accepts.

Since \(n \ge |\sigma|\), the search finds exactly the states that some word leads to from the start state of \(M\), and it stops as soon as a round adds nothing, so a larger bound costs nothing.

def accessiblePartWithin (n : ℕ) (hn : Fintype.card σ ≤ n) :
    DFA α {s // s ∈ M.reachableWithin n ∅} where
  step p a := ⟨M.step p.1 a, (M.mem_reachableWithin_iff hn).2 <| by
    obtain ⟨w, hw⟩ := (M.mem_reachableWithin_iff hn).1 p.2
    exact ⟨w ++ [a], by rw [eval_append_singleton, hw]⟩⟩
  start := ⟨M.start, (M.mem_reachableWithin_iff hn).2 ⟨[], rfl⟩⟩
  accept := {p | p.1 ∈ M.accept}
Uses 4 · Used by 8
Statement usesA state is reachable exactly when some word leads to it · Reachable states of a DFA · Early-stopping DFA reachability search · The early-stopping search finds exactly the reachable states
Used byAccessible part of a DFA · Every state of the accessible part is reached · Brzozowski's automaton · Brzozowski's automaton accepts the language of the original automaton · Brzozowski's automaton identifies exactly the Nerode equivalent words · The intermediate Brzozowski automaton · States of Brzozowski's automaton · Every state of Brzozowski's automaton is reachable

AbbreviationAccessible part of a DFA#✓fully proved

Let \(M\) be a DFA over a finite alphabet \(\alpha\) with a finite state set \(\sigma\) with decidable equality. The accessible part of \(M\) is its accessible part found by the reachability search with \(|\sigma|\) rounds: the DFA over \(\alpha\) whose states are the states found by the reachability search from the empty set with at most \(|\sigma|\) rounds (exactly the states that some word leads to from the start state of \(M\)), whose start state is the start state of \(M\), whose transition function is that of \(M\) restricted to these states, and whose accepting states are those of them that \(M\) accepts.

abbrev accessiblePart : DFA α {s // s ∈ M.reachableWithin (Fintype.card σ) ∅} :=
  M.accessiblePartWithin (Fintype.card σ) le_rfl
Uses 2
Statement usesAccessible part of a DFA, by a bounded search · Early-stopping DFA reachability search

TheoremEvery state of the accessible part is reached#✓fully proved

Let \(M\) be a DFA over a finite alphabet \(\alpha\) with a finite state set \(\sigma\) with decidable equality, and let \(n \ge |\sigma|\). For every state \(p\) of the accessible part of \(M\) found with \(n\) rounds, some word \(w\) leads the accessible part from its start state to \(p\).

theorem accessiblePartWithin_surjective (p : {s // s ∈ M.reachableWithin n ∅}) :
    ∃ w, (M.accessiblePartWithin n hn).eval w = p
Uses 5 · Used by 2
Statement usesAccessible part of a DFA, by a bounded search · Early-stopping DFA reachability search
Proof usesA state is reachable exactly when some word leads to it · Reachable states of a DFA · The early-stopping search finds exactly the reachable states
Used byEvery state of the intermediate Brzozowski automaton is reachable · Every state of Brzozowski's automaton is reachable

DefinitionEmptiness test for DFAs#✓fully proved

For a DFA \(M\) over a finite alphabet with finitely many states, the emptiness test returns true exactly when none of the reachable states of \(M\) is an accepting state.

def isEmptyB : Bool :=
  decide (∀ s ∈ M.reachable, s ∉ M.accept)
Uses 1 · Used by 5
Statement usesReachable states of a DFA
Used byEquivalence test for DFAs · Correctness of the equivalence test for DFAs · The emptiness test decides emptiness of DFAs · Universality test for DFAs · The universality test decides universality of DFAs

TheoremThe emptiness test decides emptiness of DFAs#✓fully proved

Let \(M\) be a DFA over a finite alphabet with finitely many states. The emptiness test applied to \(M\) returns true if and only if the language accepted by \(M\) is empty.

theorem isEmptyB_iff : M.isEmptyB = true ↔ M.accepts = 0
Uses 3 · Used by 2
Statement usesEmptiness test for DFAs
Proof usesA state is reachable exactly when some word leads to it · Reachable states of a DFA
Used byCorrectness of the equivalence test for DFAs · The universality test decides universality of DFAs

DefinitionUniversality test for DFAs#✓fully proved

For a DFA \(M\) over a finite alphabet with finitely many states, the universality test applied to \(M\) is the emptiness test applied to the complement of \(M\): the DFA with the same states, start state and transitions whose accepting states are the states that \(M\) does not accept.

def isUnivB : Bool :=
  Mᶜ.isEmptyB
Uses 1 · Used by 1
Statement usesEmptiness test for DFAs
Used byThe universality test decides universality of DFAs

TheoremThe universality test decides universality of DFAs#✓fully proved

Let \(M\) be a DFA over a finite alphabet with finitely many states. The universality test applied to \(M\) returns true if and only if \(M\) accepts every word over the alphabet.

theorem isUnivB_iff : M.isUnivB = true ↔ M.accepts = ⊤
Uses 3
Statement usesUniversality test for DFAs
Proof usesEmptiness test for DFAs · The emptiness test decides emptiness of DFAs

DefinitionEquivalence test for DFAs#✓fully proved

Let \(M\) and \(N\) be DFAs over the same finite alphabet, with finite state sets with decidable equality and decidable sets of accepting states. Their symmetric difference is the product DFA on pairs of states that starts at the pair of start states, moves on a letter by moving both components, and accepts a pair \((p, q)\) when exactly one of the statements "\(M\) accepts \(p\)" and "\(N\) accepts \(q\)" holds. The equivalence test of \(M\) and \(N\) is the emptiness test of their symmetric difference: the Boolean that is true exactly when no pair of states reachable from the start pair is accepting.

def equivB : Bool :=
  (M.symmDiff N).isEmptyB
Uses 2 · Used by 1
Statement usesEmptiness test for DFAs · Symmetric difference of two DFAs
Used byCorrectness of the equivalence test for DFAs

TheoremCorrectness of the equivalence test for DFAs#✓fully proved

Let \(M\) and \(N\) be DFAs over the same finite alphabet, with finite state sets with decidable equality and decidable sets of accepting states. The equivalence test of \(M\) and \(N\) returns true if and only if \(M\) and \(N\) accept the same language.

theorem equivB_iff : M.equivB N = true ↔ M.accepts = N.accepts
Uses 4
Statement usesEquivalence test for DFAs
Proof usesEmptiness test for DFAs · The emptiness test decides emptiness of DFAs · Symmetric difference of two DFAs
39 fully proved

Acceptance

DefinitionAcceptance test for encoded DFAs#✓fully proved

For an encoded DFA \(D\) over an alphabet \(\alpha\) with decidable equality and a word \(w\) over \(\alpha\), the acceptance test is the Boolean that is true exactly when the state reached by running \(D\) on \(w\) from its start state is in the list of accepting states of \(D\).

def acceptsB (D : EncodedDFA α) (w : List α) : Bool :=
  memB D.accept (D.toDFA.eval w)
Uses 3 · Used by 5
Statement usesEncoded DFA · The automaton denoted by an encoded DFA · Boolean membership test for lists of natural numbers
Used byInfiniteness test for encoded DFAs · Correctness of the infiniteness test for encoded DFAs · Equivalence of DFAs is decidable · Infiniteness of DFAs is decidable · Acceptance for DFAs is decidable

Reachability

DefinitionOne round of the list reachability search#✓fully proved

Let \(s_0 \in \mathbb{N}\), let \(\mathrm{next}\) assign to each \(s \in \mathbb{N}\) a list \(\mathrm{next}(s)\) of natural numbers, and let \(B\) and \(R\) be lists of natural numbers. The round from \(s_0\) with successors \(\mathrm{next}\) kept inside \(B\) sends the list \(R\) of states found so far to the following list: write \(s_0\) followed, for each \(s\) in \(R\) in order, by \(s\) and then the list \(\mathrm{next}(s)\); keep the entries that lie in \(B\); then delete every entry that occurs again later in the list.

Its entries are therefore the numbers in \(B\) that are \(s_0\), an element \(s\) of \(R\), or an element of \(\mathrm{next}(s)\) for some \(s\) in \(R\), each listed once.

def reachRound (s₀ : ℕ) (next : ℕ → List ℕ) (B R : List ℕ) : List ℕ :=
  dedupB ((s₀ :: R.flatMap fun s => s :: next s).filterMap fun t =>
    cond (memB B t) (some t) none)
Uses 2 · Used by 7
Statement usesDuplicate removal for lists of natural numbers · Boolean membership test for lists of natural numbers
Used byCorrectness of the bounded reachability search · Bounded reachability search on lists of states · Equivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable · Emptiness of NFAs is decidable · Membership for NFAs is decidable

DefinitionBounded reachability search on lists of states#✓fully proved

Let \(s_0 \in \mathbb{N}\), let \(\mathrm{next}\) assign to each \(s \in \mathbb{N}\) a list \(\mathrm{next}(s)\) of natural numbers, and let \(B\) be a list of natural numbers. One search round sends a list \(R\) to the list obtained by writing \(s_0\) followed, for each \(s\) in \(R\) in order, by \(s\) and then the list \(\mathrm{next}(s)\), keeping the entries that lie in \(B\), and deleting every entry that occurs again later; its entries are the elements of \(B\) that are \(s_0\), an element of \(R\), or an element of \(\mathrm{next}(s)\) for some \(s\) in \(R\), each listed once. The search returns the result of applying this round \(|B|\) times to the empty list, where \(|B|\) is the length of \(B\).

When \(B\) contains \(s_0\) and is closed under \(\mathrm{next}\), a number is an entry of the returned list exactly when it is reachable from \(s_0\) by finitely many, possibly zero, steps from some \(s\) to an element of \(\mathrm{next}(s)\).

def reachN (s₀ : ℕ) (next : ℕ → List ℕ) (B : List ℕ) : List ℕ :=
  (reachRound s₀ next B)^[B.length] []
Uses 1 · Used by 12
Statement usesOne round of the list reachability search
Used byCorrectness of the bounded reachability search · Reachable pairs of states of two encoded DFAs · Reachable states of an encoded DFA · Equivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable · ε-closure of a list of states · The reachable states are those some word can lead to · The run of an encoded NFA agrees with ε-NFA evaluation · Reachable states of an encoded NFA · Emptiness of NFAs is decidable · Membership for NFAs is decidable

TheoremCorrectness of the bounded reachability search#✓fully proved

Let \(s_0 \in \mathbb{N}\), let \(\mathrm{next}\) assign to every natural number a list of natural numbers, its successors, and let \(B\) be a list of natural numbers that contains \(s_0\) and is closed under successors: whenever \(s\) is in \(B\) and \(t\) is a successor of \(s\), then \(t\) is in \(B\). Then a natural number \(t\) is in the list computed by the reachability search from \(s_0\) through \(\mathrm{next}\) within \(B\) if and only if \(t\) is reachable from \(s_0\) in zero or more successor steps.

theorem mem_reachN_iff {s₀ : ℕ} {next : ℕ → List ℕ} {B : List ℕ} (hs₀ : s₀ ∈ B)
    (hB : ∀ s ∈ B, ∀ t ∈ next s, t ∈ B) {t : ℕ} :
    t ∈ reachN s₀ next B ↔ Relation.ReflTransGen (fun s t => t ∈ next s) s₀ t
Uses 5 · Used by 5
Statement usesBounded reachability search on lists of states
Proof usesOne round of the list reachability search · Duplicate removal for lists of natural numbers · Bounded monotone rounds on lists close off · Boolean membership test for lists of natural numbers
Used byEquivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable · The reachable states are those some word can lead to · The run of an encoded NFA agrees with ε-NFA evaluation

DefinitionReachable states of an encoded DFA#✓fully proved

For an encoded DFA \(D\) over an alphabet \(\alpha\) with decidable equality, the reachable states of \(D\) form the list returned by the bounded reachability search on lists of states started at the start state of \(D\), kept inside the states of \(D\), in which the successors of a state \(s\) are the states that the transition function of \(D\) takes \(s\) to on the letters of \(D\), in the order of the letters.

A natural number lies in this list exactly when the automaton denoted by \(D\) reaches it from its start state on some word.

def reachable (D : EncodedDFA α) : List ℕ :=
  reachN D.start (fun s => D.letters.map (D.step s)) D.states
Uses 5 · Used by 4
Statement usesEncoded DFA · Letters of an encoded DFA · Bounded reachability search on lists of states · States of an encoded DFA · Transition function of an encoded DFA
Used byEmptiness test for encoded DFAs · Universality test for encoded DFAs · Universality of DFAs is decidable · Emptiness of DFAs is decidable

Emptiness

DefinitionEmptiness test for encoded DFAs#✓fully proved

For an encoded DFA \(D\) over an alphabet \(\alpha\) with decidable equality, the emptiness test is the Boolean that is true exactly when no entry of the list of reachable states of \(D\) is in the accepting list of \(D\).

It returns true exactly when the language of \(D\) is empty.

def isEmptyB (D : EncodedDFA α) : Bool :=
  D.reachable.all fun s => !memB D.accept s
Uses 3 · Used by 1
Statement usesEncoded DFA · Reachable states of an encoded DFA · Boolean membership test for lists of natural numbers
Used byEmptiness of DFAs is decidable

Equivalence

DefinitionCoded pairs of states of two encoded DFAs#✓fully proved

For encoded DFAs \(D\) and \(E\) over the same alphabet, code a pair \((s, t)\) of natural numbers by its image \(\langle s, t \rangle \in \mathbb{N}\) under Mathlib's pairing function. This is the list of the numbers \(\langle s, t \rangle\) with \(s\) running over the states of \(D\) in their listed order and, for each \(s\), \(t\) running over the states of \(E\) in their listed order.

def pairStates (D E : EncodedDFA α) : List ℕ :=
  D.states.flatMap fun s => E.states.map fun t => Nat.pair s t
Uses 2 · Used by 2
Statement usesEncoded DFA · States of an encoded DFA
Used byReachable pairs of states of two encoded DFAs · Equivalence of DFAs is decidable

DefinitionSuccessors of a pair of states#✓fully proved

Let \(D\) and \(E\) be encoded DFAs over the same alphabet, and let \(p \in \mathbb{N}\) code the pair of states \((s, t)\) under the pairing bijection \(\mathbb{N} \times \mathbb{N} \to \mathbb{N}\). The successors of \(p\) form the list that has, for each letter \(a\) in the letters of \(D\) followed by the letters of \(E\), the code of the pair made of the step of \(D\) from \(s\) on \(a\) and the step of \(E\) from \(t\) on \(a\).

def pairNext (D E : EncodedDFA α) (p : ℕ) : List ℕ :=
  (D.letters ++ E.letters).map fun a => Nat.pair (D.step p.unpair.1 a) (E.step p.unpair.2 a)
Uses 3 · Used by 2
Statement usesEncoded DFA · Letters of an encoded DFA · Transition function of an encoded DFA
Used byReachable pairs of states of two encoded DFAs · Equivalence of DFAs is decidable

DefinitionReachable pairs of states of two encoded DFAs#✓fully proved

For encoded DFAs \(D\) and \(E\) over the same alphabet, code a pair \((s, t)\) of natural numbers by its image \(\langle s, t \rangle \in \mathbb{N}\) under Mathlib's pairing function. The reachable pairs of \(D\) and \(E\) form the list returned by the bounded reachability search on lists of states started at \(\langle s_D, s_E \rangle\), where \(s_D\) and \(s_E\) are the start states of \(D\) and \(E\), kept inside the list of coded pairs of states of \(D\) and \(E\), and in which the successors of a number \(p = \langle s, t \rangle\) are the numbers \(\langle s', t' \rangle\) with \(s'\) and \(t'\) the states that the transition functions of \(D\) and \(E\) take \(s\) and \(t\) to on the same letter \(a\), for \(a\) running over the letters of \(D\) followed by the letters of \(E\).

A number lies in this list exactly when it is \(\langle q, r \rangle\) for the states \(q\) and \(r\) that \(D\) and \(E\) reach on some common word.

def pairReachable (D E : EncodedDFA α) : List ℕ :=
  reachN (Nat.pair D.start E.start) (pairNext D E) (pairStates D E)
Uses 4 · Used by 2
Statement usesEncoded DFA · Successors of a pair of states · Coded pairs of states of two encoded DFAs · Bounded reachability search on lists of states
Used byEquivalence test for encoded DFAs · Equivalence of DFAs is decidable

DefinitionEquivalence test for encoded DFAs#✓fully proved

Let \(D\) and \(E\) be encoded DFAs over an alphabet \(\alpha\) with decidable equality. The equivalence test of \(D\) and \(E\) is the Boolean that is true exactly when, for every entry \(p\) of the list of reachable pairs of states of \(D\) and \(E\), writing \(p = \langle s, t \rangle\) with Mathlib's pairing function, \(s\) is in the accepting list of \(D\) if and only if \(t\) is in the accepting list of \(E\).

It returns true exactly when \(D\) and \(E\) have the same language.

def equivB (D E : EncodedDFA α) : Bool :=
  (pairReachable D E).all fun p => memB D.accept p.unpair.1 == memB E.accept p.unpair.2
Uses 3 · Used by 1
Statement usesEncoded DFA · Reachable pairs of states of two encoded DFAs · Boolean membership test for lists of natural numbers
Used byEquivalence of DFAs is decidable

Universality

DefinitionUniversality test for encoded DFAs#✓fully proved

For an encoded DFA \(D\) over an alphabet \(\alpha\) with decidable equality, the universality test is the Boolean that is true exactly when every entry of the list of reachable states of \(D\) is in the accepting list of \(D\).

It returns true exactly when the language of \(D\) contains every word over \(\alpha\).

def isUnivB (D : EncodedDFA α) : Bool :=
  D.reachable.all fun s => memB D.accept s
Uses 3 · Used by 1
Statement usesEncoded DFA · Reachable states of an encoded DFA · Boolean membership test for lists of natural numbers
Used byUniversality of DFAs is decidable

Infiniteness

DefinitionAn encoded DFA on its listed states#✓fully proved

For an encoded DFA \(D\), this is the DFA whose set of states is the finite set of states of \(D\) (its start state and the targets of its listed transitions), whose start state is the start state of \(D\), whose transition function is that of \(D\) restricted to these states, and whose accepting states are those in the accepting list of \(D\).

def toFinDFA (D : EncodedDFA α) : DFA α {s // s ∈ D.states.toFinset} where
  step s a := ⟨D.step s.1 a, List.mem_toFinset.2 (step_mem_states (List.mem_toFinset.1 s.2) a)⟩
  start := ⟨D.start, List.mem_toFinset.2 List.mem_cons_self⟩
  accept := {s | s.1 ∈ D.accept}
Uses 4 · Used by 2
Statement usesEncoded DFA · States of an encoded DFA · Transition function of an encoded DFA · The listed states are closed under transitions
Used byAccepted words of length between the number of listed states and twice it · A long accepted word makes the language of an encoded DFA infinite

TheoremA long accepted word makes the language of an encoded DFA infinite#✓fully proved

Let \(D\) be an encoded DFA and let \(N\) be the length of the list of states of \(D\). If \(D\) accepts a word of length at least \(N\), then the language of \(D\) is infinite.

The proof pumps the word, using the pumping lemma for DFAs.

theorem infinite_of_mem_of_le {D : EncodedDFA α} {w : List α} (hw : w ∈ D.language)
    (hlen : D.states.length ≤ w.length) : D.language.Infinite
Uses 5 · Used by 1
Statement usesEncoded DFA · Language of an encoded DFA · States of an encoded DFA
Proof usesThe automaton denoted by an encoded DFA · An encoded DFA on its listed states
Used byCorrectness of the infiniteness test for encoded DFAs

TheoremAccepted words of length between the number of listed states and twice it#✓fully proved

Let \(D\) be an encoded DFA over an alphabet \(\alpha\) with decidable equality, and let \(N\) be the length of its list of states. For every natural number \(n\) and every word \(w\) of length \(n\) in the language of \(D\) with \(N \le n\), the language of \(D\) contains a word \(v\) whose length \(|v|\) satisfies \(N \le |v| < 2N\).

theorem exists_mem_le_lt {D : EncodedDFA α} :
    ∀ (n : ℕ) (w : List α), w.length = n → w ∈ D.language → D.states.length ≤ w.length →
      ∃ v ∈ D.language, D.states.length ≤ v.length ∧ v.length < 2 * D.states.length
Uses 5 · Used by 1
Statement usesEncoded DFA · Language of an encoded DFA · States of an encoded DFA
Proof usesThe automaton denoted by an encoded DFA · An encoded DFA on its listed states
Used byCorrectness of the infiniteness test for encoded DFAs

DefinitionWords of a given length#✓fully proved

For a finite alphabet \(\alpha\) given with an enumeration of its letters and for \(n \in \mathbb{N}\), the list of the words of length \(n\) over \(\alpha\): starting from the list whose only entry is the empty word, it replaces \(n\) times each word \(w\) of the current list by the words \(a w\) for the letters \(a\) of \(\alpha\), in their enumeration order.

def wordsOfLength (n : ℕ) : List (List α) :=
  (fun W => W.flatMap fun w => (FinEnum.toList α).map fun a => a :: w)^[n] [[]]
Used by 6
Used byInfiniteness test for encoded DFAs · Correctness of the infiniteness test for encoded DFAs · Infiniteness of DFAs is decidable · Equivalence test · The equivalence test is correct · The equivalence test is primitive recursive

DefinitionInfiniteness test for encoded DFAs#✓fully proved

Let \(D\) be an encoded DFA over a finite alphabet and let \(N\) be the length of its list of states. The infiniteness test is the Boolean that is true exactly when the language of \(D\) contains a word \(w\) with \(N \le |w| < 2N\); it checks every word of each length \(N + i\) with \(0 \le i < N\).

def infiniteB (D : EncodedDFA α) : Bool :=
  (List.range D.states.length).any fun i =>
    (wordsOfLength (D.states.length + i)).any fun w => D.acceptsB w
Uses 4 · Used by 2
Statement usesEncoded DFA · Acceptance test for encoded DFAs · States of an encoded DFA · Words of a given length
Used byCorrectness of the infiniteness test for encoded DFAs · Infiniteness of DFAs is decidable

TheoremCorrectness of the infiniteness test for encoded DFAs#✓fully proved

For every encoded DFA \(D\) over a finite alphabet, the infiniteness test returns true on \(D\) if and only if the language of \(D\) is infinite.

theorem infiniteB_iff {D : EncodedDFA α} : D.infiniteB = true ↔ D.language.Infinite
Uses 10 · Used by 1
Statement usesEncoded DFA · Infiniteness test for encoded DFAs · Language of an encoded DFA
Proof usesAcceptance test for encoded DFAs · Accepted words of length between the number of listed states and twice it · A long accepted word makes the language of an encoded DFA infinite · States of an encoded DFA · The automaton denoted by an encoded DFA · Words of a given length · Boolean membership test for lists of natural numbers
Used byInfiniteness of DFAs is decidable

Computability: Sipser's Theorems 4.1, 4.4 and 4.5

TheoremAcceptance for DFAs is decidable#✓fully proved

For every alphabet \(\alpha\) with decidable equality and a primitive recursive encoding, the property of a pair \((D, w)\) of an encoded DFA \(D\) over \(\alpha\) and a word \(w\) over \(\alpha\) that \(w\) belongs to the language of \(D\) is decidable by a multi-stack machine. This is the problem \(A_{\mathrm{DFA}}\).

theorem tm2Decidable_mem_language :
    TM2Decidable fun p : EncodedDFA α × List α => p.2 ∈ p.1.language
Sources
  • Sipser, Introduction to the Theory of Computation, Theorem 4.1.
Uses 10
Statement usesEncoded DFA · Encoded DFAs as triples · Language of an encoded DFA · Decidability by multi-stack machines
Proof usesAcceptance test for encoded DFAs · Running an encoded DFA is primitive recursive · The automaton denoted by an encoded DFA · Predicates with a primitive recursive decision procedure are computable · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates

TheoremEmptiness of DFAs is decidable#✓fully proved

For every alphabet \(\alpha\) with decidable equality and a primitive recursive encoding, the property of an encoded DFA over \(\alpha\) that its language is empty is decidable by a multi-stack machine. This is the problem \(E_{\mathrm{DFA}}\).

theorem tm2Decidable_language_eq_zero : TM2Decidable fun D : EncodedDFA α => D.language = 0
Sources
  • Sipser, Introduction to the Theory of Computation, Theorem 4.4.
Uses 20
Statement usesEncoded DFA · Encoded DFAs as triples · Language of an encoded DFA · Decidability by multi-stack machines
Proof usesEmptiness test for encoded DFAs · Letters of an encoded DFA · Correctness of the bounded reachability search · The transition function of encoded DFAs is primitive recursive · Bounded reachability search on lists of states · One round of the list reachability search · Reachable states of an encoded DFA · States of an encoded DFA · Transition function of an encoded DFA · The listed states are closed under transitions · Letters without listed transitions fix every state · The automaton denoted by an encoded DFA · Predicates with a primitive recursive decision procedure are computable · Duplicate removal for lists of natural numbers · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates

TheoremEquivalence of DFAs is decidable#✓fully proved

For every alphabet \(\alpha\) with decidable equality and a primitive recursive encoding, the property of a pair of encoded DFAs over \(\alpha\) that their languages are equal is decidable by a multi-stack machine. This is the problem \(\mathrm{EQ}_{\mathrm{DFA}}\).

theorem tm2Decidable_language_eq :
    TM2Decidable fun p : EncodedDFA α × EncodedDFA α => p.1.language = p.2.language
Sources
  • Sipser, Introduction to the Theory of Computation, Theorem 4.5.
Uses 23
Statement usesEncoded DFA · Encoded DFAs as triples · Language of an encoded DFA · Decidability by multi-stack machines
Proof usesAcceptance test for encoded DFAs · Equivalence test for encoded DFAs · Letters of an encoded DFA · Correctness of the bounded reachability search · Successors of a pair of states · Reachable pairs of states of two encoded DFAs · Coded pairs of states of two encoded DFAs · The transition function of encoded DFAs is primitive recursive · Bounded reachability search on lists of states · One round of the list reachability search · States of an encoded DFA · Transition function of an encoded DFA · The listed states are closed under transitions · Letters without listed transitions fix every state · The automaton denoted by an encoded DFA · Predicates with a primitive recursive decision procedure are computable · Duplicate removal for lists of natural numbers · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates

TheoremUniversality of DFAs is decidable#✓fully proved

For every alphabet \(\alpha\) with decidable equality and a primitive recursive encoding, the property of an encoded DFA over \(\alpha\) that its language is the set of all words over \(\alpha\) is decidable by a multi-stack machine. This is the problem \(\mathrm{ALL}_{\mathrm{DFA}}\).

theorem tm2Decidable_language_eq_top : TM2Decidable fun D : EncodedDFA α => D.language = ⊤
Uses 20
Statement usesEncoded DFA · Encoded DFAs as triples · Language of an encoded DFA · Decidability by multi-stack machines
Proof usesUniversality test for encoded DFAs · Letters of an encoded DFA · Correctness of the bounded reachability search · The transition function of encoded DFAs is primitive recursive · Bounded reachability search on lists of states · One round of the list reachability search · Reachable states of an encoded DFA · States of an encoded DFA · Transition function of an encoded DFA · The listed states are closed under transitions · Letters without listed transitions fix every state · The automaton denoted by an encoded DFA · Predicates with a primitive recursive decision procedure are computable · Duplicate removal for lists of natural numbers · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates

TheoremInfiniteness of DFAs is decidable#✓fully proved

For every finite alphabet \(\alpha\), given with an enumeration of its letters, decidable equality and a primitive recursive encoding, the property of an encoded DFA over \(\alpha\) that its language is infinite is decidable by a multi-stack machine. This is the problem \(\mathrm{INFINITE}_{\mathrm{DFA}}\).

theorem tm2Decidable_language_infinite :
    TM2Decidable fun D : EncodedDFA α => D.language.Infinite
Uses 14
Statement usesEncoded DFA · Encoded DFAs as triples · Language of an encoded DFA · Decidability by multi-stack machines
Proof usesAcceptance test for encoded DFAs · Infiniteness test for encoded DFAs · Correctness of the infiniteness test for encoded DFAs · Running an encoded DFA is primitive recursive · States of an encoded DFA · The automaton denoted by an encoded DFA · Words of a given length · Predicates with a primitive recursive decision procedure are computable · Boolean membership test for lists of natural numbers · Multi-stack decidable predicates are exactly the computable predicates

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.