Documentation

Mathlib.Computability.NFA

Nondeterministic Finite Automata #

This file contains the definition of a 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. We show that DFA's are equivalent to NFA's however the construction from NFA to DFA uses an exponential number of states. Note that this definition allows for Automaton 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 set of starting states (start) and a set of acceptance states (accept). Note the transition function sends a state to a Set of states. These are the states that it may be sent to.

  • step : σαSet σ
  • start : Set σ
  • accept : Set σ
Instances For
    instance NFA.instInhabited {α : Type u} {σ : Type v} :
    Inhabited (NFA α σ)
    Equations
    • NFA.instInhabited = { default := { step := fun (x : σ) (x : α) => , start := , accept := } }
    def NFA.stepSet {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (a : α) :
    Set σ

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

    Equations
    • M.stepSet S a = sS, M.step s a
    Instances For
      theorem NFA.mem_stepSet {α : Type u} {σ : Type v} (M : NFA α σ) (s : σ) (S : Set σ) (a : α) :
      s M.stepSet S a tS, s M.step t 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 though M with input x starting at an element of S.

      Equations
      Instances For
        @[simp]
        theorem NFA.evalFrom_nil {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) :
        M.evalFrom S [] = S
        @[simp]
        theorem NFA.evalFrom_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ) (a : α) :
        M.evalFrom S [a] = M.stepSet 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
        def NFA.eval {α : Type u} {σ : Type v} (M : NFA α σ) :
        List αSet σ

        M.eval x computes all possible paths though 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.start
          @[simp]
          theorem NFA.eval_singleton {α : Type u} {σ : Type v} (M : NFA α σ) (a : α) :
          M.eval [a] = M.stepSet 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
            theorem NFA.mem_accepts {α : Type u} {σ : Type v} (M : NFA α σ) {x : List α} :
            x M.accepts SM.accept, S M.evalFrom M.start x
            def NFA.toDFA {α : Type u} {σ : Type v} (M : NFA α σ) :
            DFA α (Set σ)

            M.toDFA is a DFA constructed from an NFA M using the subset construction. The states is the type of Sets of M.state and the step function is M.stepSet.

            Equations
            • M.toDFA = { step := M.stepSet, start := M.start, accept := {S : Set σ | sS, s M.accept} }
            Instances For
              @[simp]
              theorem NFA.toDFA_correct {α : Type u} {σ : Type v} (M : NFA α σ) :
              M.toDFA.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
              @[simp]
              theorem DFA.toNFA_accept {α : Type u} {σ' : Type v} (M : DFA α σ') :
              M.toNFA.accept = M.accept
              @[simp]
              theorem DFA.toNFA_step {α : Type u} {σ' : Type v} (M : DFA α σ') (s : σ') (a : α) :
              M.toNFA.step s a = {M.step s a}
              @[simp]
              theorem DFA.toNFA_start {α : Type u} {σ' : Type v} (M : DFA α σ') :
              M.toNFA.start = {M.start}
              def DFA.toNFA {α : Type u} {σ' : Type v} (M : DFA α σ') :
              NFA α σ'

              M.toNFA is an NFA constructed from a DFA M by using the same start and accept states and a transition function which sends s with input a to the singleton M.step s a.

              Equations
              • M.toNFA = { step := fun (s : σ') (a : α) => {M.step s a}, start := {M.start}, accept := M.accept }
              Instances For
                @[simp]
                theorem DFA.toNFA_evalFrom_match {α : Type u} {σ : Type v} (M : DFA α σ) (start : σ) (s : List α) :
                M.toNFA.evalFrom {start} s = {M.evalFrom start s}
                @[simp]
                theorem DFA.toNFA_correct {α : Type u} {σ : Type v} (M : DFA α σ) :
                M.toNFA.accepts = M.accepts