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.
- step : σ → α → σ
- start : σ
- accept : set σ
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
).
Instances for DFA
- DFA.has_sizeof_inst
- DFA.inhabited
@[protected, instance]
Equations
- DFA.inhabited = {default := {step := λ (_x : σ) (_x : α), inhabited.default, start := inhabited.default _inst_1, accept := ∅}}
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 σ ≤ x.length)
(hx : M.eval_from s x = t) :