Nondeterministic Finite Automata #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file contains the definition of a 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. We show that DFA's are equivalent to NFA's however the construction from NFA to DFA uses an exponential number of states. Note that this definition allows for Automaton with infinite states, a
fintypeinstance must be supplied for true NFA's.
An NFA is a set of states (
σ), a transition function from state to state labelled by the
step), a starting state (
start) and a set of acceptance states (
Note the transition function sends a state to a
set of states. These are the states that it
may be sent to.
M.to_DFA is an
DFA constructed from a
M using the subset construction. The
states is the type of
M.state and the step function is
M.to_NFA is an
NFA constructed from a
M by using the same start and accept
states and a transition function which sends
s with input
a to the singleton
M.step s a.