mathlib3 documentation

computability.DFA

Deterministic 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 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)
  • 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
@[protected, instance]
def DFA.inhabited {α : Type u} {σ : Type v} [inhabited σ] :
inhabited (DFA α σ)
Equations
def DFA.eval_from {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) :
list α σ

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

Equations
@[simp]
theorem DFA.eval_from_nil {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) :
@[simp]
theorem DFA.eval_from_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (a : α) :
M.eval_from s [a] = M.step s a
@[simp]
theorem DFA.eval_from_append_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (x : list α) (a : α) :
M.eval_from s (x ++ [a]) = M.step (M.eval_from 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
@[simp]
theorem DFA.eval_nil {α : Type u} {σ : Type v} (M : DFA α σ) :
@[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.eval_from_of_append {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) (x y : list α) :
M.eval_from start (x ++ y) = M.eval_from (M.eval_from 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
theorem DFA.mem_accepts {α : Type u} {σ : Type v} (M : DFA α σ) (x : list α) :
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) :
(q : σ) (a b c : list α), x = a ++ b ++ c a.length + b.length fintype.card σ b list.nil M.eval_from s a = q M.eval_from q b = q M.eval_from q c = t
theorem DFA.eval_from_of_pow {α : Type u} {σ : Type v} (M : DFA α σ) {x y : list α} {s : σ} (hx : M.eval_from s x = s) (hy : y has_kstar.kstar {x}) :
M.eval_from s y = s
theorem DFA.pumping_lemma {α : Type u} {σ : Type v} (M : DFA α σ) [fintype σ] {x : list α} (hx : x M.accepts) (hlen : fintype.card σ x.length) :
(a b c : list α), x = a ++ b ++ c a.length + b.length fintype.card σ b list.nil {a} * has_kstar.kstar {b} * {c} M.accepts