Deterministic Finite Automata #
This file contains the definition of a Deterministic Finite Automaton (DFA), a state machine which
determines whether a string (implemented as a list over an arbitrary alphabet) is in a regular set
in linear time.
Note that this definition allows for Automaton with infinite states, a Fintype
instance must be
supplied for true DFA's.
A DFA 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
).
- step : σ → α → σ
A transition function from state to state labelled by the alphabet.
- start : σ
Starting state.
- accept : Set σ
Set of acceptance states.
Instances For
M.evalFrom s x
evaluates M
with input x
starting from the state s
.
Equations
- M.evalFrom start = List.foldl M.step start
Instances For
theorem
DFA.evalFrom_split
{α : Type u}
{σ : Type v}
(M : DFA α σ)
[Fintype σ]
{x : List α}
{s : σ}
{t : σ}
(hlen : Fintype.card σ ≤ x.length)
(hx : M.evalFrom s x = t)
: