# 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.

structure DFA (α : Type u) (σ : Type v) :
Type (max u v)

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
instance DFA.instInhabited {α : Type u} {σ : Type v} [] :
Inhabited (DFA α σ)
Equations
• DFA.instInhabited = { default := { step := fun (x : σ) (x : α) => default, start := default, accept := } }
def DFA.evalFrom {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) :
List ασ

M.evalFrom s x evaluates M with input x starting from the state s.

Equations
Instances For
@[simp]
theorem DFA.evalFrom_nil {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) :
M.evalFrom s [] = s
@[simp]
theorem DFA.evalFrom_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (a : α) :
M.evalFrom s [a] = M.step s a
@[simp]
theorem DFA.evalFrom_append_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (x : List α) (a : α) :
M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a
def DFA.eval {α : Type u} {σ : Type v} (M : DFA α σ) :
List ασ

M.eval x evaluates M with input x starting from the state M.start.

Equations
• M.eval = M.evalFrom M.start
Instances For
@[simp]
theorem DFA.eval_nil {α : Type u} {σ : Type v} (M : DFA α σ) :
M.eval [] = M.start
@[simp]
theorem DFA.eval_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (a : α) :
M.eval [a] = M.step M.start a
@[simp]
theorem DFA.eval_append_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (x : List α) (a : α) :
M.eval (x ++ [a]) = M.step (M.eval x) a
theorem DFA.evalFrom_of_append {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) (x : List α) (y : List α) :
M.evalFrom start (x ++ y) = M.evalFrom (M.evalFrom start x) y
def DFA.accepts {α : Type u} {σ : Type v} (M : DFA α σ) :

M.accepts is the language of x such that M.eval x is an accept state.

Equations
• M.accepts = {x : List α | M.eval x M.accept}
Instances For
theorem DFA.mem_accepts {α : Type u} {σ : Type v} (M : DFA α σ) (x : List α) :
x M.accepts M.evalFrom M.start x M.accept
theorem DFA.evalFrom_split {α : Type u} {σ : Type v} (M : DFA α σ) [] {x : List α} {s : σ} {t : σ} (hlen : x.length) (hx : M.evalFrom s x = t) :
∃ (q : σ) (a : List α) (b : List α) (c : List α), x = a ++ b ++ c a.length + b.length b [] M.evalFrom s a = q M.evalFrom q b = q M.evalFrom q c = t
theorem DFA.evalFrom_of_pow {α : Type u} {σ : Type v} (M : DFA α σ) {x : List α} {y : List α} {s : σ} (hx : M.evalFrom s x = s) (hy : y KStar.kstar {x}) :
M.evalFrom s y = s
theorem DFA.pumping_lemma {α : Type u} {σ : Type v} (M : DFA α σ) [] {x : List α} (hx : x M.accepts) (hlen : x.length) :
∃ (a : List α) (b : List α) (c : List α), x = a ++ b ++ c a.length + b.length b [] {a} * KStar.kstar {b} * {c} M.accepts