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.

instance DFA.instInhabitedDFA {α : Type u} {σ : Type v} [Inhabited σ] : Inhabited (DFA α σ)

Equations

• DFA.instInhabitedDFA = { 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

• DFA.evalFrom M start = List.foldl M.step start

@[simp]

theorem DFA.evalFrom_nil {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) : DFA.evalFrom M s [] = s

@[simp]

theorem DFA.evalFrom_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (a : α) : DFA.evalFrom M s [a] = M.step s a

@[simp]

theorem DFA.evalFrom_append_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (s : σ) (x : List α) (a : α) : DFA.evalFrom M s (x ++ [a]) = M.step (DFA.evalFrom M 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

• DFA.eval M = DFA.evalFrom M M.start

@[simp]

theorem DFA.eval_nil {α : Type u} {σ : Type v} (M : DFA α σ) : DFA.eval M [] = M.start

@[simp]

theorem DFA.eval_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (a : α) : DFA.eval M [a] = M.step M.start a

@[simp]

theorem DFA.eval_append_singleton {α : Type u} {σ : Type v} (M : DFA α σ) (x : List α) (a : α) : DFA.eval M (x ++ [a]) = M.step (DFA.eval M x) a

theorem DFA.evalFrom_of_append {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) (x : List α) (y : List α) : DFA.evalFrom M start (x ++ y) = DFA.evalFrom M (DFA.evalFrom M start x) y

def DFA.accepts {α : Type u} {σ : Type v} (M : DFA α σ) : Language α

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

Equations

• DFA.accepts M = {x : List α | DFA.eval M x ∈ M.accept}

theorem DFA.mem_accepts {α : Type u} {σ : Type v} (M : DFA α σ) (x : List α) : x ∈ DFA.accepts M ↔ DFA.evalFrom M M.start x ∈ M.accept

theorem DFA.evalFrom_split {α : Type u} {σ : Type v} (M : DFA α σ) [Fintype σ] {x : List α} {s : σ} {t : σ} (hlen : Fintype.card σ ≤ List.length x) (hx : DFA.evalFrom M s x = t) : ∃ (q : σ) (a : List α) (b : List α) (c : List α), x = a ++ b ++ c ∧ List.length a + List.length b ≤ Fintype.card σ ∧ b ≠ [] ∧ DFA.evalFrom M s a = q ∧ DFA.evalFrom M q b = q ∧ DFA.evalFrom M q c = t

theorem DFA.evalFrom_of_pow {α : Type u} {σ : Type v} (M : DFA α σ) {x : List α} {y : List α} {s : σ} (hx : DFA.evalFrom M s x = s) (hy : y ∈ KStar.kstar {x}) : DFA.evalFrom M s y = s

theorem DFA.pumping_lemma {α : Type u} {σ : Type v} (M : DFA α σ) [Fintype σ] {x : List α} (hx : x ∈ DFA.accepts M) (hlen : Fintype.card σ ≤ List.length x) : ∃ (a : List α) (b : List α) (c : List α), x = a ++ b ++ c ∧ List.length a + List.length b ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * KStar.kstar {b} * {c} ≤ DFA.accepts M