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.

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

source
@[simp]
theorem ε_NFA.subset_ε_closure {α : Type u} {σ : Type v} (M : ε_NFA α σ) (S : set σ) :
S ⊆ M.ε_closure S
source
@[simp]
theorem ε_NFA.ε_closure_empty {α : Type u} {σ : Type v} (M : ε_NFA α σ) :
M.ε_closure ∅ = ∅
source
@[simp]
theorem ε_NFA.ε_closure_univ {α : Type u} {σ : Type v} (M : ε_NFA α σ) :
M.ε_closure set.univ = set.univ
source
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
source
@[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)
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 through 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 = M.ε_closure 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 (M.ε_closure 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
@[simp]
theorem ε_NFA.eval_from_empty {α : Type u} {σ : Type v} (M : ε_NFA α σ) (x : list α) :
M.eval_from ∅ x = ∅
source
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
source
@[simp]
theorem ε_NFA.eval_nil {α : Type u} {σ : Type v} (M : ε_NFA α σ) :
M.eval list.nil = M.ε_closure M.start
source
@[simp]
theorem ε_NFA.eval_singleton {α : Type u} {σ : Type v} (M : ε_NFA α σ) (a : α) :
M.eval [a] = M.step_set (M.ε_closure 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

Conversions between ε_NFA and NFA #

source
def ε_NFA.to_NFA {α : Type u} {σ : Type v} (M : ε_NFA α σ) :
NFA α σ

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

Equations
source
@[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
source
@[simp]
theorem ε_NFA.to_NFA_correct {α : Type u} {σ : Type v} (M : ε_NFA α σ) :
M.to_NFA.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 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
source
@[simp]
theorem NFA.to_ε_NFA_ε_closure {α : Type u} {σ : Type v} (M : NFA α σ) (S : set σ) :
M.to_ε_NFA.ε_closure S = S
source
@[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
source
@[simp]
theorem NFA.to_ε_NFA_correct {α : Type u} {σ : Type v} (M : NFA α σ) :
M.to_ε_NFA.accepts = M.accepts

Regex-like operations #

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