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

決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。
例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。
この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。しかし、リストを使うとかなり煩雑になる。

このようなものが必要な理由は、 Regular Language の Concatを考えるためである。

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

二つのオートマトンが、a0..ae b0..be につながる様子を図にしてみる。

<center><img src="fig/concat.svg"></center>

このためには後半のB automatonを、前半のA automatonが終わる可能性がある時だけ、
一文字毎に増やしてやればよい。増やしたものの一つでも成功すればよい。Bが増えるので、その増えた状態を覚えておく必要がある。

    an (Aのn番目の状態)と、b0...bn の部分集合

状態はAの状態とBの状態の部分集合の組になる。

--(a.*f)(b.*f) を考えよう

abcfbffbcdf は、この正規表現にマッチする。a.*fb.*f と書いても良い。

a.*f は以下の状態遷移で書ける。

State は a0,a1,ae,af で、ae ならば受理。

     δa a0 a = a1
     δa a1 f = ae
     δa a1 _ = a1
     δa a0 _ = af

b.*f もどうように書ける。

     δb b0 b = b1
     δb b1 f = be
     δb b1 _ = b1
     δb b0 _ = bf

これを使って、a.*fb.*f を受理してみる。

<center><img src="fig/af-concat.svg"></center>

受理パターンは二通りある。これを非決定性があるという。

この状況は、f がきた時に a.*f を終了しても良く、終了しなくてよいことから来てる。

なので、それを許すオートマトンを考える。

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

オートマトンの状態遷移は関数だった。

   δ : Q → Σ → Q 

その代わりに、複数の状態を許したい。Aの場合なら、f でaeにもa1にもいって良い。
それには、a1の状態で f がきた時に ae と a1 で true を返すようにすると良い。
行き先の状態を  Q → Bool で、部分集合として指定する。

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

これを非決定性オートマトンという。

入力にそって、可能な状態の集合を作ってやれば良い。そうすると
決定性オートマトンにできる。

<center><img src="fig/afbf.svg"></center>


--もう一つの例


この場合では 1 が来た時に q1 に行っても、q2,q3 に行っても良い。q1から始める。

    q1  0 → q1
    q1  1 → q1
    q1  1 → q2
    q1  1 → q3
    q2  0 → q3
    q3  1 → q4
    q4  0 → q4
    q4  1 → q4

最後に q4で accept。

<center><img src="fig/nfa.svg"></center>

この時に、入力に従って状態の部分集合を計算していく方法でNFAのacceptを決定できる。

このNFA(nondeterministic automaton)は .*(101|11).* に対応している。


--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を付けた。

たとえば、以下のように非決定的な状態遷移を定義する

    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


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

--NAutomatonの受理と遷移

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

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

--状態と入力の List を使って深さ優先探索する

    {-# TERMINATING #-}
    NtraceDepth : { Q : Set } { Σ : Set  } 
        → NAutomaton Q  Σ
        → (Nstart : Q → Bool) → List Q  → List  Σ → List (List ( Σ ∧ Q ))
    NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where
        ndepth : List Q → (q : Q → Bool ) → List Σ  → List ( Σ ∧ Q )  →  List (List ( Σ ∧ Q )  ) →  List (List ( Σ ∧ Q )  )
        ndepth1 : Q → Σ → List Q →  List Σ  → List ( Σ ∧ Q )  →  List ( List ( Σ ∧ Q )) →  List ( List ( Σ ∧ Q ))
        ndepth1 q i [] is t t1 = t1
        ndepth1 q i (x ∷ qns) is t t1 =  ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 )
        ndepth [] sb is t t1 =  t1
        ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
        ... | true =  ndepth qs sb [] t ( t  ∷ t1 )
        ... | false =  ndepth qs sb [] t t1
        ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q 
        ... | true  = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
        ... | false = ndepth qs sb (i ∷ is) t t1

確かに動く。しかし、複雑すぎる。

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

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

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

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

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

--finiteSet

有限な集合を表すのに、個々の data を使えばよいが、統一的に扱いたい。Agda には Data.Fin が用意されている。

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 という形に見える。

これで実際に、NFAから DFA を作成することができた。ここで、状態の有限性を使っていることを確認しよう。

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

--NFAの実行

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