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

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

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

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

    record NAutomaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
              nδ : Q → Σ → List Q
              sid : Q  →  ℕ
              nstart : Q
              nend  : Q → Bool

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

次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。

少し複雑がだが、insert と merge を定義して、

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

    insert : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) →  List Q  → Q  → List Q
    insert  M  [] q =  q ∷ []
    insert  M  ( q  ∷ T ) q' with  (sid M q ) ≟ (sid M q')
    ... | yes _ = insert  M  T q'
    ... | no _ = q  ∷ (insert  M  T q' )

    merge : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) → List Q  → List Q  → List Q
    merge  M L1 [] = L1
    merge  M L1 ( H  ∷ L  ) =  insert M (merge M L1 L ) H

    Nmoves : { Q : Set } { Σ : Set  }
        → NAutomaton Q  Σ
        → List Q → List  Σ → List Q
    Nmoves {Q} { Σ} M q L = Nmoves1 q L []
       where
          Nmoves1 : (q : List Q ) ( L : List  Σ ) → List Q → List Q
          Nmoves1 q  [] _ = q
          Nmoves1 []  (_  ∷ L) LQ = Nmoves1 LQ L []
          Nmoves1 (q  ∷ T ) (H  ∷ L) LQ = Nmoves1 T  (H  ∷ L) ( merge M  ( nδ M q H ) LQ )

    Naccept : { Q : Set } { Σ : Set  }
        → NAutomaton Q  Σ
        →  List  Σ → Bool
    Naccept {Q} { Σ} M L =
           checkAccept ( Nmoves M ((nstart M)  ∷ [] )  L )
       where
          checkAccept : (q : List Q ) → Bool
          checkAccept [] = false
          checkAccept ( H ∷ L ) with (nend M) H
          ... | true = true
          ... | false = checkAccept L

とする。 

--部分集合を使うと簡単になる

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


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


    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}
        → List  Σ  → Bool
    Naccept {Q} {Σ} M fin input = Naccept1 M ( Nstart M ) input
       where
          Naccept1 : NAutomaton Q  Σ → ( Q → Bool ) →  List  Σ  →  Bool
          Naccept1 M sb []  = exists fin ( λ q → sb q ∧ Nend M q )
          Naccept1 M sb (i ∷ t ) = Naccept1 M ( Nmoves M  fin sb i ) t

--例題

    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 ; Nstart = start1 ; Nend = fin1}

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