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.

source
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
source
@[protected, instance]
def NFA.inhabited {α : Type u} {σ : Type v} :
inhabited (NFA α σ)
Equations
source
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
source
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
source
@[simp]
theorem NFA.step_set_empty {α : Type u} {σ : Type v} (M : NFA α σ) (a : α) :
M.step_set ∅ a = ∅
source
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
source
@[simp]
theorem NFA.eval_from_nil {α : Type u} {σ : Type v} (M : NFA α σ) (S : set σ) :
M.eval_from S list.nil = S
source
@[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
source
@[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
source
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
source
@[simp]
theorem NFA.eval_nil {α : Type u} {σ : Type v} (M : NFA α σ) :
M.eval list.nil = M.start
source
@[simp]
theorem NFA.eval_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (a : α) :
M.eval [a] = M.step_set M.start a
source
@[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
source
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
source
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
source
@[simp]
theorem NFA.to_DFA_correct {α : Type u} {σ : Type v} (M : NFA α σ) :
M.to_DFA.accepts = M.accepts
source
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
source
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
source
@[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}
source
@[simp]
theorem DFA.to_NFA_correct {α : Type u} {σ : Type v} (M : DFA α σ) :
M.to_NFA.accepts = M.accepts