mathlib documentation

computability.epsilon_NFA

Epsilon Nondeterministic Finite Automata #

This file contains the definition of an epsilon 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, also having access to ε-transitons, which can be followed without reading a character. Since this definition allows for automata 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 and can make ε-transitions by inputing none. Since this definition allows for Automata with infinite states, a fintype instance must be supplied for true ε_NFA's.

@[instance]
def ε_NFA.inhabited {α : Type u} {σ : Type v} :
Equations
inductive ε_NFA.ε_closure {α : Type u} {σ : Type v} (M : ε_NFA α σ) :
set σset σ

The ε_closure of a set is the set of states which can be reached by taking a finite string of ε-transitions from an element of the set

def ε_NFA.step_set {α : Type u} {σ : Type v} (M : ε_NFA α σ) :
set σα → set σ

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

Equations
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
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
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_NFA {α : Type u} {σ : Type v} (M : ε_NFA α σ) :
NFA α σ

M.to_NFA is an NFA constructed from an ε_NFA M.

Equations
@[simp]
theorem ε_NFA.to_NFA_eval_from_match {α : Type u} {σ : Type v} (M : ε_NFA α σ) (start : set σ) :
M.to_NFA.eval_from (M.ε_closure start) = M.eval_from start
@[simp]
theorem ε_NFA.to_NFA_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} * {b}.star) * {c} M.accepts
def NFA.to_ε_NFA {α : Type u} {σ : Type v} (M : NFA α σ) :
ε_NFA α σ

M.to_ε_NFA is an ε_NFA constructed from an NFA M by using the same start and accept states and transition functions.

Equations
@[simp]
theorem NFA.to_ε_NFA_ε_closure {α : Type u} {σ : Type v} (M : NFA α σ) (S : set σ) :
@[simp]
theorem NFA.to_ε_NFA_eval_from_match {α : Type u} {σ : Type v} (M : NFA α σ) (start : set σ) :
M.to_ε_NFA.eval_from start = M.eval_from start
@[simp]
theorem NFA.to_ε_NFA_correct {α : Type u} {σ : Type v} (M : NFA α σ) :