-title: 非決定性オートマトン 決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。 例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。 この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。しかし、リストを使うとかなり煩雑になる。 このようなものが必要な理由は、 Regular Language の Concatを考えるためである。 Regular Language は Concatについて閉じている。これは オートマトン A と B があった時に、z を前半 x ++ y にわけて x を A が受理し、y を B で受理するものを、単一ののオートマトンで実現できると言う意味である。 しかい、 これを決定性オートマトンで示すのは難しい。A ++ B の 境目がどこかを前もって予測することができないからである。 二つのオートマトンが、a0..ae b0..be につながる様子を図にしてみる。
このためには後半のB automatonを、前半のA automatonが終わる可能性がある時だけ、 一文字毎に増やしてやればよい。増やしたものの一つでも成功すればよい。Bが増えるので、その増えた状態を覚えておく必要がある。 an (Aのn番目の状態)と、b0...bn の部分集合 状態はAの状態とBの状態の部分集合の組になる。 --(a.*f)(b.*f) を考えよう abcfbffbcdf は、この正規表現にマッチする。a.*fb.*f と書いても良い。 Perl で書けば perl -de 0 DB<14> if ($x =~ /^(a.*f)(b.*f)$/) { print "$1 $2\n"; } perl -e 'if ($x =~ /^(a.*f)(b.*f)$/) { print "$1 $2\n"; }' 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 を受理してみる。 nfa136.agda
受理パターンは二通りある。これを非決定性があるという。 この状況は、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 これを非決定性オートマトンという。 入力にそって、可能な状態の集合を作ってやれば良い。そうすると 決定性オートマトンにできる。
--もう一つの例 この場合では 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。
この時に、入力に従って状態の部分集合を計算していく方法で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 nfa.agda --NAutomatonの受理と遷移 非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが 入力を読み終わった後に、終了状態になれば受理されることになる。 このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。これを exists : ( P : Q → Bool ) → Bool として定義する。この気持ちは P 満たす状態Qが一つはあるということ。それは自分で保証するようにかく。 状態が有限なら、FiniteSet の exists を使える。 状態の受理と遷移は exists を使って以下のようになる。 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 Σ → (exists : ( Q → Bool ) → Bool) → (Nstart : Q → Bool) → List Σ → Bool Naccept M exists sb [] = exists ( λ q → sb q /\ Nend M q ) Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。 --Ntrace Qをすべて含む List Qを用意すれば、状態と入力の List から、状態の集合のListを作ることができる。 Ntrace : { Q : Set } { Σ : Set } → NAutomaton Q Σ → (all-states : List Q ) → (exists : ( Q → Bool ) → Bool) → (Nstart : Q → Bool) → List Σ → List (List Q) Ntrace M all-states exists sb [] = to-list all-states ( λ q → sb q /\ Nend M q ) ∷ [] Ntrace M all-states exists sb (i ∷ t ) = to-list all-states (λ q → sb q ) ∷ Ntrace M all-states exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t たとえば、 Ntrace am2 LStates1 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) のように呼び出す。 --例題 例題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 } 1.36 の例題 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 ∷ [] ) ---問題4.1 NFAのtrace NFAのtrace Ntrace を修正すればよい。