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