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.
M.eval_from s x
evaluates M
with input x
starting from the state s
.
Equations
- M.eval_from start = list.foldl M.step start
theorem
DFA.eval_from_split
{α : Type u}
{σ : Type v}
(M : DFA α σ)
[fintype σ]
{x : list α}
{s t : σ}
(hlen : fintype.card σ + 1 ≤ x.length)
(hx : M.eval_from s x = t) :