mathlib3 documentation

computability.NFA

Nondeterministic Finite Automata #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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 starting state (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.

Instances for NFA
@[protected, instance]
def NFA.inhabited {α : Type u} {σ : Type v} :
inhabited (NFA α σ)
Equations
def NFA.step_set {α : Type u} {σ : Type v} (M : NFA α σ) (S : set σ) (a : α) :
set σ

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

Equations
theorem NFA.mem_step_set {α : Type u} {σ : Type v} (M : NFA α σ) (s : σ) (S : set σ) (a : α) :
s M.step_set S a (t : σ) (H : t S), s M.step t a
@[simp]
theorem NFA.step_set_empty {α : Type u} {σ : Type v} (M : NFA α σ) (a : α) :
def NFA.eval_from {α : Type u} {σ : Type v} (M : NFA α σ) (start : set σ) :
list α set σ

M.eval_from S x computes all possible paths though M with input x starting at an element of S.

Equations
@[simp]
theorem NFA.eval_from_nil {α : Type u} {σ : Type v} (M : NFA α σ) (S : set σ) :
@[simp]
theorem NFA.eval_from_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (S : set σ) (a : α) :
M.eval_from S [a] = M.step_set S a
@[simp]
theorem NFA.eval_from_append_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (S : set σ) (x : list α) (a : α) :
M.eval_from S (x ++ [a]) = M.step_set (M.eval_from 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
@[simp]
theorem NFA.eval_nil {α : Type u} {σ : Type v} (M : NFA α σ) :
@[simp]
theorem NFA.eval_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (a : α) :
M.eval [a] = M.step_set M.start a
@[simp]
theorem NFA.eval_append_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (x : list α) (a : α) :
M.eval (x ++ [a]) = M.step_set (M.eval x) a
def NFA.accepts {α : Type u} {σ : Type v} (M : NFA α σ) :

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

Equations
def NFA.to_DFA {α : Type u} {σ : Type v} (M : NFA α σ) :
DFA α (set σ)

M.to_DFA is an DFA constructed from a NFA M using the subset construction. The states is the type of sets of M.state and the step function is M.step_set.

Equations
@[simp]
theorem NFA.to_DFA_correct {α : Type u} {σ : Type v} (M : NFA α σ) :
theorem NFA.pumping_lemma {α : Type u} {σ : Type v} (M : NFA α σ) [fintype σ] {x : list α} (hx : x M.accepts) (hlen : fintype.card (set σ) x.length) :
(a b c : list α), x = a ++ b ++ c a.length + b.length fintype.card (set σ) b list.nil {a} * has_kstar.kstar {b} * {c} M.accepts
def DFA.to_NFA {α : Type u} {σ' : Type v} (M : DFA α σ') :
NFA α σ'

M.to_NFA 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
@[simp]
theorem DFA.to_NFA_eval_from_match {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) (s : list α) :
M.to_NFA.eval_from {start} s = {M.eval_from start s}
@[simp]
theorem DFA.to_NFA_correct {α : Type u} {σ : Type v} (M : DFA α σ) :