Documentation

Mathlib.Computability.EpsilonNFA

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.

Instances For
    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 σ}, sS, M.εClosure S s
    • step: ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} (s t : σ), t M.step s noneM.εClosure S sM.εClosure S t
    Instances For
      @[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
      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 = sS, M.εClosure (M.step s (some a))
      Instances For
        @[simp]
        theorem εNFA.mem_stepSet_iff {α : Type u} {σ : Type v} {M : εNFA α σ} {S : Set σ} {s : σ} {a : α} :
        s M.stepSet S a tS, 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)
        Instances For
          @[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 =
          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
          Instances For
            @[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 α σ) :

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

            Equations
            • M.accepts = {x : List α | SM.accept, S M.eval x}
            Instances For

              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 }
              Instances For
                @[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 }
                Instances For
                  @[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 : Option α) => , start := , accept := } }
                  instance εNFA.instOne {α : Type u} {σ : Type v} :
                  One (εNFA α σ)
                  Equations
                  • εNFA.instOne = { one := { step := fun (x : σ) (x : Option α) => , start := Set.univ, accept := Set.univ } }
                  instance εNFA.instInhabited {α : Type u} {σ : Type v} :
                  Equations
                  • εNFA.instInhabited = { default := 0 }
                  @[simp]
                  theorem εNFA.step_zero {α : Type u} {σ : Type v} (s : σ) (a : Option α) :
                  @[simp]
                  theorem εNFA.step_one {α : Type u} {σ : Type v} (s : σ) (a : Option α) :
                  @[simp]
                  theorem εNFA.start_zero {α : Type u} {σ : Type v} :
                  @[simp]
                  theorem εNFA.start_one {α : Type u} {σ : Type v} :
                  εNFA.start 1 = Set.univ
                  @[simp]
                  theorem εNFA.accept_zero {α : Type u} {σ : Type v} :
                  @[simp]
                  theorem εNFA.accept_one {α : Type u} {σ : Type v} :
                  εNFA.accept 1 = Set.univ