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.
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
- ε_NFA.has_sizeof_inst
- ε_NFA.has_zero
- ε_NFA.has_one
- ε_NFA.inhabited
- base : ∀ {α : Type u} {σ : Type v} {M : ε_NFA α σ} {S : set σ} (s : σ), s ∈ S → M.ε_closure S s
- step : ∀ {α : Type u} {σ : Type v} {M : ε_NFA α σ} {S : set σ} (s t : σ), t ∈ M.step s option.none → M.ε_closure S s → M.ε_closure S t
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.
Regex-like operations #
Equations
- ε_NFA.inhabited = {default := 0}