Mercurial > hg > Members > kono > Proof > automaton

comparison a04/lecture.ind @ 104:fba1cd54581d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use exists in cond, nfa example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 14 Nov 2019 05:13:49 +0900
parents f124fceba460
children b3f05cd08d24
comparison
equal deleted inserted replaced
103:a46e0a2a3543 104:fba1cd54581d
2 2
3 決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。 3 決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。
4 4
5 例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。 5 例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。
6 6
7 この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。部分集合を使っても良いが、ここではリストを使おう。 7 この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。しかし、リストを使うとかなり煩雑になる。
8
9 Regular Language は Concatについて閉じている。これは オートマトン A と B があった時に、z を前半 x ++ y
10 にわけて x を A が受理し、y を B で受理するものを、単一ののオートマトンで実現できると言う意味である。
11 しかい、 これを決定性オートマトンで示すのは難しい。A ++ B の 境目がどこかを前もって予測することができないからである。
12
13 --Agda での非決定性オートマトン
14
15 ここでは、部分集合を写像を使って表す。集合 Q から Bool (true または false) への写像を使う。true になる要素が
16 部分集合になる。すると、遷移関数は入力Σと状態から Bool への写像となる。終了条件は変わらない。
8 17
9 record NAutomaton ( Q : Set ) ( Σ : Set ) 18 record NAutomaton ( Q : Set ) ( Σ : Set )
10 : Set where 19 : Set where
11 field 20 field
12 Nδ : Q → Σ → Q → Bool 21 Nδ : Q → Σ → Q → Bool
13 Nend : Q → Bool 22 Nend : Q → Bool
14 23
15 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、nを付けた。 24 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、Nを付けた。
16 25
17 <a href="../agda/nfa.agda"> nfa.agda </a> 26 <a href="../agda/nfa.agda"> nfa.agda </a>
18 27
19 状態の受理と遷移は以下のようになる。 28 --NAutomatonの受理と遷移
29
30 非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが
31 入力を読み終わった後に、終了状態になれば受理されることになる。
32
33 このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。
34
35 true になるものは複数あるので、やはり部分集合で表される。つまり、
36
37 exists : ( P : Q → Bool ) → Q → Bool
38
39 このような関数を実現する必要がある。
40
41 もし、Q が有限集合なら、P を順々に調べていけばよい。やはり List で良いのだが、ここでは Agda の Data.Fin を使ってみよう。
42
43 --finiteSet
44
45 Data.Fin だけを使って記述することもできるが、数字だけというのも味気ない。
46
47 record FiniteSet ( Q : Set ) { n : ℕ } : Set where
48 field
49 Q←F : Fin n → Q
50 F←Q : Q → Fin n
51 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
52 finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
53
54 という感じで、Data.Fin と 状態を対応させる。そうすると、
55
56 lt0 : (n : ℕ) → n Data.Nat.≤ n
57 lt0 zero = z≤n
58 lt0 (suc n) = s≤s (lt0 n)
59
60 exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
61 exists1 zero _ _ = false
62 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
63
64 exists : ( Q → Bool ) → Bool
65 exists p = exists1 n (lt0 n) p
66
67 という形で、 exists を記述することができる。
68
69 <a href="../agda/finiteSet.agda"> finiteSet.agda </a>
70
71
72 --NAutomatonの受理と遷移
73
74 状態の受理と遷移は exists を使って以下のようになる。
20 75
21 Nmoves : { Q : Set } { Σ : Set } 76 Nmoves : { Q : Set } { Σ : Set }
22 → NAutomaton Q Σ 77 → NAutomaton Q Σ
23 → {n : ℕ } → FiniteSet Q {n} 78 → {n : ℕ } → FiniteSet Q {n}
24 → ( Q → Bool ) → Σ → Q → Bool 79 → ( Qs : Q → Bool ) → (s : Σ ) → Q → Bool
25 Nmoves {Q} { Σ} M fin Qs s q = 80 Nmoves {Q} { Σ} M fin Qs s q =
26 exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q ) )) 81 exists fin ( λ qn → (Qs qn /\ ( Nδ M qn s q ) ))
27 82
28 Naccept : { Q : Set } { Σ : Set } 83 Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、
84 Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば
85 遷移可能になる。
86
87 Naccept : { Q : Set } { Σ : Set }
29 → NAutomaton Q Σ 88 → NAutomaton Q Σ
30 → {n : ℕ } → FiniteSet Q {n} 89 → {n : ℕ } → FiniteSet Q {n}
31 → (Nstart : Q → Bool) → List Σ → Bool 90 → (Nstart : Q → Bool) → List Σ → Bool
32 Naccept M fin sb [] = exists fin ( λ q → sb q ∧ Nend M q ) 91 Naccept M fin sb [] = exists fin ( λ q → sb q /\ Nend M q )
33 Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M fin sb i ) t 92 Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M fin sb i ) t
34 93
35 次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。 94 Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。
36 しかし、List で定義すると少し複雑になる。
37
38 部分集合を使うと簡単になる。Q の部分集合は Q → Bool で true になるものであるとする。
39 95
40 96
41 --例題 97 --例題
42 98
43 transition3 : States1 → In2 → States1 → Bool 99 例題1.36 を考えよう。状態遷移関数は以下のようになる。
44 transition3 sr i0 sr = true 100
45 transition3 sr i1 ss = true 101 transition136 : StatesQ → A2 → StatesQ → Bool
46 transition3 sr i1 sr = true 102 transition136 q1 b0 q2 = true
47 transition3 ss i0 sr = true 103 transition136 q1 a0 q1 = true -- q1 → ep → q3
48 transition3 ss i1 st = true 104 transition136 q2 a0 q2 = true
49 transition3 st i0 sr = true 105 transition136 q2 a0 q3 = true
50 transition3 st i1 st = true 106 transition136 q2 b0 q3 = true
51 transition3 _ _ _ = false 107 transition136 q3 a0 q1 = true
52 108 transition136 _ _ _ = false
53 fin1 : States1 → Bool 109
54 fin1 st = true 110 教科書にはε遷移(入力がなくても遷移できる)があるが、ここでは、ε遷移先の矢印を全部手元に持ってきてしまうという
55 fin1 ss = false 111 ことしてしまう。
56 fin1 sr = false 112
57 113 end136 : StatesQ → Bool
58 start1 : States1 → Bool 114 end136 q1 = true
59 start1 sr = true 115 end136 _ = false
60 start1 _ = false 116
61 117 start136 : StatesQ → Bool
62 am2 : NAutomaton States1 In2 118 start136 q1 = true
63 am2 = record { Nδ = transition3 ; Nend = fin1} 119 start136 _ = false
64 120
65 example2-1 = Naccept am2 finState1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) 121 nfa136 : NAutomaton StatesQ A2
66 example2-2 = Naccept am2 finState1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) 122 nfa136 = record { Nδ = transition136; Nend = end136 }
67 123
68 fin0 : States1 → Bool 124 <a href=" ../agda/nfa136.agda"> 1.36 の例題 </a>
69 fin0 st = false 125
70 fin0 ss = false 126 example136-1 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ [] )
71 fin0 sr = false 127
72 128 最初の状態 q1 から a0 ∷ b0 ∷ a0 ∷ [] の入力を受けとる場合を考える。
73 test0 : Bool 129
74 test0 = exists finState1 fin0 130 a0 を受けとると、q1 にしか行けない。q1 で b0 を受けとると、q2 に移動する。q2 で a0 を受けとると、q3 か、または、
75 131 q2 に行ける。どちらも終了状態ではないので、不受理となる。ここで、もう一つ a0 が来れば q3 から q1 に行ける。q2
76 test1 : Bool 132 から行けないが、どれかの経路が成功すれば良いので受理となる。
77 test1 = exists finState1 fin1 133
78 134 example136-2 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] )
79 test2 = Nmoves am2 finState1 start1 135
80 136
137 --問題
138
139 ... 作成中...
140
141
142 --非決定性オートマトンと決定性オートマトン
143
144 record Automaton ( Q : Set ) ( Σ : Set )
145 : Set where
146 field
147 δ : Q → Σ → Q
148 aend : Q → Bool
149
150 の Q に Q → Bool を入れてみる。
151
152 δ : (Q → Bool ) → Σ → Q → Bool
153 aend : (Q → Bool ) → Bool
154
155 これを、
156
157 record NAutomaton ( Q : Set ) ( Σ : Set )
158 : Set where
159 field
160 Nδ : Q → Σ → Q → Bool
161 Nend : Q → Bool
162
163 これの Nδ と Nend から作れれば、NFA から DFA を作れることになる。
164
165 NFAの受理を考えると、状態の集合を持ち歩いて受理を判断している。つまり、状態の集合を状態とする Automaton を考えることになる。
166
167 遷移条件は、状態の集合を受けとって、条件を満たす状態の集合を返せば良い。条件は
168
169 Nδ : Q → Σ → Q → Bool
170
171 だった。つまり、入力の状態集合を選別する関数 f と、 Nδ との /\ を取ってやればよい。q は何かの状態、iは入力、nq は次の状態である。
172
173 f q /\ Nδ NFA q i nq
174
175 これが true になるものを exists を使って探し出す。
176
177 δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
178 δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → f r /\ nδ r i q )
179
180 ここで、( nδ : Q → Σ → Q → Bool ) は NFAの状態遷移関数を受けとる部分である。
181
182 終了条件は
183
184 f q /\ Nend NFA q )
185 '
186 で良い。 これが true になるものを exists を使って探し出す。
187
188 Q が FiniteSet Q {n} であれば
189
190 subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} →
191 (NAutomaton Q Σ ) → (astart : Q ) → (Automaton (Q → Bool) Σ )
192 subset-construction {Q} { Σ} {n} fin NFA astart = record {
193 δ = λ f i → δconv fin ( Nδ NFA ) f i
194 ; aend = λ f → exists fin ( λ q → f q /\ Nend NFA q )
195 }
196
197 という形で書くことができる。状態の部分集合を作っていくので、subset construction と呼ばれる。
198
199 λ f i → δconv fin ( Nδ NFA ) f i
200 は
201 λ f i q → δconv fin ( Nδ NFA ) f i q
202
203 であることに注意しよう。これは、Curry 化の省略になっている。省略があるので、δ : (Q → Bool ) → Σ → Q → Bool という形に見える。
204
205 <a href=" ../agda/sbconst2.agda"> subset construction </a>
206
207 --subset constructionの状態数
208
209 実際にこれを計算すると、状態数 n のNFAから、最大、2^n の状態を持つDFAが生成される。しかし、この論理式からそれを
210 自明に理解することは難しい。しかし、f は Q → Bool なので、例えば、3状態でも、
211
212 q1 q2 q3
213 false false false
214 false false true
215 false true false
216 false true true
217 true false false
218 true false true
219 true true false
220 true true true
221
222 という8個の状態を持つ。exists は、このすべての場合を尽くすように働いている。
223
224 アルゴリズムとしてこのまま実装すると、 exists が必要な分だけ計算するようになっている。これは結構遅い。
225 前もって、可能な状態を Automaton として探し出そうとすると、 指数関数的な爆発になってしまう。
226
227 実際に、指数関数的な状態を作る NFA が存在するので、これを避けることはできない。
228