-title: 非決定性オートマトン

決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。

例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。

この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。部分集合を使っても良いが、ここではリストを使おう。

    record NAutomaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
              Nδ : Q → Σ → Q → Bool
              Nend  :  Q → Bool

これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、nを付けた。

<a href="../agda/nfa.agda"> nfa.agda </a>

状態の受理と遷移は以下のようになる。

    Nmoves : { Q : Set } { Σ : Set  }
        → NAutomaton Q  Σ
        → {n : ℕ } → FiniteSet Q  {n}
        →  ( Q → Bool )  → Σ → Q → Bool
    Nmoves {Q} { Σ} M fin  Qs  s q  =
          exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q )  ))

    Naccept : { Q : Set } { Σ : Set  }
        → NAutomaton Q  Σ
        → {n : ℕ } → FiniteSet Q {n}
        → (Nstart : Q → Bool) → List  Σ → Bool
    Naccept M fin sb []  = exists fin ( λ q → sb q ∧ Nend M q )
    Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M  fin sb i ) t

次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。
しかし、List で定義すると少し複雑になる。

部分集合を使うと簡単になる。Q の部分集合は Q → Bool で true になるものであるとする。


--例題

    transition3 : States1  → In2  → States1 → Bool
    transition3 sr i0 sr = true
    transition3 sr i1 ss = true
    transition3 sr i1 sr = true
    transition3 ss i0 sr = true
    transition3 ss i1 st = true
    transition3 st i0 sr = true
    transition3 st i1 st = true
    transition3 _ _ _ = false

    fin1 :  States1  → Bool
    fin1 st = true
    fin1 ss = false
    fin1 sr = false

    start1 : States1 → Bool
    start1 sr = true
    start1 _ = false

    am2  :  NAutomaton  States1 In2
    am2  =  record { Nδ = transition3 ; Nend = fin1}

    example2-1 = Naccept am2 finState1 start1 ( i0  ∷ i1  ∷ i0  ∷ [] )
    example2-2 = Naccept am2 finState1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] )

    fin0 :  States1  → Bool
    fin0 st = false
    fin0 ss = false
    fin0 sr = false

    test0 : Bool
    test0 = exists finState1 fin0

    test1 : Bool
    test1 = exists finState1 fin1

    test2 = Nmoves am2 finState1 start1