comparison agda/flcagl.agda @ 52:8438c989d5a7

fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 02 Oct 2019 13:19:44 +0900
parents bc0400528027
children eddc4ad8e99a
comparison
equal deleted inserted replaced
51:bc0400528027 52:8438c989d5a7
69 _∪_ : ∀{i} (k l : Lang i) → Lang i 69 _∪_ : ∀{i} (k l : Lang i) → Lang i
70 ν (k ∪ l) = ν k ∨ ν l 70 ν (k ∪ l) = ν k ∨ ν l
71 δ (k ∪ l) x = δ k x ∪ δ l x 71 δ (k ∪ l) x = δ k x ∪ δ l x
72 72
73 73
74 _·'_ : ∀{i} (k l : Lang i) → Lang i 74 _·_ : ∀{i} (k l : Lang i) → Lang i
75 ν (k ·' l) = ν k ∧ ν l
76 δ (k ·' l) x = let k′l = δ k x ·' l in if ν k then k′l ∪ δ l x else k′l
77
78 _·_ : ∀{i} (k l : Lang i ) → Lang i
79 ν (k · l) = ν k ∧ ν l 75 ν (k · l) = ν k ∧ ν l
80 δ (_·_ {i} k l) {j} x = 76 δ (k · l) x = let k′l = δ k x · l in if ν k then k′l ∪ δ l x else k′l
77
78 _*_ : ∀{i} (k l : Lang i ) → Lang i
79 ν (k * l) = ν k ∧ ν l
80 δ (_*_ {i} k l) {j} x =
81 let 81 let
82 k′l : Lang j 82 k′l : Lang j
83 k′l = _·_ {j} (δ k {j} x) l 83 k′l = _*_ {j} (δ k {j} x) l
84 in if ν k then _∪_ {j} k′l (δ l {j} x) else k′l 84 in if ν k then _∪_ {j} k′l (δ l {j} x) else k′l
85 85
86 _* : ∀{i} (l : Lang i) → Lang i 86 _* : ∀{i} (l : Lang i) → Lang i
87 ν (l *) = true 87 ν (l *) = true
88 δ (l *) x = δ l x · (l *) 88 δ (l *) x = δ l x · (l *)
216 ≈⟨ ≅refl ⟩ 216 ≈⟨ ≅refl ⟩
217 (if false then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m) 217 (if false then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m)
218 218
219 where open EqR (Bis _) 219 where open EqR (Bis _)
220 ≅δ (concat-union-distribl k {l} {m}) a | true | false = begin 220 ≅δ (concat-union-distribl k {l} {m}) a | true | false = begin
221 (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) 221 (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩
222 ≈⟨ ≅refl ⟩ 222 ((δ k a ∪ δ l a) · m ) ∪ δ m a ≈⟨ union-congl (concat-union-distribl _) ⟩
223 ((δ k a ∪ δ l a) · m ) ∪ δ m a 223 (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨ union-assoc _ ⟩
224 ≈⟨ union-congl (concat-union-distribl _) ⟩ 224 δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨ union-congr ( union-comm _ _) ⟩
225 (δ k a · m ∪ δ l a · m) ∪ δ m a 225 δ k a · m ∪ δ m a ∪ δ l a · m ≈⟨ ≅sym ( union-assoc _ ) ⟩
226 ≈⟨ union-assoc _ ⟩ 226 (δ k a · m ∪ δ m a) ∪ δ l a · m ≈⟨ ≅refl ⟩
227 δ k a · m ∪ ( δ l a · m ∪ δ m a )
228 ≈⟨ union-congr ( union-comm _ _) ⟩
229 δ k a · m ∪ δ m a ∪ δ l a · m
230 ≈⟨ ≅sym ( union-assoc _ ) ⟩
231 (δ k a · m ∪ δ m a) ∪ δ l a · m
232 ≈⟨ ≅refl ⟩
233 ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if false then δ l a · m ∪ δ m a else δ l a · m)) 227 ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if false then δ l a · m ∪ δ m a else δ l a · m))
234 228
235 where open EqR (Bis _) 229 where open EqR (Bis _)
236 ≅δ (concat-union-distribl k {l} {m}) a | true | true = begin 230 ≅δ (concat-union-distribl k {l} {m}) a | true | true = begin
237 (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) 231 (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩
238 ≈⟨ ≅refl ⟩ 232 (δ k a ∪ δ l a) · m ∪ δ m a ≈⟨ union-congl ( concat-union-distribl _ ) ⟩
239 (δ k a ∪ δ l a) · m ∪ δ m a 233 (δ k a · m ∪ δ l a · m) ∪ δ m a ≈⟨ union-assoc _ ⟩
240 ≈⟨ union-congl ( concat-union-distribl _ ) ⟩ 234 δ k a · m ∪ ( δ l a · m ∪ δ m a ) ≈⟨ ≅sym ( union-congr ( union-congr ( union-idem _ ) ) ) ⟩
241 (δ k a · m ∪ δ l a · m) ∪ δ m a 235 δ k a · m ∪ ( δ l a · m ∪ (δ m a ∪ δ m a) ) ≈⟨ ≅sym ( union-congr ( union-assoc _ )) ⟩
242 ≈⟨ union-assoc _ ⟩ 236 δ k a · m ∪ ( (δ l a · m ∪ δ m a ) ∪ δ m a ) ≈⟨ union-congr ( union-congl ( union-comm _ _) ) ⟩
243 δ k a · m ∪ ( δ l a · m ∪ δ m a ) 237 δ k a · m ∪ ( (δ m a ∪ δ l a · m ) ∪ δ m a ) ≈⟨ ≅sym ( union-assoc _ ) ⟩
244 ≈⟨ ≅sym ( union-congr ( union-congr ( union-idem _ ) ) ) ⟩ 238 ( δ k a · m ∪ (δ m a ∪ δ l a · m )) ∪ δ m a ≈⟨ ≅sym ( union-congl ( union-assoc _ ) ) ⟩
245 δ k a · m ∪ ( δ l a · m ∪ (δ m a ∪ δ m a) ) 239 ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a ≈⟨ union-assoc _ ⟩
246 ≈⟨ ≅sym ( union-congr ( union-assoc _ )) ⟩ 240 (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a ≈⟨ ≅refl ⟩
247 δ k a · m ∪ ( (δ l a · m ∪ δ m a ) ∪ δ m a ) 241 ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m))
248 ≈⟨ union-congr ( union-congl ( union-comm _ _) ) ⟩
249 δ k a · m ∪ ( (δ m a ∪ δ l a · m ) ∪ δ m a )
250 ≈⟨ ≅sym ( union-assoc _ ) ⟩
251 ( δ k a · m ∪ (δ m a ∪ δ l a · m )) ∪ δ m a
252 ≈⟨ ≅sym ( union-congl ( union-assoc _ ) ) ⟩
253 ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a
254 ≈⟨ union-assoc _ ⟩
255 (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a
256 ≈⟨ ≅refl ⟩
257 ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m))
258 242
259 where open EqR (Bis _) 243 where open EqR (Bis _)
260 244
261 postulate 245 postulate
262 concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅ 246 concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅
308 ∎ where open EqR (Bis _) 292 ∎ where open EqR (Bis _)
309 293
310 star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l * 294 star-concat-idem : ∀{i} (l : Lang ∞) → l * · l * ≅⟨ i ⟩≅ l *
311 ≅ν (star-concat-idem l) = refl 295 ≅ν (star-concat-idem l) = refl
312 ≅δ (star-concat-idem l) a = begin 296 ≅δ (star-concat-idem l) a = begin
313 δ ((l *) · (l *)) a 297 δ ((l *) · (l *)) a ≈⟨ union-congl (concat-assoc _) ⟩
314 ≈⟨ union-congl (concat-assoc _) ⟩ 298 δ l a · (l * · l *) ∪ δ l a · l * ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩
315 δ l a · (l * · l *) ∪ δ l a · l * 299 δ l a · l * ∪ δ l a · l * ≈⟨ union-idem _ ⟩
316 ≈⟨ union-congl (concat-congr (star-concat-idem _)) ⟩ 300 δ (l *) a ∎ where open EqR (Bis _)
317 δ l a · l * ∪ δ l a · l *
318 ≈⟨ union-idem _ ⟩
319 δ (l *) a
320 ∎ where open EqR (Bis _)
321 301
322 star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l * 302 star-idem : ∀{i} (l : Lang ∞) → (l *) * ≅⟨ i ⟩≅ l *
323 ≅ν (star-idem l) = refl 303 ≅ν (star-idem l) = refl
324 ≅δ (star-idem l) a = begin 304 ≅δ (star-idem l) a = begin
325 δ ((l *) *) a ≈⟨ concat-assoc (δ l a) ⟩ 305 δ ((l *) *) a ≈⟨ concat-assoc (δ l a) ⟩
475 lang (starA s0 da) ss ≅⟨ i ⟩≅ 455 lang (starA s0 da) ss ≅⟨ i ⟩≅
476 lang (powA (acceptingInitial s0 da)) ss · (lang da s0) * 456 lang (powA (acceptingInitial s0 da)) ss · (lang da s0) *
477 starA-correct : ∀{i S} (da : DA S) (s0 : S) → 457 starA-correct : ∀{i S} (da : DA S) (s0 : S) →
478 lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) * 458 lang (starA s0 da) (nothing ∷ []) ≅⟨ i ⟩≅ (lang da s0) *
479 459
460 record NAutomaton ( Q : Set ) ( Σ : Set )
461 : Set where
462 field
463 Nδ : Q → Σ → Q → Bool
464 Nstart : Q → Bool
465 Nend : Q → Bool
466
467 postulate
468 exists : { S : Set} → ( S → Bool ) → Bool
469
470 nlang : ∀{i} {S} (nfa : NAutomaton S A ) (s : S → Bool ) → Lang i
471 Lang.ν (nlang nfa s) = exists ( λ x → (s x ∧ NAutomaton.Nend nfa x ))
472 Lang.δ (nlang nfa s) a = nlang nfa (λ x → s x ∧ (NAutomaton.Nδ nfa x a) x)
473
474 -- nlang' : ∀{i} {S} (nfa : DA (S → Bool) ) (s : S → Bool ) → Lang i
475 -- Lang.ν (nlang' nfa s) = DA.ν nfa s
476 -- Lang.δ (nlang' nfa s) a = nlang' nfa (DA.δ nfa s a)
477