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

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

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

この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。しかし、リストを使うとかなり煩雑になる。

Regular Language は Concatについて閉じている。これは オートマトン A と B があった時に、z を前半 x ++ y
にわけて x を A が受理し、y を B で受理するものを、単一ののオートマトンで実現できると言う意味である。
しかい、 これを決定性オートマトンで示すのは難しい。A ++ B の 境目がどこかを前もって予測することができないからである。

--Agda での非決定性オートマトン

ここでは、部分集合を写像を使って表す。集合 Q から Bool (true または false) への写像を使う。true になる要素が
部分集合になる。すると、遷移関数は入力Σと状態から Bool への写像となる。終了条件は変わらない。

    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>

--NAutomatonの受理と遷移

非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが
入力を読み終わった後に、終了状態になれば受理されることになる。

このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。

true になるものは複数あるので、やはり部分集合で表される。つまり、

     exists : ( P : Q → Bool ) → Q → Bool

このような関数を実現する必要がある。

もし、Q が有限集合なら、P を順々に調べていけばよい。やはり List で良いのだが、ここでは Agda の Data.Fin を使ってみよう。

--finiteSet

Data.Fin だけを使って記述することもできるが、数字だけというのも味気ない。

    record FiniteSet ( Q : Set ) { n : ℕ } : Set  where
         field
            Q←F : Fin n → Q
            F←Q : Q → Fin n
            finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
            finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f

という感じで、Data.Fin と 状態を対応させる。そうすると、

     lt0 : (n : ℕ) →  n Data.Nat.≤ n
     lt0 zero = z≤n
     lt0 (suc n) = s≤s (lt0 n)

     exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
     exists1  zero  _ _ = false
     exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p

     exists : ( Q → Bool ) → Bool
     exists p = exists1 n (lt0 n) p 

という形で、 exists を記述することができる。

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


--NAutomatonの受理と遷移

状態の受理と遷移は exists を使って以下のようになる。

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

Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、
Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば
遷移可能になる。

    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

Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。


--例題

例題1.36 を考えよう。状態遷移関数は以下のようになる。

    transition136 : StatesQ  → A2  → StatesQ → Bool
    transition136 q1 b0 q2 = true
    transition136 q1 a0 q1 = true  -- q1 → ep → q3
    transition136 q2 a0 q2 = true
    transition136 q2 a0 q3 = true
    transition136 q2 b0 q3 = true
    transition136 q3 a0 q1 = true
    transition136 _ _ _ = false

教科書にはε遷移(入力がなくても遷移できる)があるが、ここでは、ε遷移先の矢印を全部手元に持ってきてしまうという
ことしてしまう。

    end136 : StatesQ → Bool
    end136  q1 = true
    end136  _ = false

    start136 : StatesQ → Bool
    start136 q1 = true
    start136 _ = false

    nfa136 :  NAutomaton  StatesQ A2
    nfa136 =  record { Nδ = transition136; Nend = end136 }

<a href=" ../agda/nfa136.agda"> 1.36 の例題  </a>

    example136-1 = Naccept nfa136 finStateQ start136( a0  ∷ b0  ∷ a0 ∷ [] )

最初の状態 q1 から a0  ∷ b0  ∷ a0 ∷ [] の入力を受けとる場合を考える。

a0 を受けとると、q1 にしか行けない。q1 で b0 を受けとると、q2 に移動する。q2 で a0 を受けとると、q3 か、または、
q2 に行ける。どちらも終了状態ではないので、不受理となる。ここで、もう一つ a0 が来れば q3 から q1 に行ける。q2
から行けないが、どれかの経路が成功すれば良いので受理となる。

    example136-2 = Naccept nfa136 finStateQ start136( a0  ∷ b0  ∷ a0 ∷ a0 ∷ [] )


--問題

... 作成中...


--非決定性オートマトンと決定性オートマトン

    record Automaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
            δ : Q → Σ → Q
            aend : Q → Bool

の Q に Q → Bool を入れてみる。

            δ : (Q → Bool ) → Σ → Q → Bool
            aend : (Q → Bool ) → Bool

これを、

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

これの Nδ と Nend から作れれば、NFA から DFA を作れることになる。

NFAの受理を考えると、状態の集合を持ち歩いて受理を判断している。つまり、状態の集合を状態とする Automaton を考えることになる。

遷移条件は、状態の集合を受けとって、条件を満たす状態の集合を返せば良い。条件は

              Nδ : Q → Σ → Q → Bool

だった。つまり、入力の状態集合を選別する関数 f と、 Nδ との /\ を取ってやればよい。q は何かの状態、iは入力、nq は次の状態である。

    f q /\ Nδ NFA q i nq

これが true になるものを exists を使って探し出す。

    δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
    δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → f r /\ nδ r i q )

ここで、( nδ : Q → Σ → Q → Bool ) は NFAの状態遷移関数を受けとる部分である。
 
終了条件は

    f q /\ Nend NFA q )
'
で良い。 これが true になるものを exists を使って探し出す。

Q が FiniteSet Q {n} であれば

    subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  
        (NAutomaton Q  Σ ) → (astart : Q ) → (Automaton (Q → Bool)  Σ )  
    subset-construction {Q} { Σ} {n} fin NFA astart = record {
            δ = λ f i  → δconv fin ( Nδ NFA ) f i 
         ;  aend = λ f → exists fin ( λ q → f q /\ Nend NFA q )
       } 

という形で書くことができる。状態の部分集合を作っていくので、subset construction と呼ばれる。

            λ f i  → δconv fin ( Nδ NFA ) f i 
は
            λ f i q → δconv fin ( Nδ NFA ) f i q

であることに注意しよう。これは、Curry 化の省略になっている。省略があるので、δ : (Q → Bool ) → Σ → Q → Bool という形に見える。

<a href=" ../agda/sbconst2.agda"> subset construction  </a>

--subset constructionの状態数

実際にこれを計算すると、状態数 n のNFAから、最大、2^n の状態を持つDFAが生成される。しかし、この論理式からそれを
自明に理解することは難しい。しかし、f は Q → Bool なので、例えば、3状態でも、

      q1    q2    q3
      false false false
      false false true
      false true  false
      false true  true
      true  false false
      true  false true
      true  true  false
      true  true  true

という8個の状態を持つ。exists は、このすべての場合を尽くすように働いている。

アルゴリズムとしてこのまま実装すると、 exists が必要な分だけ計算するようになっている。これは結構遅い。
前もって、可能な状態を Automaton として探し出そうとすると、 指数関数的な爆発になってしまう。

実際に、指数関数的な状態を作る NFA が存在するので、これを避けることはできない。