Nondeterministic Finite Automata

A Nondeterministic Finite Automaton (NFA) is a state machine which decides membership in a particular Language, by following every possible path that describes an input string.

We show that DFAs and NFAs can decide the same languages, by constructing an equivalent DFA for every NFA, and vice versa.

As constructing a DFA from an NFA uses an exponential number of states, we re-prove the pumping lemma instead of lifting DFA.pumping_lemma, in order to obtain the optimal bound on the minimal length of the string.

Like DFA, this definition allows for automata with infinite states; a Fintype instance must be supplied for true NFAs.

Main definitions

• NFA α σ: automaton over alphabet α and set of states σ
• NFA.evalFrom M S x: set of possible ending states for an input word x and set of initial states S
• NFA.accepts M: the language accepted by the NFA M
• NFA.Path M s t x: a specific path from s to t for an input word x
• NFA.Path.supp p: set of states visited by the path p

Main theorems

• NFA.pumping_lemma: every sufficiently long string accepted by the NFA has a substring that can be repeated arbitrarily many times (and have the overall string still be accepted)

structure NFA (α : Type u) (σ : Type v) : Type (max u v)

An NFA is a set of states (σ), a transition function from state to state labelled by the alphabet (step), a set of starting states (start) and a set of acceptance states (accept). Note the transition function sends a state to a Set of states. These are the states that it may be sent to.

• step : σ → α → Set σ

  The NFA's transition function

• start : Set σ

  Set of starting states

• accept : Set σ

  Set of accepting states

@[implicit_reducible]

instance NFA.instInhabited {α : Type u} {σ : Type v} : Inhabited (NFA α σ)

def NFA.stepSet {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (a : α) : Set σ

M.stepSet S a is the union of M.step s a for all s ∈ S.

theorem NFA.mem_stepSet {α : Type u} {σ : Type v} {M : NFA α σ} {s : σ} {S : Set σ} {a : α} : s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a

@[simp]

theorem NFA.stepSet_empty {α : Type u} {σ : Type v} (M : NFA α σ) (a : α) : M.stepSet ∅ a = ∅

@[simp]

theorem NFA.stepSet_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (s : σ) (a : α) : M.stepSet {s} a = M.step s a

@[simp]

theorem NFA.stepSet_union {α : Type u} {σ : Type v} (M : NFA α σ) {S T : Set σ} {a : α} : M.stepSet (S ∪ T) a = M.stepSet S a ∪ M.stepSet T a

def NFA.evalFrom {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) : List α → Set σ

M.evalFrom S x computes all possible paths through M with input x starting at an element of S.

@[simp]

theorem NFA.evalFrom_nil {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) : M.evalFrom S [] = S

@[simp]

theorem NFA.evalFrom_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (a : α) : M.evalFrom S [a] = M.stepSet S a

@[simp]

theorem NFA.evalFrom_cons {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (a : α) (x : List α) : M.evalFrom S (a :: x) = M.evalFrom (M.stepSet S a) x

@[simp]

theorem NFA.evalFrom_append {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (x y : List α) : M.evalFrom S (x ++ y) = M.evalFrom (M.evalFrom S x) y

@[deprecated "Use evalFrom_append, evalFrom_cons, and evalFrom_nil" (since := "2025-11-17")]

theorem NFA.evalFrom_append_singleton {α : Type u} {σ : Type v} {M : NFA α σ} (S : Set σ) (x : List α) (a : α) : M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a

@[simp]

theorem NFA.evalFrom_union {α : Type u} {σ : Type v} (M : NFA α σ) (S T : Set σ) (x : List α) : M.evalFrom (S ∪ T) x = M.evalFrom S x ∪ M.evalFrom T x

@[simp]

theorem NFA.evalFrom_iUnion {α : Type u} {σ : Type v} (M : NFA α σ) {ι : Sort u_1} (s : ι → Set σ) (x : List α) : M.evalFrom (⋃ (i : ι), s i) x = ⋃ (i : ι), M.evalFrom (s i) x

theorem NFA.evalFrom_iUnion₂ {α : Type u} {σ : Type v} (M : NFA α σ) {ι : Sort u_1} {κ : ι → Sort u_2} (f : (i : ι) → κ i → Set σ) (x : List α) : M.evalFrom (⋃ (i : ι), ⋃ (j : κ i), f i j) x = ⋃ (i : ι), ⋃ (j : κ i), M.evalFrom (f i j) x

@[deprecated NFA.evalFrom_iUnion₂ (since := "2025-11-17")]

theorem NFA.evalFrom_biUnion {α : Type u} {σ : Type v} (M : NFA α σ) {ι : Type u_1} (t : Set ι) (f : ι → Set σ) (x : List α) : M.evalFrom (⋃ i ∈ t, f i) x = ⋃ i ∈ t, M.evalFrom (f i) x

theorem NFA.evalFrom_eq_biUnion_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (x : List α) : M.evalFrom S x = ⋃ s ∈ S, M.evalFrom {s} x

theorem NFA.mem_evalFrom_iff_exists {α : Type u} {σ : Type v} {M : NFA α σ} {s : σ} {S : Set σ} {x : List α} : s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

def NFA.acceptsFrom {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) : Language α

M.acceptsFrom S is the language of x such that there is an accept state in M.evalFrom S x.

theorem NFA.mem_acceptsFrom {α : Type u} {σ : Type v} {M : NFA α σ} {S : Set σ} {x : List α} : x ∈ M.acceptsFrom S ↔ ∃ s ∈ M.accept, s ∈ M.evalFrom S x

@[simp]

theorem NFA.nil_mem_acceptsFrom {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ} : [] ∈ M.acceptsFrom S ↔ ∃ s ∈ S, s ∈ M.accept

@[simp]

theorem NFA.cons_mem_acceptsFrom {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ} {a : α} {x : List α} : a :: x ∈ M.acceptsFrom S ↔ x ∈ M.acceptsFrom (M.stepSet S a)

theorem NFA.cons_preimage_acceptsFrom {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ} {a : α} : (fun (x : List α) => a :: x) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.stepSet S a)

@[simp]

theorem NFA.append_mem_acceptsFrom {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ} {x y : List α} : x ++ y ∈ M.acceptsFrom S ↔ y ∈ M.acceptsFrom (M.evalFrom S x)

theorem NFA.append_preimage_acceptsFrom {α : Type u} {σ : Type v} (M : NFA α σ) {S : Set σ} {x : List α} : (fun (x_1 : List α) => x ++ x_1) ⁻¹' M.acceptsFrom S = M.acceptsFrom (M.evalFrom S x)

@[simp]

theorem NFA.acceptsFrom_union {α : Type u} {σ : Type v} (M : NFA α σ) {S T : Set σ} : M.acceptsFrom (S ∪ T) = M.acceptsFrom S + M.acceptsFrom T

@[simp]

theorem NFA.acceptsFrom_iUnion {α : Type u} {σ : Type v} (M : NFA α σ) {ι : Sort u_1} (s : ι → Set σ) : M.acceptsFrom (⋃ (i : ι), s i) = ⋃ (i : ι), M.acceptsFrom (s i)

theorem NFA.acceptsFrom_iUnion₂ {α : Type u} {σ : Type v} (M : NFA α σ) {ι : Sort u_1} {κ : ι → Sort u_2} (f : (i : ι) → κ i → Set σ) : M.acceptsFrom (⋃ (i : ι), ⋃ (j : κ i), f i j) = ⋃ (i : ι), ⋃ (j : κ i), M.acceptsFrom (f i j)

def NFA.eval {α : Type u} {σ : Type v} (M : NFA α σ) : List α → Set σ

M.eval x computes all possible paths though M with input x starting at an element of M.start.

@[simp]

theorem NFA.eval_nil {α : Type u} {σ : Type v} (M : NFA α σ) : M.eval [] = M.start

@[simp]

theorem NFA.eval_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (a : α) : M.eval [a] = M.stepSet M.start a

@[simp]

theorem NFA.eval_append_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (x : List α) (a : α) : M.eval (x ++ [a]) = M.stepSet (M.eval x) a

def NFA.accepts {α : Type u} {σ : Type v} (M : NFA α σ) : Language α

M.accepts is the language of x such that there is an accept state in M.eval x.

theorem NFA.mem_accepts {α : Type u} {σ : Type v} {M : NFA α σ} {x : List α} : x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x

theorem NFA.accepts_eq_acceptsFrom_start {α : Type u} {σ : Type v} {M : NFA α σ} : M.accepts = M.acceptsFrom M.start

inductive NFA.Path {α : Type u} {σ : Type v} (M : NFA α σ) : σ → σ → List α → Type (max u v)

M.Path represents a concrete path through the NFA from a start state to an end state for a particular word.

Note that due to the non-deterministic nature of the automata, there can be more than one Path for a given word.

Also note that this is Type and not a Prop, so that we can speak about the properties of a particular Path, such as the set of states visited along the way (defined as Path.supp).

• nil {α : Type u} {σ : Type v} {M : NFA α σ} (s : σ) : M.Path s s []
• cons {α : Type u} {σ : Type v} {M : NFA α σ} (t s u : σ) (a : α) (x : List α) : t ∈ M.step s a → M.Path t u x → M.Path s u (a :: x)

def NFA.Path.supp {α : Type u} {σ : Type v} {M : NFA α σ} [DecidableEq σ] {s t : σ} {x : List α} : M.Path s t x → Finset σ

Set of states visited by a path.

theorem NFA.mem_evalFrom_iff_nonempty_path {α : Type u} {σ : Type v} {M : NFA α σ} {s t : σ} {x : List α} : t ∈ M.evalFrom {s} x ↔ Nonempty (M.Path s t x)

theorem NFA.accepts_iff_exists_path {α : Type u} {σ : Type v} {M : NFA α σ} {x : List α} : x ∈ M.accepts ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, Nonempty (M.Path s t x)

def NFA.toDFA {α : Type u} {σ : Type v} (M : NFA α σ) : DFA α (Set σ)

M.toDFA is a DFA constructed from an NFA M using the subset construction. The states is the type of Sets of M.state and the step function is M.stepSet.

@[simp]

theorem NFA.toDFA_correct {α : Type u} {σ : Type v} {M : NFA α σ} : M.toDFA.accepts = M.accepts

theorem NFA.pumping_lemma {α : Type u} {σ : Type v} {M : NFA α σ} [Fintype σ] {x : List α} (hx : x ∈ M.accepts) (hlen : Fintype.card (Set σ) ≤ x.length) : ∃ (a : List α) (b : List α) (c : List α), x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * KStar.kstar {b} * {c} ≤ M.accepts

def DFA.toNFA {α : Type u} {σ : Type v} (M : DFA α σ) : NFA α σ

M.toNFA is an NFA constructed from a DFA M by using the same start and accept states and a transition function which sends s with input a to the singleton M.step s a.

@[simp]

theorem DFA.toNFA_start {α : Type u} {σ : Type v} (M : DFA α σ) : M.toNFA.start = {M.start}

@[simp]

theorem DFA.toNFA_step {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (a : α) : M.toNFA.step s a = {M.step s a}

@[simp]

theorem DFA.toNFA_accept {α : Type u} {σ : Type v} (M : DFA α σ) : M.toNFA.accept = M.accept

@[simp]

theorem DFA.toNFA_evalFrom_match {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) (s : List α) : M.toNFA.evalFrom {start} s = {M.evalFrom start s}

@[simp]

theorem DFA.toNFA_correct {α : Type u} {σ : Type v} (M : DFA α σ) : M.toNFA.accepts = M.accepts

def NFA.reverse {α : Type u} {σ : Type v} (M : NFA α σ) : NFA α σ

M.reverse constructs an NFA with the same states as M, but all the transitions reversed. The resulting automaton accepts a word x if and only if M accepts List.reverse x.

@[simp]

theorem NFA.reverse_accept {α : Type u} {σ : Type v} (M : NFA α σ) : M.reverse.accept = M.start

@[simp]

theorem NFA.reverse_start {α : Type u} {σ : Type v} (M : NFA α σ) : M.reverse.start = M.accept

@[simp]

theorem NFA.reverse_step {α : Type u} {σ : Type v} (M : NFA α σ) (s : σ) (a : α) : M.reverse.step s a = {s' : σ | s ∈ M.step s' a}

@[simp]

theorem NFA.reverse_reverse {α : Type u} {σ : Type v} (M : NFA α σ) : M.reverse.reverse = M

theorem NFA.disjoint_stepSet_reverse {α : Type u} {σ : Type v} {M : NFA α σ} {a : α} {S S' : Set σ} : Disjoint S (M.reverse.stepSet S' a) ↔ Disjoint S' (M.stepSet S a)

theorem NFA.disjoint_evalFrom_reverse {α : Type u} {σ : Type v} {M : NFA α σ} {x : List α} {S S' : Set σ} (h : Disjoint S (M.reverse.evalFrom S' x)) : Disjoint S' (M.evalFrom S x.reverse)

theorem NFA.disjoint_evalFrom_reverse_iff {α : Type u} {σ : Type v} {M : NFA α σ} {x : List α} {S S' : Set σ} : Disjoint S (M.reverse.evalFrom S' x) ↔ Disjoint S' (M.evalFrom S x.reverse)

@[simp]

theorem NFA.mem_accepts_reverse {α : Type u} {σ : Type v} {M : NFA α σ} {x : List α} : x ∈ M.reverse.accepts ↔ x.reverse ∈ M.accepts

theorem Language.IsRegular.reverse {α : Type u} {L : Language α} (h : L.IsRegular) : L.reverse.IsRegular

theorem Language.IsRegular.of_reverse {α : Type u} {L : Language α} (h : L.reverse.IsRegular) : L.IsRegular

@[simp]

theorem Language.isRegular_reverse_iff {α : Type u} {L : Language α} : L.reverse.IsRegular ↔ L.IsRegular

Regular languages are closed under reversal.