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 : σ → α → σ
A transition function from state to state labelled by the alphabet.
- start : σ
- accept : Set σ
Set of acceptance states.