-title: 非決定性オートマトンから決定性オートマトンへの変換

非決定性オートマトンは、ある状態から複数の可能な状態へ遷移する。そのうちのどれかが受理状態へ遷移すれば accept となる。

状態は有限なので、複数の可能な状態は、状態の部分集合となる。状態Qの部分集合は、

　　Q → Bool

と表すことができる。つまり、その部分集合に含まれるかどうかを表す関数が部分集合そのものになる。

これを、Bool
<sup>Q</sup> と書くことがある。Bool は二つの要素がある。状態数4からBoolへの関数は、2
<sup>4</sup>個ある。集合のべき乗をこのようにして定義することができる。

非決定性オートマトンを状態Qの部分集合を状態とする決定性オートマトンと考えることができる。
NAutomaton Q Σ は状態の集合Qと入力文字の集合Σからなる非決定性オートマトンだった。これから、

    Automaton (Q → Bool)  Σ

を作れれば、非決定性オートマトンから決定性オートマトンへの変換ができることになる。

状態Q入力文字Σの決定性オートマトンの状態遷移関数は Q → Σ → Q だったから、
この状態Qの部分集合を状態とするAutomatonの状態遷移関数は、

　(Q → Bool) → Σ → (Q → Bool)

となる。右のかっこは省略可能である。

　(Q → Bool) → Σ → Q → Bool

つまり、状態遷移関数は三つの入力を持つ。f i q としよう。決定性オートマトンの状態遷移関数は、

　  Nδ : Q → Σ → Q → Bool

だった。f : Q → Bool が入力の状態で、i : Σ が決まっている。出力状態は Q → Bool なので q を入力に持つ。

　　λ q → f q ∧ Nδ q i 


--状態の部分集合を使う

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

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

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

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

    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  } → (exists :  ( Q → Bool ) → Bool ) 
        →  ( Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
    δconv {Q} { Σ} exists nδ f i q =  exists ( λ 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  } → 
        ( ( Q → Bool ) → Bool ) →
        (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )  
    subset-construction {Q} { Σ}  exists NFA = record {
            δ = λ q x → δconv exists ( Nδ NFA ) q x
         ;  aend = λ f → exists ( λ q → f q /\ Nend NFA q )
       } 

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

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

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

これで実際に、NFAから DFA を作成することができた。
ここで、状態の exists (有限性または部分集合の決定性)を使っていることに注意しよう。

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


---問題7.1 以下の非決定性オートマトンを決定性オートマトンへ変換せよ


<a href="../exercise/003.html"> 例題  </a> <!---  Exercise 7.1 --->

--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 が存在するので、これを避けることはできない。

--NFAの実行

subset construction した automaton はすべての状態を生成する前でも実行することができる。
ただし、毎回、nest した exists を実行することになる。