Encoded finite automata

StructureEncoded DFA#✓fully proved

An encoded deterministic finite automaton over an alphabet \(\alpha\) is a deterministic finite automaton given as data with natural-number states: a start state in \(\mathbb{N}\), a list of accepting states in \(\mathbb{N}\), and a list of transitions \(((s, a), t)\) with \(s, t \in \mathbb{N}\) and \(a \in \alpha\), read as "on letter \(a\), state \(s\) moves to \(t\)".

structure EncodedDFA (α : Type*) where
  /-- The start state. -/
  start : ℕ
  /-- The accepting states. -/
  accept : List ℕ
  /-- The transitions `((s, a), t)`: on letter `a`, state `s` moves to `t`. The first matching
  transition applies; without one the state does not change. -/
  trans : List ((ℕ × α) × ℕ)

Used by 51

Used byAcceptance test for encoded DFAs · Equivalence test for encoded DFAs · Accepted words of length between the number of listed states and twice it · Infiniteness test for encoded DFAs · Correctness of the infiniteness test for encoded DFAs · A long accepted word makes the language of an encoded DFA infinite · Emptiness test for encoded DFAs · Universality test for encoded DFAs · Successors of a pair of states · Reachable pairs of states of two encoded DFAs · Coded 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 · Infiniteness of DFAs is decidable · Acceptance for DFAs is decidable · An encoded DFA on its listed states · Inclusion test · Inclusion of a regular language in a DFA language is decidable · Items found for a grammar and a DFA · Candidate items for a grammar and a DFA · Sound items for a grammar and a DFA · Start states of a right-hand side in a DFA · Start states of a right-hand side are states of the DFA · One round of the item search against a DFA · Whether a symbol fits at a DFA state · The intersection-emptiness test for a grammar and a DFA · Correctness of the intersection-emptiness test · Completeness of the start states in a DFA · The inclusion test for a grammar and a DFA · Correctness of the inclusion test · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable · Complement of an encoded DFA · Encoded DFAs as triples · Every finite DFA has an encoding · Language of an encoded DFA · Letters of an encoded DFA · The complement DFA accepts the complement language · Running an encoded DFA is primitive recursive · Assembling an encoded DFA is primitive recursive · The transition function of encoded DFAs is primitive recursive · States of an encoded DFA · Transition function of an encoded DFA · A step determined by its listed transitions · Unlisted transitions fix the state · Where a step can lead · The listed states are closed under transitions · Letters without listed transitions fix every state · The automaton denoted by an encoded DFA

DefinitionTransition function of an encoded DFA#✓fully proved

For an encoded DFA \(D\), a state \(s \in \mathbb{N}\) and a letter \(a\), the step of \(D\) from \(s\) on \(a\) is the target of the first transition that \(D\) lists from \(s\) on \(a\), or \(s\) itself when \(D\) lists no such transition.

def step (D : EncodedDFA α) (s : ℕ) (a : α) : ℕ :=
  D.trans.foldr (fun e r => if e.1 = (s, a) then e.2 else r) s

Uses 1 · Used by 22

Statement usesEncoded DFA

Used bySuccessors of a pair of states · Reachable states of an encoded DFA · Equivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable · An encoded DFA on its listed states · Inclusion of a regular language in a DFA language is decidable · Whether a symbol fits at a DFA state · Correctness of the intersection-emptiness test · Completeness of the start states in a DFA · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable · Every finite DFA has an encoding · The complement DFA accepts the complement language · Running an encoded DFA is primitive recursive · The transition function of encoded DFAs is primitive recursive · A step determined by its listed transitions · Unlisted transitions fix the state · Where a step can lead · The listed states are closed under transitions · Letters without listed transitions fix every state · The automaton denoted by an encoded DFA

DefinitionThe automaton denoted by an encoded DFA#✓fully proved

An encoded DFA \(D\) over an alphabet \(\alpha\) denotes the deterministic automaton over \(\alpha\) with state set \(\mathbb{N}\) whose start state is the start state of \(D\), whose transition function is the transition function of \(D\), and whose accepting states are the states in the accepting list of \(D\).

def toDFA (D : EncodedDFA α) : DFA α ℕ where
  step := D.step
  start := D.start
  accept := {s | s ∈ D.accept}

Uses 2 · Used by 16

Statement usesEncoded DFA · Transition function of an encoded DFA

Used byAcceptance test for encoded DFAs · Accepted words of length between the number of listed states and twice it · Correctness of the infiniteness test for encoded DFAs · A long accepted word makes the language of an encoded DFA infinite · Equivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable · Infiniteness of DFAs is decidable · Acceptance for DFAs is decidable · Sound items for a grammar and a DFA · Correctness of the intersection-emptiness test · Completeness of the start states in a DFA · Every finite DFA has an encoding · Language of an encoded DFA · The complement DFA accepts the complement language · Running an encoded DFA is primitive recursive

DefinitionLanguage of an encoded DFA#✓fully proved

The language of an encoded DFA \(D\) is the set of words \(w\) such that the state reached by running \(D\) on \(w\) from its start state, following its transition function, is one of its accepting states.

def language (D : EncodedDFA α) : Language α :=
  D.toDFA.accepts

Uses 2 · Used by 15

Statement usesEncoded DFA · The automaton denoted by an encoded DFA

Used byAccepted words of length between the number of listed states and twice it · Correctness of the infiniteness test for encoded DFAs · A long accepted word makes the language of an encoded DFA infinite · Equivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable · Infiniteness of DFAs is decidable · Acceptance for DFAs is decidable · Inclusion of a regular language in a DFA language is decidable · Correctness of the intersection-emptiness test · Correctness of the inclusion test · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable · Every finite DFA has an encoding · The complement DFA accepts the complement language

DefinitionLetters of an encoded DFA#✓fully proved

The letters of an encoded DFA \(D\) form the list of the letters \(a\) of its listed transitions \(((s, a), t)\), in the order the transitions are listed.

def letters (D : EncodedDFA α) : List α :=
  D.trans.map fun e => e.1.2

Uses 1 · Used by 6

Statement usesEncoded DFA

Used bySuccessors of a pair of states · Reachable states of an encoded DFA · Equivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable · Letters without listed transitions fix every state

DefinitionStates of an encoded DFA#✓fully proved

The states of an encoded DFA \(D\) form the list consisting of its start state followed by the targets of its listed transitions, in the order they are listed.

def states (D : EncodedDFA α) : List ℕ :=
  D.start :: D.trans.map Prod.snd

Uses 1 · Used by 24

Statement usesEncoded DFA

Used byAccepted words of length between the number of listed states and twice it · Infiniteness test for encoded DFAs · Correctness of the infiniteness test for encoded DFAs · A long accepted word makes the language of an encoded DFA infinite · Coded 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 · Infiniteness of DFAs is decidable · An encoded DFA on its listed states · Inclusion of a regular language in a DFA language is decidable · Candidate items for a grammar and a DFA · Start states of a right-hand side in a DFA · Start states of a right-hand side are states of the DFA · One round of the item search against a DFA · The intersection-emptiness test for a grammar and a DFA · Correctness of the intersection-emptiness test · Completeness of the start states in a DFA · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable · Complement of an encoded DFA · The complement DFA accepts the complement language · The listed states are closed under transitions

TheoremUnlisted transitions fix the state#✓fully proved

Let \(D\) be an encoded DFA, \(s \in \mathbb{N}\) a state and \(a\) a letter. If \(D\) lists no transition from \(s\) on \(a\), then the transition function of \(D\) takes \(s\) on \(a\) to \(s\).

theorem step_eq_self {D : EncodedDFA α} {s : ℕ} {a : α} (h : ∀ e ∈ D.trans, e.1 ≠ (s, a)) :
    D.step s a = s

Uses 2 · Used by 1

Statement usesEncoded DFA · Transition function of an encoded DFA

Used byLetters without listed transitions fix every state

TheoremA step determined by its listed transitions#✓fully proved

Let \(D\) be an encoded DFA, let \(s, t \in \mathbb{N}\) be states and let \(a\) be a letter. If \(D\) lists at least one transition from \(s\) on \(a\), and every transition listed from \(s\) on \(a\) has target \(t\), then the transition function of \(D\) takes \(s\) on \(a\) to \(t\).

theorem step_eq_of_forall {D : EncodedDFA α} {s t : ℕ} {a : α}
    (hmem : ∃ e ∈ D.trans, e.1 = (s, a)) (huniq : ∀ e ∈ D.trans, e.1 = (s, a) → e.2 = t) :
    D.step s a = t

Uses 2 · Used by 1

Statement usesEncoded DFA · Transition function of an encoded DFA

Used byEvery finite DFA has an encoding

TheoremLetters without listed transitions fix every state#✓fully proved

Let \(D\) be an encoded DFA and let \(a\) be a letter that is not among the letters of \(D\), that is, no listed transition of \(D\) is labelled \(a\). Then for every state \(s \in \mathbb{N}\) the transition function of \(D\) takes \(s\) on \(a\) to \(s\).

theorem step_of_not_mem_letters {D : EncodedDFA α} {s : ℕ} {a : α} (h : a ∉ D.letters) :
    D.step s a = s

Uses 4 · Used by 3

Statement usesEncoded DFA · Letters of an encoded DFA · Transition function of an encoded DFA

Proof usesUnlisted transitions fix the state

Used byEquivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable

TheoremWhere a step can lead#✓fully proved

For every encoded DFA \(D\), state \(s \in \mathbb{N}\) and letter \(a\), the transition function of \(D\) takes \(s\) on \(a\) either to the target of some listed transition of \(D\) or to \(s\) itself.

theorem step_mem_or_eq (D : EncodedDFA α) (s : ℕ) (a : α) :
    D.step s a ∈ D.trans.map Prod.snd ∨ D.step s a = s

Uses 2 · Used by 1

Statement usesEncoded DFA · Transition function of an encoded DFA

Used byThe listed states are closed under transitions

TheoremThe listed states are closed under transitions#✓fully proved

Let \(D\) be an encoded DFA and let \(s\) be one of its states, that is, its start state or the target of one of its listed transitions. Then for every letter \(a\) the transition function of \(D\) takes \(s\) on \(a\) to one of the states of \(D\).

theorem step_mem_states {D : EncodedDFA α} {s : ℕ} (hs : s ∈ D.states) (a : α) :
    D.step s a ∈ D.states

Uses 4 · Used by 7

Statement usesEncoded DFA · States of an encoded DFA · Transition function of an encoded DFA

Proof usesWhere a step can lead

Used byEquivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable · An encoded DFA on its listed states · Correctness of the intersection-emptiness test · Completeness of the start states in a DFA · The complement DFA accepts the complement language

DefinitionComplement of an encoded DFA#✓fully proved

The complement of an encoded DFA \(D\) has the same start state and the same transitions as \(D\), and its accepting states are those states of \(D\) (its start state and the targets of its listed transitions) that \(D\) does not accept.

def compl (D : EncodedDFA α) : EncodedDFA α :=
  ⟨D.start, D.states.filter fun s => decide (s ∉ D.accept), D.trans⟩

Uses 2 · Used by 5

Statement usesEncoded DFA · States of an encoded DFA

Used byInclusion of a regular language in a DFA language is decidable · The inclusion test for a grammar and a DFA · Correctness of the inclusion test · Inclusion of a context-free language in a regular language is decidable · The complement DFA accepts the complement language

TheoremThe complement DFA accepts the complement language#✓fully proved

For every encoded DFA \(D\) and every word \(w\), the complement of \(D\) accepts \(w\) if and only if \(D\) does not accept \(w\).

theorem mem_language_compl {D : EncodedDFA α} {w : List α} :
    w ∈ D.compl.language ↔ w ∉ D.language

Uses 7 · Used by 1

Statement usesEncoded DFA · Complement of an encoded DFA · Language of an encoded DFA

Proof usesStates of an encoded DFA · Transition function of an encoded DFA · The listed states are closed under transitions · The automaton denoted by an encoded DFA

Used byCorrectness of the inclusion test

TheoremEvery finite DFA has an encoding#✓fully proved

A DFA over a finite alphabet with finitely many states has an encoded DFA with the same language.

theorem exists_language_eq [Finite α] {σ : Type*} [Finite σ] (M : DFA α σ) :
    ∃ D : EncodedDFA α, D.language = M.accepts

Uses 5

Statement usesEncoded DFA · Language of an encoded DFA

Proof usesTransition function of an encoded DFA · A step determined by its listed transitions · The automaton denoted by an encoded DFA

DefinitionEncoded DFAs as triples#✓fully proved

Sending an encoded DFA over \(\alpha\) to the triple of its start state, its list of accepting states and its list of transitions is an equivalence (a bijection with explicit inverse) between encoded DFAs over \(\alpha\) and the set \(\mathbb{N} \times \mathrm{List}\,\mathbb{N} \times \mathrm{List}((\mathbb{N} \times \alpha) \times \mathbb{N})\).

def equivProd : EncodedDFA α ≃ ℕ × List ℕ × List ((ℕ × α) × ℕ) where
  toFun D := (D.start, D.accept, D.trans)
  invFun p := ⟨p.1, p.2.1, p.2.2⟩
  left_inv _ := rfl
  right_inv _ := rfl

Uses 1 · Used by 11

Statement usesEncoded DFA

Used byEquivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable · Infiniteness of DFAs is decidable · Acceptance for DFAs is decidable · Inclusion of a regular language in a DFA language is decidable · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable · Running an encoded DFA is primitive recursive · Assembling an encoded DFA is primitive recursive · The transition function of encoded DFAs is primitive recursive

TheoremAssembling an encoded DFA is primitive recursive#✓fully proved

Let \(\alpha\) be an alphabet with a primitive recursive encoding, and encode encoded DFAs over \(\alpha\) through their start state, accepting states and transitions. The map sending a triple \((s, F, T)\), where \(s \in \mathbb{N}\), \(F\) is a list of natural numbers and \(T\) is a list of pairs \(((q, a), t)\) with \(q, t \in \mathbb{N}\) and \(a \in \alpha\), to the encoded DFA over \(\alpha\) with start state \(s\), accepting states \(F\) and transitions \(T\) is primitive recursive.

theorem primrec_mk : Primrec fun p : ℕ × List ℕ × List ((ℕ × α) × ℕ) => (⟨p.1, p.2.1, p.2.2⟩ :
    EncodedDFA α)

Uses 2 · Used by 2

Statement usesEncoded DFA · Encoded DFAs as triples

Used byInclusion of a regular language in a DFA language is decidable · Inclusion of a context-free language in a regular language is decidable

TheoremThe transition function of encoded DFAs is primitive recursive#✓fully proved

Let \(\alpha\) be an alphabet with a primitive recursive encoding and decidable equality, and encode encoded DFAs over \(\alpha\) through their start state, accepting states and transitions. The map sending an encoded DFA \(D\) over \(\alpha\), a state \(s \in \mathbb{N}\) and a letter \(a \in \alpha\) to the state that \(D\) moves to from \(s\) on \(a\) (the target of the first transition listed for \((s, a)\), or \(s\) if there is none) is primitive recursive.

theorem primrec_step : Primrec fun p : EncodedDFA α × ℕ × α => p.1.step p.2.1 p.2.2

Uses 3 · Used by 7

Statement usesEncoded DFA · Encoded DFAs as triples · Transition function of an encoded DFA

Used byEquivalence of DFAs is decidable · Universality of DFAs is decidable · Emptiness of DFAs is decidable · Inclusion of a regular language in a DFA language is decidable · Emptiness of the intersection of a context-free and a regular language is decidable · Inclusion of a context-free language in a regular language is decidable · Running an encoded DFA is primitive recursive

TheoremRunning an encoded DFA is primitive recursive#✓fully proved

Let \(\alpha\) be an alphabet with a primitive recursive encoding and decidable equality, and encode encoded DFAs over \(\alpha\) through their start state, accepting states and transitions. The map sending an encoded DFA \(D\) and a word \(w\) over \(\alpha\) to the state reached by running \(D\) on \(w\) from its start state is primitive recursive.

theorem primrec₂_eval : Primrec₂ fun (D : EncodedDFA α) (w : List α) => D.toDFA.eval w

Uses 5 · Used by 2

Statement usesEncoded DFA · Encoded DFAs as triples · The automaton denoted by an encoded DFA

Proof usesThe transition function of encoded DFAs is primitive recursive · Transition function of an encoded DFA

Used byInfiniteness of DFAs is decidable · Acceptance for DFAs is decidable

StructureEncoded NFA#✓fully proved

An encoded NFA over an alphabet \(\alpha\) is a nondeterministic finite automaton with ε-moves given as data, with natural numbers as states: a list of start states, a list of accepting states, a list of transitions \(((s, a), t)\), meaning that on the letter \(a\) the state \(s\) may move to \(t\), and a list of ε-moves \((s, t)\), meaning that the state \(s\) may move to \(t\) without reading a letter.

structure EncodedNFA (α : Type*) where
  /-- The start states. -/
  start : List ℕ
  /-- The accepting states. -/
  accept : List ℕ
  /-- The transitions `((s, a), t)`: on letter `a`, state `s` may move to `t`. -/
  trans : List ((ℕ × α) × ℕ)
  /-- The ε-moves `(s, t)`: state `s` may move to `t` without reading a letter. -/
  eps : List (ℕ × ℕ)

Used by 23

Used byMembership test for encoded NFAs · Correctness of the NFA membership test · ε-closure of a list of states · ε-successors of a state · ε-move relation · Encoded NFAs as tuples · The states reached on a word are closed under ε-moves · Every finite NFA has an encoding · Every finite ε-NFA has an encoding · Emptiness test for encoded NFAs · Language of an encoded NFA · Letter step of an encoded NFA · The ε-closure is reachability along ε-moves · The reachable states are those some word can lead to · The run of an encoded NFA agrees with ε-NFA evaluation · Successors of a state in an encoded NFA · Reachable states of an encoded NFA · Run of an encoded NFA · States an encoded NFA mentions as start states or targets · One step of an encoded NFA on a list of states · Emptiness of NFAs is decidable · Membership for NFAs is decidable · The ε-NFA of an encoded NFA

DefinitionThe ε-NFA of an encoded NFA#✓fully proved

An encoded NFA \(N\) over \(\alpha\) denotes the ε-NFA over \(\alpha\) with state set \(\mathbb{N}\) whose start states are the start states listed in \(N\), whose accepting states are the accepting states listed in \(N\), and in which a state \(s\) may move to \(t\) on a letter \(a\) exactly when \(((s, a), t)\) is a transition of \(N\), and without reading a letter exactly when \((s, t)\) is an ε-move of \(N\).

def toεNFA (N : EncodedNFA α) : εNFA α ℕ where
  step s o := match o with
    | some a => {t | ((s, a), t) ∈ N.trans}
    | none => {t | (s, t) ∈ N.eps}
  start := {s | s ∈ N.start}
  accept := {s | s ∈ N.accept}

Uses 1 · Used by 8

Statement usesEncoded NFA

Used byCorrectness of the NFA membership test · The states reached on a word are closed under ε-moves · Every finite ε-NFA has an encoding · Language of an encoded NFA · The ε-closure is reachability along ε-moves · The reachable states are those some word can lead to · The run of an encoded NFA agrees with ε-NFA evaluation · Emptiness of NFAs is decidable

DefinitionLanguage of an encoded NFA#✓fully proved

The language of an encoded NFA \(N\) over an alphabet \(\alpha\) is the language accepted by the ε-NFA that \(N\) denotes, whose states are the natural numbers: the words \(w\) over \(\alpha\) such that some accepting state of \(N\) is among the states reached on \(w\) from the start states of \(N\), with ε-moves allowed before, between and after the letters.

def language (N : EncodedNFA α) : Language α :=
  N.toεNFA.accepts

Uses 2 · Used by 5

Statement usesEncoded NFA · The ε-NFA of an encoded NFA

Used byCorrectness of the NFA membership test · Every finite NFA has an encoding · Every finite ε-NFA has an encoding · Emptiness of NFAs is decidable · Membership for NFAs is decidable

DefinitionStates an encoded NFA mentions as start states or targets#✓fully proved

For an encoded NFA \(N\), this is the list of the start states of \(N\), followed by the targets \(t\) of its transitions \(((s, a), t)\), followed by the targets \(t\) of its ε-moves \((s, t)\).

def states (N : EncodedNFA α) : List ℕ :=
  N.start ++ N.trans.map Prod.snd ++ N.eps.map Prod.snd

Uses 1 · Used by 6

Statement usesEncoded NFA

Used byε-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

Definitionε-move relation#✓fully proved

For an encoded NFA \(N\), the ε-move relation holds between states \(s\) and \(t\) exactly when \((s, t)\) is one of the ε-moves of \(N\).

def EpsRel (N : EncodedNFA α) (s t : ℕ) : Prop :=
  (s, t) ∈ N.eps

Uses 1 · Used by 4

Statement usesEncoded NFA

Used byThe states reached on a word are closed under ε-moves · The ε-closure is reachability along ε-moves · The reachable states are those some word can lead to · The run of an encoded NFA agrees with ε-NFA evaluation

TheoremThe ε-closure is reachability along ε-moves#✓fully proved

For an encoded NFA \(N\), a set \(X\) of natural numbers and a natural number \(t\), \(t\) lies in the ε-closure of \(X\) in the ε-NFA that \(N\) denotes if and only if \(t\) is reachable from some \(u \in X\) by a sequence of zero or more ε-moves of \(N\).

theorem mem_εClosure_iff {N : EncodedNFA α} {X : Set ℕ} {t : ℕ} :
    t ∈ N.toεNFA.εClosure X ↔ ∃ u ∈ X, Relation.ReflTransGen N.EpsRel u t

Uses 3 · Used by 2

Statement usesEncoded NFA · ε-move relation · The ε-NFA of an encoded NFA

Used byThe reachable states are those some word can lead to · The run of an encoded NFA agrees with ε-NFA evaluation

Definitionε-successors of a state#✓fully proved

For an encoded NFA \(N\) and a state \(s\), the ε-successors of \(s\) are the list of the targets \(t\) of the ε-moves \((s, t)\) of \(N\), in the order in which these ε-moves are listed.

def epsNext (N : EncodedNFA α) (s : ℕ) : List ℕ :=
  N.eps.filterMap fun e => cond (decide (e.1 = s)) (some e.2) none

Uses 1 · Used by 6

Statement usesEncoded NFA

Used byε-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 · Successors of a state in an encoded NFA · Emptiness of NFAs is decidable · Membership for NFAs is decidable

Definitionε-closure of a list of states#✓fully proved

For an encoded NFA \(N\) and a list \(S\) of states, the ε-closure of \(S\) is a list whose members are exactly the states reachable from some state of \(S\) by finitely many ε-moves of \(N\) (zero moves included), computed by a search from each state of \(S\).

def closure (N : EncodedNFA α) (S : List ℕ) : List ℕ :=
  S.flatMap fun s => EncodedDFA.reachN s N.epsNext (s :: N.states)

Uses 4 · Used by 4

Statement usesBounded reachability search on lists of states · Encoded NFA · ε-successors of a state · States an encoded NFA mentions as start states or targets

Used byThe run of an encoded NFA agrees with ε-NFA evaluation · Run of an encoded NFA · One step of an encoded NFA on a list of states · Membership for NFAs is decidable

DefinitionLetter step of an encoded NFA#✓fully proved

For an encoded NFA \(N\), a list \(S\) of states and a letter \(a\), the letter step lists the target \(t\) of every transition \(((s, a), t)\) of \(N\) with \(s \in S\), in the order of the transition list of \(N\), without taking the ε-closure.

def letterStep (N : EncodedNFA α) (S : List ℕ) (a : α) : List ℕ :=
  N.trans.filterMap fun e => cond (memB S e.1.1 && decide (e.1.2 = a)) (some e.2) none

Uses 2 · Used by 3

Statement usesEncoded NFA · Boolean membership test for lists of natural numbers

Used byThe run of an encoded NFA agrees with ε-NFA evaluation · One step of an encoded NFA on a list of states · Membership for NFAs is decidable

DefinitionOne step of an encoded NFA on a list of states#✓fully proved

For an encoded NFA \(N\), a list \(S\) of states and a letter \(a\), the list of states reached from \(S\) on \(a\): the ε-closure, computed as a list, of the list of states \(t\) such that \(((s, a), t)\) is a transition of \(N\) for some \(s\) in \(S\).

def stepList (N : EncodedNFA α) (S : List ℕ) (a : α) : List ℕ :=
  N.closure (N.letterStep S a)

Uses 3 · Used by 3

Statement usesEncoded NFA · ε-closure of a list of states · Letter step of an encoded NFA

Used byThe run of an encoded NFA agrees with ε-NFA evaluation · Run of an encoded NFA · Membership for NFAs is decidable

DefinitionRun of an encoded NFA#✓fully proved

For an encoded NFA \(N\) and a word \(w = a_1 \cdots a_n\), the run of \(N\) on \(w\) is the list of states obtained by starting from the ε-closure of the start states of \(N\) and, for each letter \(a_i\) in turn, taking the letter step on \(a_i\) and then the ε-closure.

def run (N : EncodedNFA α) (w : List α) : List ℕ :=
  w.foldl N.stepList (N.closure N.start)

Uses 3 · Used by 4

Statement usesEncoded NFA · ε-closure of a list of states · One step of an encoded NFA on a list of states

Used byMembership test for encoded NFAs · Correctness of the NFA membership test · The run of an encoded NFA agrees with ε-NFA evaluation · Membership for NFAs is decidable

DefinitionMembership test for encoded NFAs#✓fully proved

For an encoded NFA \(N\) and a word \(w\), the membership test is the Boolean that is true exactly when some state reached on \(w\) is an accepting state of \(N\). The states reached on \(w\) are computed from the ε-closure of the start states by, for each letter of \(w\) in turn, following the transitions on that letter and taking the ε-closure.

def acceptsB (N : EncodedNFA α) (w : List α) : Bool :=
  (N.run w).any (memB N.accept)

Uses 3 · Used by 2

Statement usesEncoded NFA · Run of an encoded NFA · Boolean membership test for lists of natural numbers

Used byCorrectness of the NFA membership test · Membership for NFAs is decidable

TheoremThe run of an encoded NFA agrees with ε-NFA evaluation#✓fully proved

For an encoded NFA \(N\), a word \(w\) and a natural number \(t\), \(t\) is among the states in the run of \(N\) on \(w\) if and only if \(t\) is among the states that the ε-NFA denoted by \(N\) reaches on \(w\) from its start states, with ε-moves allowed before, between and after the letters.

theorem mem_run_iff {N : EncodedNFA α} {w : List α} {t : ℕ} :
    t ∈ N.run w ↔ t ∈ N.toεNFA.eval w

Uses 13 · Used by 1

Statement usesEncoded NFA · Run of an encoded NFA · The ε-NFA of an encoded NFA

Proof usesCorrectness of the bounded reachability search · Bounded reachability search on lists of states · ε-move relation · ε-closure of a list of states · ε-successors of a state · Letter step of an encoded NFA · The ε-closure is reachability along ε-moves · States an encoded NFA mentions as start states or targets · One step of an encoded NFA on a list of states · Boolean membership test for lists of natural numbers

Used byCorrectness of the NFA membership test

TheoremCorrectness of the NFA membership test#✓fully proved

For an encoded NFA \(N\) and a word \(w\), the membership test returns true on \(w\) if and only if \(w\) belongs to the language of \(N\).

theorem acceptsB_iff {N : EncodedNFA α} {w : List α} : N.acceptsB w = true ↔ w ∈ N.language

Uses 7 · Used by 1

Statement usesEncoded NFA · Membership test for encoded NFAs · Language of an encoded NFA

Proof usesThe run of an encoded NFA agrees with ε-NFA evaluation · Run of an encoded NFA · The ε-NFA of an encoded NFA · Boolean membership test for lists of natural numbers

Used byMembership for NFAs is decidable

TheoremThe states reached on a word are closed under ε-moves#✓fully proved

Let \(N\) be an encoded NFA and \(w\) a word. If \(u\) is one of the states that the ε-NFA denoted by \(N\) can be in after reading \(w\), and \(N\) has an ε-move from \(u\) to \(v\), then \(v\) is also one of these states.

theorem eval_epsRel {N : EncodedNFA α} {w : List α} {u v : ℕ} (hu : u ∈ N.toεNFA.eval w)
    (huv : N.EpsRel u v) : v ∈ N.toεNFA.eval w

Uses 3 · Used by 1

Statement usesEncoded NFA · ε-move relation · The ε-NFA of an encoded NFA

Used byThe reachable states are those some word can lead to

DefinitionSuccessors of a state in an encoded NFA#✓fully proved

For an encoded NFA \(N\) and a state \(s\), this is the list of the targets \(t\) of the transitions \(((s, a), t)\) of \(N\) on any letter \(a\), followed by the targets \(t\) of the ε-moves \((s, t)\) of \(N\), each in the order of the corresponding list of \(N\).

def next (N : EncodedNFA α) (s : ℕ) : List ℕ :=
  N.trans.filterMap (fun e => cond (decide (e.1.1 = s)) (some e.2) none) ++ N.epsNext s

Uses 2 · Used by 3

Statement usesEncoded NFA · ε-successors of a state

Used byThe reachable states are those some word can lead to · Reachable states of an encoded NFA · Emptiness of NFAs is decidable

DefinitionReachable states of an encoded NFA#✓fully proved

For an encoded NFA \(N\), this is the list, found by a search from each start state of \(N\) in turn through the start states of \(N\) and the targets of its transitions and ε-moves, of the states reachable from a start state of \(N\) by zero or more moves, each a transition of \(N\) on some letter or an ε-move of \(N\).

def reachable (N : EncodedNFA α) : List ℕ :=
  N.start.flatMap fun s => EncodedDFA.reachN s N.next N.states

Uses 4 · Used by 3

Statement usesBounded reachability search on lists of states · Encoded NFA · Successors of a state in an encoded NFA · States an encoded NFA mentions as start states or targets

Used byEmptiness test for encoded NFAs · The reachable states are those some word can lead to · Emptiness of NFAs is decidable

TheoremThe reachable states are those some word can lead to#✓fully proved

For an encoded NFA \(N\) and a natural number \(t\), \(t\) is among the reachable states of \(N\) if and only if there is a word \(w\) such that \(t\) is among the states that the ε-NFA denoted by \(N\) reaches on \(w\) from its start states, with ε-moves allowed before, between and after the letters.

theorem mem_reachable_iff {N : EncodedNFA α} {t : ℕ} :
    t ∈ N.reachable ↔ ∃ w, t ∈ N.toεNFA.eval w

Uses 11 · Used by 1

Statement usesEncoded NFA · Reachable states of an encoded NFA · The ε-NFA of an encoded NFA

Proof usesCorrectness of the bounded reachability search · Bounded reachability search on lists of states · ε-move relation · ε-successors of a state · The states reached on a word are closed under ε-moves · The ε-closure is reachability along ε-moves · Successors of a state in an encoded NFA · States an encoded NFA mentions as start states or targets

Used byEmptiness of NFAs is decidable

DefinitionEmptiness test for encoded NFAs#✓fully proved

For an encoded NFA \(N\), the emptiness test is the Boolean that is true exactly when no state in the list of reachable states of \(N\) is an accepting state of \(N\); the reachable states are those reachable from a start state of \(N\) by zero or more moves, each a transition on some letter or an ε-move.

def isEmptyB (N : EncodedNFA α) : Bool :=
  N.reachable.all fun s => !memB N.accept s

Uses 3 · Used by 1

Statement usesEncoded NFA · Reachable states of an encoded NFA · Boolean membership test for lists of natural numbers

Used byEmptiness of NFAs is decidable

TheoremEvery finite ε-NFA has an encoding#✓fully proved

An εNFA over a finite alphabet with finitely many states has an encoded NFA with the same language.

theorem exists_language_eq_εNFA [Finite α] {σ : Type*} [Finite σ] (M : εNFA α σ) :
    ∃ N : EncodedNFA α, N.language = M.accepts

Uses 3 · Used by 1

Statement usesEncoded NFA · Language of an encoded NFA

Proof usesThe ε-NFA of an encoded NFA

Used byEvery finite NFA has an encoding

TheoremEvery finite NFA has an encoding#✓fully proved

An NFA over a finite alphabet with finitely many states has an encoded NFA with the same language.

theorem exists_language_eq [Finite α] {σ : Type*} [Finite σ] (M : NFA α σ) :
    ∃ N : EncodedNFA α, N.language = M.accepts

Uses 3

Statement usesEncoded NFA · Language of an encoded NFA

Proof usesEvery finite ε-NFA has an encoding

DefinitionEncoded NFAs as tuples#✓fully proved

The bijection between encoded NFAs over \(\alpha\) and quadruples consisting of a list of natural numbers, a list of natural numbers, a list of elements of \((\mathbb{N} \times \alpha) \times \mathbb{N}\) and a list of pairs of natural numbers, which sends an encoded NFA to its start states, accepting states, transitions and ε-moves.

def equivProd : EncodedNFA α ≃ List ℕ × List ℕ × List ((ℕ × α) × ℕ) × List (ℕ × ℕ) where
  toFun N := (N.start, N.accept, N.trans, N.eps)
  invFun p := ⟨p.1, p.2.1, p.2.2.1, p.2.2.2⟩
  left_inv _ := rfl
  right_inv _ := rfl

Uses 1 · Used by 2

Statement usesEncoded NFA

Used byEmptiness of NFAs is decidable · Membership for NFAs is decidable

TheoremMembership for NFAs is decidable#✓fully proved

For every alphabet \(\alpha\) with a primitive recursive encoding, the property of a pair \((N, w)\), where \(N\) is an encoded NFA (with ε-moves) over \(\alpha\) and \(w\) is a word over \(\alpha\), that \(w\) is in the language of \(N\) is decidable by a multi-stack machine. This is Sipser, Theorem 4.2: the problem \(A_{\mathrm{NFA}}\) is decidable.

theorem tm2Decidable_mem_language :
    TM2Decidable fun p : EncodedNFA α × List α => p.2 ∈ p.1.language

Uses 18

Statement usesEncoded NFA · Encoded NFAs as tuples · Language of an encoded NFA · Decidability by multi-stack machines

Proof usesBounded reachability search on lists of states · One round of the list reachability search · Membership test for encoded NFAs · Correctness of the NFA membership test · ε-closure of a list of states · ε-successors of a state · Letter step of an encoded NFA · Run of an encoded NFA · States an encoded NFA mentions as start states or targets · One step of an encoded NFA on a list of states · 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

TheoremEmptiness of NFAs is decidable#✓fully proved

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

theorem tm2Decidable_language_eq_zero : TM2Decidable fun N : EncodedNFA α => N.language = 0

Uses 17

Statement usesEncoded NFA · Encoded NFAs as tuples · Language of an encoded NFA · Decidability by multi-stack machines

Proof usesBounded reachability search on lists of states · One round of the list reachability search · ε-successors of a state · Emptiness test for encoded NFAs · The reachable states are those some word can lead to · Successors of a state in an encoded NFA · Reachable states of an encoded NFA · States an encoded NFA mentions as start states or targets · The ε-NFA of an encoded NFA · 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

42 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.