Nondeterministic Finite Automata

This file contains the definition of a Nondeterministic Finite Automaton (NFA), a state machine which determines whether a string (implemented as a list over an arbitrary alphabet) is in a regular set by evaluating the string over every possible path. We show that DFA's are equivalent to NFA's however the construction from NFA to DFA uses an exponential number of states. Note that this definition allows for Automaton with infinite states; a Fintype instance must be supplied for true NFA's.

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

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

Equations

• NFA.instInhabited = { default := { step := fun (x : σ) (x : α) => ∅, start := ∅, accept := ∅ } }

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.

Equations

• M.stepSet S a = ⋃ s ∈ S, M.step s a

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 = ∅

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.

Equations

• M.evalFrom S = List.foldl M.stepSet 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_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

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.

Equations

• M.eval = M.evalFrom 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.

Equations

• M.accepts = {x : List α | ∃ S ∈ M.accept, S ∈ 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

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.

Equations

• M.toDFA = { step := M.stepSet, start := M.start, accept := {S : Set σ | ∃ s ∈ S, s ∈ M.accept} }

@[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.

Equations

• M.toNFA = { step := fun (s : σ) (a : α) => {M.step s a}, start := {M.start}, accept := M.accept }

@[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.

Equations

• M.reverse = { step := fun (s : σ) (a : α) => {s' : σ | s ∈ M.step s' a}, start := M.accept, 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_accept {α : Type u} {σ : Type v} (M : NFA α σ) : M.reverse.accept = M.start

@[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.