Mercurial > hg > Members > kono > Proof > automaton

comparison a04/lecture.ind @ 410:db02b6938e04

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
StarProp and Ntrace
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 22 Nov 2023 17:07:01 +0900
parents 3d0aa205edf9
children
comparison
equal deleted inserted replaced
409:4e4acdc43dee 410:db02b6938e04
138 --NAutomatonの受理と遷移 138 --NAutomatonの受理と遷移
139 139
140 非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが 140 非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが
141 入力を読み終わった後に、終了状態になれば受理されることになる。 141 入力を読み終わった後に、終了状態になれば受理されることになる。
142 142
143 このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。 143 このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。これを
144 144
145 --状態と入力の List を使って深さ優先探索する 145 exists : ( P : Q → Bool ) → Bool
146 146
147 {-# TERMINATING #-} 147 として定義する。この気持ちは P 満たす状態Qが一つはあるということ。それは自分で保証するようにかく。
148 NtraceDepth : { Q : Set } { Σ : Set } 148
149 → NAutomaton Q Σ 149 状態が有限なら、FiniteSet の exists を使える。
150 → (Nstart : Q → Bool) → List Q → List Σ → List (List ( Σ ∧ Q ))
151 NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where
152 ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (List ( Σ ∧ Q ) ) → List (List ( Σ ∧ Q ) )
153 ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( List ( Σ ∧ Q )) → List ( List ( Σ ∧ Q ))
154 ndepth1 q i [] is t t1 = t1
155 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 )
156 ndepth [] sb is t t1 = t1
157 ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q
158 ... | true = ndepth qs sb [] t ( t ∷ t1 )
159 ... | false = ndepth qs sb [] t t1
160 ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q
161 ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 )
162 ... | false = ndepth qs sb (i ∷ is) t t1
163
164 確かに動く。しかし、複雑すぎる。
165
166 --状態の部分集合を使う
167
168 true になるものは複数あるので、やはり部分集合で表される。つまり、
169
170 exists : ( P : Q → Bool ) → Q → Bool
171
172 このような関数を実現する必要がある。
173
174 もし、Q が有限集合なら、P を順々に調べていけばよい。やはり List で良いのだが、ここでは Agda の Data.Fin を使ってみよう。
175
176
177 --NAutomatonの受理と遷移
178 150
179 状態の受理と遷移は exists を使って以下のようになる。 151 状態の受理と遷移は exists を使って以下のようになる。
180
181 Nmoves : { Q : Set } { Σ : Set }
182 → NAutomaton Q Σ
183 → (exists : ( Q → Bool ) → Bool)
184 → ( Qs : Q → Bool ) → (s : Σ ) → ( Q → Bool )
185 Nmoves {Q} { Σ} M exists Qs s = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q ) ))
186 152
187 Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、 153 Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、
188 Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば 154 Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば
189 遷移可能になる。(だいぶ簡単になった) 155 遷移可能になる。(だいぶ簡単になった)
190 156
195 → (Nstart : Q → Bool) → List Σ → Bool 161 → (Nstart : Q → Bool) → List Σ → Bool
196 Naccept M exists sb [] = exists ( λ q → sb q /\ Nend M q ) 162 Naccept M exists sb [] = exists ( λ q → sb q /\ Nend M q )
197 Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t 163 Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t
198 164
199 Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。 165 Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。
166
167 --Ntrace
168
169 Qをすべて含む List Qを用意すれば、状態と入力の List から、状態の集合のListを作ることができる。
170
171 Ntrace : { Q : Set } { Σ : Set }
172 → NAutomaton Q Σ
173 → (all-states : List Q )
174 → (exists : ( Q → Bool ) → Bool)
175 → (Nstart : Q → Bool) → List Σ → List (List Q)
176 Ntrace M all-states exists sb [] = to-list all-states ( λ q → sb q /\ Nend M q ) ∷ []
177 Ntrace M all-states exists sb (i ∷ t ) =
178 to-list all-states (λ q → sb q ) ∷
179 Ntrace M all-states exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t
180
181 たとえば、
182
183 Ntrace am2 LStates1 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] )
184
185 のように呼び出す。
200 186
201 --例題 187 --例題
202 188
203 例題1.36 を考えよう。状態遷移関数は以下のようになる。 189 例題1.36 を考えよう。状態遷移関数は以下のようになる。
204 190
235 q2 に行ける。どちらも終了状態ではないので、不受理となる。ここで、もう一つ a0 が来れば q3 から q1 に行ける。q2 221 q2 に行ける。どちらも終了状態ではないので、不受理となる。ここで、もう一つ a0 が来れば q3 から q1 に行ける。q2
236 から行けないが、どれかの経路が成功すれば良いので受理となる。 222 から行けないが、どれかの経路が成功すれば良いので受理となる。
237 223
238 example136-2 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] ) 224 example136-2 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] )
239 225
240 226 ---問題4.1 NFAのtrace
241 227
242 228
243 229 <a href="../exercise/007.html"> NFAのtrace </a> <!--- Exercise 4.1 --->
244 230
245 231 Ntrace を修正すればよい。
246 232
247 233
248 234
249 235
250 236
251 237
238
239
240
241
242