Mercurial > hg > Members > kono > Proof > automaton1
annotate nfa.agda @ 10:ef43350ea0e2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 15 Nov 2020 14:36:25 +0900 |
| parents | 8a6660c5b1da |
| children | 554fa6e5a09d |
| rev | line source |
|---|---|
|
8
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
1 {-# OPTIONS --allow-unsolved-metas #-} |
| 0 | 2 module nfa where |
| 3 open import Level renaming ( suc to Suc ; zero to Zero ) | |
| 4 | |
| 5 open import Relation.Binary.PropositionalEquality | |
| 6 open import Data.List | |
| 1 | 7 open import Relation.Nullary |
| 0 | 8 open import automaton |
| 9 open import logic | |
| 10 | |
| 11 record NAutomaton {n : Level} ( Q : Set n ) ( Σ : Set ) | |
| 12 : Set (Suc n) where | |
| 13 field | |
| 14 Nδ : Q → Σ → Q → Set | |
| 1 | 15 NF : Q → Set |
| 0 | 16 |
| 17 open NAutomaton | |
| 18 | |
| 2 | 19 naccept : {n : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set) → Set) → NAutomaton Q Σ → (Q → Set) → List Σ → Set |
| 9 | 20 naccept {n} {Q} {Σ} Nexists nfa qs [] = Nexists (λ p → qs p ∧ NF nfa p ) |
| 2 | 21 naccept {n} {Q} {Σ} Nexists nfa qs (x ∷ input) = |
| 9 | 22 naccept Nexists nfa (λ p' → Nexists (λ p → qs p ∧ Nδ nfa p x p' )) input |
| 1 | 23 |
| 2 | 24 qlist : {n : Level} {Q : Set n} → (P : Q → Set ) → ((q : Q) → Dec ( P q)) → List Q → List Q |
| 25 qlist P dec [] = [] | |
| 26 qlist P dec (q ∷ qs) with dec q | |
| 27 ... | yes _ = q ∷ qlist P dec qs | |
| 28 ... | no _ = qlist P dec qs | |
| 0 | 29 |
| 2 | 30 ntrace : {n : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set) → Set) → (nfa : NAutomaton Q Σ) → (qs : Q → Set ) → (input : List Σ ) |
| 31 → naccept Nexists nfa qs input | |
| 6 | 32 → ((q : Q) → Dec (qs q)) |
| 33 → (next-dec : (qs : Q → Set) → ((q : Q) → Dec (qs q)) → (x : Σ) → (q : Q ) → Dec (Nexists (λ nq → qs nq ∧ Nδ nfa nq x q))) | |
| 2 | 34 → List Q |
| 35 → List (List Q) | |
| 6 | 36 ntrace {n} {Q} {Σ} Nexists nfa qs [] a dec next-dec L = qlist qs dec L ∷ [] |
| 37 ntrace {n} {Q} {Σ} Nexists nfa qs (x ∷ t) a dec next-dec L = | |
| 38 qlist qs dec L ∷ ( ntrace Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a (next-dec qs dec x) next-dec L ) | |
| 39 | |
| 40 data exists-in-Q3 (P : Q3 → Set) : Set where | |
| 41 qe1 : P q₁ → exists-in-Q3 P | |
| 42 qe2 : P q₂ → exists-in-Q3 P | |
| 43 qe3 : P q₃ → exists-in-Q3 P | |
| 0 | 44 |
| 9 | 45 record FindQ {n : Level} (Q : Set n) (Nexists : (Q → Set) → Set) : Set (Suc n) where |
| 46 field | |
| 10 | 47 create : {P : Q → Set} (q : Q ) → P q → Nexists (λ q → P q) |
| 48 found : {P : Q → Set} → Nexists (λ q → P q) → Q | |
| 49 exists : {P : Q → Set} → (n : Nexists (λ q → P q)) → P (found n) | |
| 9 | 50 |
| 51 FindQ3 : FindQ Q3 exists-in-Q3 | |
| 52 FindQ3 = record { create = create ; found = found ; exists = exists } where | |
| 10 | 53 create : {P : Q3 → Set} (q : Q3) → P q → exists-in-Q3 P |
| 54 create q₁ p = qe1 p | |
| 55 create q₂ p = qe2 p | |
| 56 create q₃ p = qe3 p | |
| 57 found : {P : Q3 → Set} → exists-in-Q3 P → Q3 | |
| 58 found (qe1 x) = q₁ | |
| 59 found (qe2 x) = q₂ | |
| 60 found (qe3 x) = q₃ | |
| 61 exists : {P : Q3 → Set} (n : exists-in-Q3 P) → P (found n) | |
| 62 exists (qe1 x) = x | |
| 63 exists (qe2 x) = x | |
| 64 exists (qe3 x) = x | |
| 9 | 65 |
| 0 | 66 data transition136 : Q3 → Σ2 → Q3 → Set where |
| 67 d0 : transition136 q₁ s1 q₂ | |
| 68 d1 : transition136 q₁ s0 q₁ | |
| 69 d2 : transition136 q₂ s0 q₂ | |
| 70 d3 : transition136 q₂ s0 q₃ | |
| 71 d4 : transition136 q₂ s1 q₃ | |
| 72 d5 : transition136 q₃ s0 q₁ | |
| 73 | |
| 74 start136 : Q3 → Set | |
| 75 start136 q = q ≡ q₁ | |
| 76 | |
| 77 nfa136 : NAutomaton Q3 Σ2 | |
| 2 | 78 nfa136 = record { Nδ = transition136 ; NF = λ q → q ≡ q₁ } |
| 0 | 79 |
| 2 | 80 example136-1 = naccept exists-in-Q3 nfa136 start136 ( s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] ) |
| 0 | 81 |
| 2 | 82 example136-0 = naccept exists-in-Q3 nfa136 start136 ( s0 ∷ [] ) |
| 0 | 83 |
| 2 | 84 example136-2 = naccept exists-in-Q3 nfa136 start136 ( s1 ∷ s0 ∷ s1 ∷ s0 ∷ s1 ∷ [] ) |
| 0 | 85 |
| 2 | 86 subset-construction : {n : Level} { Q : Set n } { Σ : Set } → (Nexists : (Q → Set) → Set) → |
| 0 | 87 (NAutomaton Q Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ |
| 2 | 88 subset-construction {n} {Q} { Σ} Nexists nfa = record { |
| 89 δ = λ qs x q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' ) | |
|
8
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
90 ; F = λ qs → Nexists ( λ q → qs q ∧ NF nfa q ) |
| 0 | 91 } |
| 92 | |
| 2 | 93 dfa136 : Automaton (Q3 → Set) Σ2 |
| 94 dfa136 = subset-construction exists-in-Q3 nfa136 | |
| 95 | |
| 96 t136 : accept dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ []) → List ( Q3 → Set ) | |
| 9 | 97 t136 = trace dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] ) |
| 2 | 98 |
|
8
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
99 open _∧_ |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
100 |
| 0 | 101 subset-construction-lemma→ : { Q : Set } { Σ : Set } → |
| 2 | 102 (Nexists : (Q → Set) → Set) → |
| 0 | 103 (NFA : NAutomaton Q Σ ) → (astart : Q → Set ) |
| 104 → (x : List Σ) | |
| 2 | 105 → naccept Nexists NFA ( λ q1 → astart q1) x |
| 106 → accept ( subset-construction Nexists NFA ) ( λ q1 → astart q1) x | |
|
8
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
107 subset-construction-lemma→ {Q} {Σ} Nexists nfa qs [] na = na |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
108 subset-construction-lemma→ {Q} {Σ} Nexists nfa qs (x ∷ t) na = |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
109 subset-construction-lemma→ Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t na |
| 0 | 110 |
| 111 subset-construction-lemma← : { Q : Set } { Σ : Set } → | |
| 2 | 112 (Nexists : (Q → Set) → Set) → |
| 0 | 113 (NFA : NAutomaton Q Σ ) → (astart : Q → Set ) |
| 114 → (x : List Σ) | |
| 2 | 115 → accept ( subset-construction Nexists NFA ) ( λ q1 → astart q1) x |
| 116 → naccept Nexists NFA ( λ q1 → astart q1) x | |
|
8
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
117 subset-construction-lemma← {Q} {Σ} Nexists nfa qs [] a = a |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
118 subset-construction-lemma← {Q} {Σ} Nexists nfa qs (x ∷ t) a = |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
119 subset-construction-lemma← Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a |
| 0 | 120 |
| 121 open import regular-language | |
| 122 | |
| 123 open RegularLanguage | |
| 124 open Automaton | |
| 125 open import Data.Empty | |
| 126 | |
| 2 | 127 Union-Nexists : {n m : Level} → {A : Set n} → {B : Set m} → ( (A → Set) → Set )→ ( (B → Set) → Set ) → ( (A ∨ B → Set) → Set ) |
| 128 Union-Nexists {n} {m} {A} {B} PA PB P = PA (λ q → P (case1 q)) ∨ PB (λ q → P (case2 q)) | |
| 0 | 129 |
| 2 | 130 Concat-NFA : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → NAutomaton (states A ∨ states B) Σ |
| 131 Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend } | |
| 0 | 132 module Concat-NFA where |
| 133 data δnfa : states A ∨ states B → Σ → states A ∨ states B → Set where | |
| 134 a-case : {q : states A} {i : Σ } → δnfa ( case1 q) i (case1 (δ (automaton A) q i)) | |
| 135 ab-trans : {q : states A} {i : Σ } → F (automaton A) q → δnfa ( case1 q) i (case2 (δ (automaton B) (astart B) i)) | |
| 136 b-case : {q : states B} {i : Σ } → δnfa ( case2 q) i (case2 (δ (automaton B) q i)) | |
| 137 nend : states A ∨ states B → Set | |
| 138 nend (case2 q) = F (automaton B) q | |
| 139 nend (case1 q) = F (automaton A) q ∧ F (automaton B) (astart B) -- empty B case | |
| 140 | |
| 10 | 141 data state-is {n : Level} {Σ : Set } (A B : RegularLanguage {n} Σ ) : (q : states A ∨ states B ) → Set where |
| 142 this : state-is A B (case1 (astart A)) | |
| 143 | |
| 144 record Split {Σ : Set} (A : List Σ → Set ) ( B : List Σ → Set ) (x : List Σ ) : Set where | |
| 145 field | |
| 146 sp0 : List Σ | |
| 147 sp1 : List Σ | |
| 148 sp-concat : sp0 ++ sp1 ≡ x | |
| 149 prop0 : A sp0 | |
| 150 prop1 : B sp1 | |
| 151 | |
| 152 open Split | |
| 153 split→AB : {Σ : Set} → (A B : List Σ → Set ) → ( x : List Σ ) → split A B x → Split A B x | |
| 154 split→AB A B [] sp = record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = proj1 sp ; prop1 = proj2 sp } | |
| 155 split→AB A B (x ∷ t) (case1 sp) = record { sp0 = [] ; sp1 = x ∷ t ; sp-concat = refl ; prop0 = proj1 sp ; prop1 = proj2 sp } | |
| 156 split→AB A B (x ∷ t) (case2 sp) with split→AB (λ t1 → A ( x ∷ t1 )) B t sp | |
| 157 ... | Sn = record { sp0 = x ∷ sp0 Sn ; sp1 = sp1 Sn ; sp-concat = cong (λ k → x ∷ k) (sp-concat Sn) ; prop0 = prop0 Sn ; prop1 = prop1 Sn } | |
| 0 | 158 |
| 159 closed-in-concat : {n : Level} {Σ : Set } → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) | |
| 9 | 160 (PA : (states A → Set) → Set) (FA : FindQ (states A) PA) |
| 161 (PB : (states B → Set) → Set) (FB : FindQ (states B) PB) | |
| 10 | 162 → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A B q |
| 2 | 163 ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )} |
| 9 | 164 closed-in-concat {n} {Σ} A B x PA FA PB FB = [ closed-in-concat→ x , closed-in-concat← x ] where |
| 165 open FindQ | |
|
8
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
166 fa : RegularLanguage Σ |
| 10 | 167 fa = record {states = states A ∨ states B → Set ; astart = λ q → state-is A B q |
|
8
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
168 ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )} |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
169 closed-in-concat→ : (x : List Σ) → Concat {n} {Σ} (contain A) (contain B) x → contain fa x |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
170 closed-in-concat→ [] c = cc1 c where |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
171 cc1 : contain A [] ∧ contain B [] → |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
172 PA (λ q → astart fa (case1 q) ∧ NF (Concat-NFA A B) (case1 q)) ∨ PB (λ q → astart fa (case2 q) ∧ NF (Concat-NFA A B) (case2 q)) |
| 10 | 173 cc1 ctab = case1 (create FA (astart A) [ this , [ proj1 ctab , proj2 ctab ] ] ) |
| 174 -- fina : (F (automaton A) (astart A) ∧ accept (automaton B) (δ (automaton B) (astart B) x) t) | |
| 175 closed-in-concat→ (x ∷ t) (case1 fina ) = {!!} | |
| 176 -- sp : split (λ t1 → accept (automaton A) (δ (automaton A) (astart A) x) t1) (λ x₁ → accept (automaton B) (astart B) x₁) t | |
| 177 closed-in-concat→ (x ∷ t) (case2 sp ) = {!!} | |
|
8
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
178 closed-in-concat← : (x : List Σ) → contain fa x → Concat {n} {Σ} (contain A) (contain B) x |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
179 closed-in-concat← [] cn = cc2 cn where |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
180 cc2 : PA (λ q → astart fa (case1 q) ∧ NF (Concat-NFA A B) (case1 q)) ∨ PB (λ q → astart fa (case2 q) ∧ NF (Concat-NFA A B) (case2 q)) |
|
894feefc3084
subset construction lemma
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
7
diff
changeset
|
181 → contain A [] ∧ contain B [] |
| 10 | 182 -- ca : PA (λ q → state-is A B (case1 q) ∧ F (automaton A) q ∧ F (automaton B) (astart B)) |
| 183 cc2 (case1 ca) = [ subst (λ k → accept (automaton A) k [] ) (cc5 _ (proj1 (exists FA ca))) cc3 , proj2 (proj2 (exists FA ca)) ] where | |
| 184 cc5 : (q : states A) → state-is A B (case1 q) → q ≡ astart A | |
| 185 cc5 q this = refl | |
| 186 cc3 : accept (automaton A) (found FA ca ) [] | |
| 187 cc3 = proj1 (proj2 (exists FA ca)) | |
| 188 cc2 (case2 cb) with proj1 (exists FB cb) | |
| 189 ... | () | |
| 190 closed-in-concat← (x ∷ t) cn = {!!} | |
| 0 | 191 |
| 192 | |
| 193 | |
| 194 | |
| 195 |