# Documentation

Mathlib.Computability.EpsilonNFA

# 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 ε-transitions, 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)
• step : σSet σ
• start : Set σ
• accept : Set σ

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.

Instances For
inductive εNFA.εClosure {α : Type u} {σ : Type v} (M : εNFA α σ) (S : 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.

Instances For
@[simp]
theorem εNFA.subset_εClosure {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) :
S
@[simp]
theorem εNFA.εClosure_empty {α : Type u} {σ : Type v} (M : εNFA α σ) :
@[simp]
theorem εNFA.εClosure_univ {α : Type u} {σ : Type v} (M : εNFA α σ) :
εNFA.εClosure M Set.univ = Set.univ
def εNFA.stepSet {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) (a : α) :
Set σ

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

Instances For
@[simp]
theorem εNFA.mem_stepSet_iff {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} {s : σ} {a : α} :
s εNFA.stepSet M S a t, t S s εNFA.εClosure M (εNFA.step M t (some a))
@[simp]
theorem εNFA.stepSet_empty {α : Type u} {σ : Type v} {M : εNFA α σ} (a : α) :
def εNFA.evalFrom {α : Type u} {σ : Type v} (M : εNFA α σ) (start : Set σ) :
List αSet σ

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

Instances For
@[simp]
theorem εNFA.evalFrom_nil {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) :
@[simp]
theorem εNFA.evalFrom_singleton {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) (a : α) :
@[simp]
theorem εNFA.evalFrom_append_singleton {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) (x : List α) (a : α) :
εNFA.evalFrom M S (x ++ [a]) = εNFA.stepSet M () a
@[simp]
theorem εNFA.evalFrom_empty {α : Type u} {σ : Type v} (M : εNFA α σ) (x : List α) :
def εNFA.eval {α : Type u} {σ : Type v} (M : εNFA α σ) :
List αSet σ

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

Instances For
@[simp]
theorem εNFA.eval_nil {α : Type u} {σ : Type v} (M : εNFA α σ) :
@[simp]
theorem εNFA.eval_singleton {α : Type u} {σ : Type v} (M : εNFA α σ) (a : α) :
@[simp]
theorem εNFA.eval_append_singleton {α : Type u} {σ : Type v} (M : εNFA α σ) (x : List α) (a : α) :
εNFA.eval M (x ++ [a]) = εNFA.stepSet M () 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.

Instances For

### Conversions between εNFA and NFA#

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

M.toNFA is an NFA constructed from an εNFA M.

Instances For
@[simp]
theorem εNFA.toNFA_evalFrom_match {α : Type u} {σ : Type v} (M : εNFA α σ) (start : Set σ) :
@[simp]
theorem εNFA.toNFA_correct {α : Type u} {σ : Type v} (M : εNFA α σ) :
theorem εNFA.pumping_lemma {α : Type u} {σ : Type v} (M : εNFA α σ) [] {x : List α} (hx : ) (hlen : Fintype.card (Set σ) ) :
a b c, x = a ++ b ++ c Fintype.card (Set σ) b [] {a} * KStar.kstar {b} * {c}
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.

Instances For
@[simp]
theorem NFA.toεNFA_εClosure {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) :
= S
@[simp]
theorem NFA.toεNFA_evalFrom_match {α : Type u} {σ : Type v} (M : NFA α σ) (start : Set σ) :
εNFA.evalFrom () start = NFA.evalFrom M start
@[simp]
theorem NFA.toεNFA_correct {α : Type u} {σ : Type v} (M : NFA α σ) :

### Regex-like operations #

instance εNFA.instZeroεNFA {α : Type u} {σ : Type v} :
Zero (εNFA α σ)
instance εNFA.instOneεNFA {α : Type u} {σ : Type v} :
One (εNFA α σ)
instance εNFA.instInhabitedεNFA {α : Type u} {σ : Type v} :
@[simp]
theorem εNFA.step_zero {α : Type u} {σ : Type v} (s : σ) (a : ) :
@[simp]
theorem εNFA.step_one {α : Type u} {σ : Type v} (s : σ) (a : ) :
@[simp]
theorem εNFA.start_zero {α : Type u} {σ : Type v} :
0.start =
@[simp]
theorem εNFA.start_one {α : Type u} {σ : Type v} :
1.start = Set.univ
@[simp]
theorem εNFA.accept_zero {α : Type u} {σ : Type v} :
0.accept =
@[simp]
theorem εNFA.accept_one {α : Type u} {σ : Type v} :
1.accept = Set.univ