Epsilon Nondeterministic Finite Automata

This file contains the definition of an epsilon 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, also having access to ε-transitions, which can be followed without reading a character. Since this definition allows for automata with infinite states, a Fintype instance must be supplied for true εNFA's.

structure εNFA (α : Type u) (σ : Type v) : Type (max u v)

An εNFA 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). Note the transition function sends a state to a Set of states and can make ε-transitions by inputting none. Since this definition allows for Automata with infinite states, a Fintype instance must be supplied for true εNFA's.

• step : σ → Option α → Set σ

  Transition function. The automaton is rendered non-deterministic by this transition function returning Set σ (rather than σ), and ε-transitions are made possible by taking Option α (rather than α).

• start : Set σ

  Starting states.

• accept : Set σ

  Set of acceptance states.

inductive εNFA.εClosure {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) : Set σ

The εClosure of a set is the set of states which can be reached by taking a finite string of ε-transitions from an element of the set.

• base {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} (s : σ) : s ∈ S → M.εClosure S s
• step {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} (s t : σ) : t ∈ M.step s none → M.εClosure S s → M.εClosure S t

@[simp]

theorem εNFA.subset_εClosure {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) : S ⊆ M.εClosure S

@[simp]

theorem εNFA.εClosure_empty {α : Type u} {σ : Type v} (M : εNFA α σ) : M.εClosure ∅ = ∅

@[simp]

theorem εNFA.εClosure_univ {α : Type u} {σ : Type v} (M : εNFA α σ) : M.εClosure Set.univ = Set.univ

theorem εNFA.mem_εClosure_iff_exists {α : Type u} {σ : Type v} (M : εNFA α σ) {S : Set σ} {s : σ} : s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t}

def εNFA.stepSet {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) (a : α) : Set σ

M.stepSet S a is the union of the ε-closure of M.step s a for all s ∈ S.

Equations

• M.stepSet S a = ⋃ s ∈ S, M.εClosure (M.step s (some a))

@[simp]

theorem εNFA.mem_stepSet_iff {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} {s : σ} {a : α} : s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))

@[simp]

theorem εNFA.stepSet_empty {α : Type u} {σ : Type v} {M : εNFA α σ} (a : α) : M.stepSet ∅ a = ∅

def εNFA.evalFrom {α : Type u} {σ : Type v} (M : εNFA α σ) (start : Set σ) : List α → Set σ

M.evalFrom S x computes all possible paths through M with input x starting at an element of S.

Equations

• M.evalFrom start = List.foldl M.stepSet (M.εClosure start)

@[simp]

theorem εNFA.evalFrom_nil {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) : M.evalFrom S [] = M.εClosure S

@[simp]

theorem εNFA.evalFrom_singleton {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) (a : α) : M.evalFrom S [a] = M.stepSet (M.εClosure S) a

@[simp]

theorem εNFA.evalFrom_append_singleton {α : Type u} {σ : Type v} (M : εNFA α σ) (S : Set σ) (x : List α) (a : α) : M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a

@[simp]

theorem εNFA.evalFrom_empty {α : Type u} {σ : Type v} (M : εNFA α σ) (x : List α) : M.evalFrom ∅ x = ∅

theorem εNFA.mem_evalFrom_iff_exists {α : Type u} {σ : Type v} (M : εNFA α σ) {s : σ} {S : Set σ} {x : List α} : s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x

def εNFA.eval {α : Type u} {σ : Type v} (M : εNFA α σ) : List α → Set σ

M.eval x computes all possible paths through M with input x starting at an element of M.start.

Equations

• M.eval = M.evalFrom M.start

@[simp]

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

@[simp]

theorem εNFA.eval_singleton {α : Type u} {σ : Type v} (M : εNFA α σ) (a : α) : M.eval [a] = M.stepSet (M.εClosure M.start) a

@[simp]

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

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

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

Equations

• M.accepts = {x : List α | ∃ S ∈ M.accept, S ∈ M.eval x}

inductive εNFA.IsPath {α : Type u} {σ : Type v} (M : εNFA α σ) : σ → σ → List (Option α) → Prop

M.IsPath represents a traversal in M from a start state to an end state by following a list of transitions in order.

• nil {α : Type u} {σ : Type v} {M : εNFA α σ} (s : σ) : M.IsPath s s []
• cons {α : Type u} {σ : Type v} {M : εNFA α σ} (t s u : σ) (a : Option α) (x : List (Option α)) : t ∈ M.step s a → M.IsPath t u x → M.IsPath s u (a :: x)

theorem εNFA.isPath_iff {α : Type u} {σ : Type v} (M : εNFA α σ) (a✝ a✝¹ : σ) (a✝² : List (Option α)) : M.IsPath a✝ a✝¹ a✝² ↔ a✝¹ = a✝ ∧ a✝² = [] ∨ ∃ (t : σ) (a : Option α) (x : List (Option α)), t ∈ M.step a✝ a ∧ M.IsPath t a✝¹ x ∧ a✝² = a :: x

@[simp]

theorem εNFA.isPath_nil {α : Type u} {σ : Type v} (M : εNFA α σ) {s t : σ} : M.IsPath s t [] ↔ s = t

theorem εNFA.IsPath.eq_of_nil {α : Type u} {σ : Type v} (M : εNFA α σ) {s t : σ} : M.IsPath s t [] → s = t

Alias of the forward direction of εNFA.isPath_nil.

@[simp]

theorem εNFA.isPath_singleton {α : Type u} {σ : Type v} (M : εNFA α σ) {s t : σ} {a : Option α} : M.IsPath s t [a] ↔ t ∈ M.step s a

theorem εNFA.IsPath.singleton {α : Type u} {σ : Type v} (M : εNFA α σ) {s t : σ} {a : Option α} : t ∈ M.step s a → M.IsPath s t [a]

Alias of the reverse direction of εNFA.isPath_singleton.

theorem εNFA.isPath_append {α : Type u} {σ : Type v} (M : εNFA α σ) {s u : σ} {x y : List (Option α)} : M.IsPath s u (x ++ y) ↔ ∃ (t : σ), M.IsPath s t x ∧ M.IsPath t u y

theorem εNFA.mem_εClosure_iff_exists_path {α : Type u} {σ : Type v} (M : εNFA α σ) {s₁ s₂ : σ} : s₂ ∈ M.εClosure {s₁} ↔ ∃ (n : ℕ), M.IsPath s₁ s₂ (List.replicate n none)

theorem εNFA.mem_evalFrom_iff_exists_path {α : Type u} {σ : Type v} (M : εNFA α σ) {s₁ s₂ : σ} {x : List α} : s₂ ∈ M.evalFrom {s₁} x ↔ ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'

theorem εNFA.mem_accepts_iff_exists_path {α : Type u} {σ : Type v} (M : εNFA α σ) {x : List α} : x ∈ M.accepts ↔ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'

Conversions between εNFA and NFA

def εNFA.toNFA {α : Type u} {σ : Type v} (M : εNFA α σ) : NFA α σ

M.toNFA is an NFA constructed from an εNFA M.

Equations

• M.toNFA = { step := fun (S : σ) (a : α) => M.εClosure (M.step S (some a)), start := M.εClosure M.start, accept := M.accept }

@[simp]

theorem εNFA.toNFA_evalFrom_match {α : Type u} {σ : Type v} (M : εNFA α σ) (start : Set σ) : M.toNFA.evalFrom (M.εClosure start) = M.evalFrom start

@[simp]

theorem εNFA.toNFA_correct {α : Type u} {σ : Type v} (M : εNFA α σ) : M.toNFA.accepts = M.accepts

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

def NFA.toεNFA {α : Type u} {σ : Type v} (M : NFA α σ) : εNFA α σ

M.toεNFA is an εNFA constructed from an NFA M by using the same start and accept states and transition functions.

Equations

• M.toεNFA = { step := fun (s : σ) (a : Option α) => a.casesOn' ∅ fun (a : α) => M.step s a, start := M.start, accept := M.accept }

@[simp]

theorem NFA.toεNFA_εClosure {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) : M.toεNFA.εClosure S = S

@[simp]

theorem NFA.toεNFA_evalFrom_match {α : Type u} {σ : Type v} (M : NFA α σ) (start : Set σ) : M.toεNFA.evalFrom start = M.evalFrom start

@[simp]

theorem NFA.toεNFA_correct {α : Type u} {σ : Type v} (M : NFA α σ) : M.toεNFA.accepts = M.accepts

Regex-like operations

instance εNFA.instZero {α : Type u} {σ : Type v} : Zero (εNFA α σ)

Equations

• εNFA.instZero = { zero := { step := fun (x : σ) (x_1 : Option α) => ∅, start := ∅, accept := ∅ } }

instance εNFA.instOne {α : Type u} {σ : Type v} : One (εNFA α σ)

Equations

• εNFA.instOne = { one := { step := fun (x : σ) (x_1 : Option α) => ∅, start := Set.univ, accept := Set.univ } }

instance εNFA.instInhabited {α : Type u} {σ : Type v} : Inhabited (εNFA α σ)

Equations

• εNFA.instInhabited = { default := 0 }

@[simp]

theorem εNFA.step_zero {α : Type u} {σ : Type v} (s : σ) (a : Option α) : step 0 s a = ∅

@[simp]

theorem εNFA.step_one {α : Type u} {σ : Type v} (s : σ) (a : Option α) : step 1 s a = ∅

@[simp]

theorem εNFA.start_zero {α : Type u} {σ : Type v} : start 0 = ∅

@[simp]

theorem εNFA.start_one {α : Type u} {σ : Type v} : start 1 = Set.univ

@[simp]

theorem εNFA.accept_zero {α : Type u} {σ : Type v} : accept 0 = ∅

@[simp]

theorem εNFA.accept_one {α : Type u} {σ : Type v} : accept 1 = Set.univ