mathlib3 documentation

computability.epsilon_NFA

Epsilon 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 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.

Instances for ε_NFA
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.

@[simp]
theorem ε_NFA.subset_ε_closure {α : Type u} {σ : Type v} (M : ε_NFA α σ) (S : set σ) :
@[simp]
theorem ε_NFA.ε_closure_empty {α : Type u} {σ : Type v} (M : ε_NFA α σ) :
@[simp]
theorem ε_NFA.ε_closure_univ {α : Type u} {σ : Type v} (M : ε_NFA α σ) :
def ε_NFA.step_set {α : Type u} {σ : Type v} (M : ε_NFA α σ) (S : set σ) (a : α) :
set σ

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

Equations
@[simp]
theorem ε_NFA.mem_step_set_iff {α : Type u} {σ : Type v} {M : ε_NFA α σ} {S : set σ} {s : σ} {a : α} :
s M.step_set S a (t : σ) (H : t S), s M.ε_closure (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 through 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 (M.ε_closure 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
@[simp]
theorem ε_NFA.eval_from_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.

Equations
@[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 : α) :
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

Conversions between ε_NFA and NFA #

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} * has_kstar.kstar {b} * {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 α σ) :

Regex-like operations #

@[protected, instance]
def ε_NFA.has_zero {α : Type u} {σ : Type v} :
Equations
@[protected, instance]
def ε_NFA.has_one {α : Type u} {σ : Type v} :
has_one (ε_NFA α σ)
Equations
@[protected, instance]
def ε_NFA.inhabited {α : Type u} {σ : Type v} :
Equations
@[simp]
theorem ε_NFA.step_zero {α : Type u} {σ : Type v} (s : σ) (a : option α) :
0.step s a =
@[simp]
theorem ε_NFA.step_one {α : Type u} {σ : Type v} (s : σ) (a : option α) :
1.step s a =
@[simp]
theorem ε_NFA.start_zero {α : Type u} {σ : Type v} :
@[simp]
theorem ε_NFA.start_one {α : Type u} {σ : Type v} :
@[simp]
theorem ε_NFA.accept_zero {α : Type u} {σ : Type v} :
@[simp]
theorem ε_NFA.accept_one {α : Type u} {σ : Type v} :