Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/nfa.agda @ 406:a60132983557
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Nov 2023 21:35:54 +0900 |
| parents | af8f630b7e60 |
| children | 207e6c4e155c |
| rev | line source |
|---|---|
| 406 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 2 -- {-# OPTIONS --allow-unsolved-metas #-} | |
| 25 | 3 module nfa where |
| 4 | |
| 5 -- open import Level renaming ( suc to succ ; zero to Zero ) | |
| 6 open import Data.Nat | |
| 7 open import Data.List | |
| 27 | 8 open import Data.Fin hiding ( _<_ ) |
| 267 | 9 open import Data.Maybe hiding ( zip ) |
| 27 | 10 open import Relation.Nullary |
| 11 open import Data.Empty | |
| 69 | 12 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ ) |
| 25 | 13 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 14 open import Relation.Nullary using (¬_; Dec; yes; no) | |
| 69 | 15 open import logic |
| 36 | 16 |
| 25 | 17 data States1 : Set where |
| 18 sr : States1 | |
| 19 ss : States1 | |
| 20 st : States1 | |
| 21 | |
| 22 data In2 : Set where | |
| 23 i0 : In2 | |
| 24 i1 : In2 | |
| 25 | |
| 26 | |
| 27 record NAutomaton ( Q : Set ) ( Σ : Set ) | |
| 28 : Set where | |
| 29 field | |
| 30 Nδ : Q → Σ → Q → Bool | |
| 31 Nend : Q → Bool | |
| 32 | |
| 33 open NAutomaton | |
| 34 | |
| 141 | 35 LStates1 : List States1 |
| 36 LStates1 = sr ∷ ss ∷ st ∷ [] | |
| 37 | |
| 38 -- one of qs q is true | |
| 39 existsS1 : ( States1 → Bool ) → Bool | |
| 40 existsS1 qs = qs sr \/ qs ss \/ qs st | |
| 26 | 41 |
| 332 | 42 -- given list of all states, extract list of q which qs q is true |
| 43 | |
| 44 to-list : {Q : Set} → List Q → ( Q → Bool ) → List Q | |
| 45 to-list {Q} x exists = to-list1 x [] where | |
| 46 to-list1 : List Q → List Q → List Q | |
| 47 to-list1 [] x = x | |
| 48 to-list1 (q ∷ qs) x with exists q | |
| 49 ... | true = to-list1 qs (q ∷ x ) | |
| 50 ... | false = to-list1 qs x | |
| 25 | 51 |
| 52 Nmoves : { Q : Set } { Σ : Set } | |
| 53 → NAutomaton Q Σ | |
| 141 | 54 → (exists : ( Q → Bool ) → Bool) |
| 274 | 55 → ( Qs : Q → Bool ) → (s : Σ ) → ( Q → Bool ) |
| 56 Nmoves {Q} { Σ} M exists Qs s = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q ) )) | |
| 25 | 57 |
| 406 | 58 -- |
| 59 -- Q is finiteSet | |
| 60 -- so we have | |
| 61 -- exists : ( P : Q → Bool ) → Bool | |
| 62 -- which checks if there is a q in Q such that P q is true | |
| 63 | |
| 25 | 64 Naccept : { Q : Set } { Σ : Set } |
| 65 → NAutomaton Q Σ | |
| 141 | 66 → (exists : ( Q → Bool ) → Bool) |
| 69 | 67 → (Nstart : Q → Bool) → List Σ → Bool |
| 141 | 68 Naccept M exists sb [] = exists ( λ q → sb q /\ Nend M q ) |
| 69 Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t | |
| 70 | |
| 406 | 71 -- {-# TERMINATING #-} |
| 72 -- NtraceDepth : { Q : Set } { Σ : Set } | |
| 73 -- → NAutomaton Q Σ | |
| 74 -- → (Nstart : Q → Bool) → (all-states : List Q ) → List Σ → List (List ( Σ ∧ Q )) | |
| 75 -- NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where | |
| 76 -- ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (List ( Σ ∧ Q ) ) → List (List ( Σ ∧ Q ) ) | |
| 77 -- ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( List ( Σ ∧ Q )) → List ( List ( Σ ∧ Q )) | |
| 78 -- ndepth1 q i [] is t t1 = t1 | |
| 79 -- 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 ) | |
| 80 -- ndepth [] sb is t t1 = t1 | |
| 81 -- ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q | |
| 82 -- ... | true = ndepth qs sb [] t ( t ∷ t1 ) | |
| 83 -- ... | false = ndepth qs sb [] t t1 | |
| 84 -- ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q | |
| 85 -- ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 ) | |
| 86 -- ... | false = ndepth qs sb (i ∷ is) t t1 | |
| 332 | 87 |
|
273
192263adfc02
depth first trace in nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
272
diff
changeset
|
88 -- trace in state set |
|
192263adfc02
depth first trace in nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
272
diff
changeset
|
89 -- |
| 141 | 90 Ntrace : { Q : Set } { Σ : Set } |
| 91 → NAutomaton Q Σ | |
| 332 | 92 → (all-states : List Q ) |
| 141 | 93 → (exists : ( Q → Bool ) → Bool) |
| 94 → (Nstart : Q → Bool) → List Σ → List (List Q) | |
| 332 | 95 Ntrace M all-states exists sb [] = to-list all-states ( λ q → sb q /\ Nend M q ) ∷ [] |
| 96 Ntrace M all-states exists sb (i ∷ t ) = | |
| 97 to-list all-states (λ q → sb q ) ∷ | |
| 98 Ntrace M all-states exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t | |
| 25 | 99 |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
100 data-fin-00 : ( Fin 3 ) → Bool |
|
273
192263adfc02
depth first trace in nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
272
diff
changeset
|
101 data-fin-00 zero = true |
|
192263adfc02
depth first trace in nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
272
diff
changeset
|
102 data-fin-00 (suc zero) = true |
|
192263adfc02
depth first trace in nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
272
diff
changeset
|
103 data-fin-00 (suc (suc zero)) = true |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
104 data-fin-00 (suc (suc (suc ()))) |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
105 |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
106 data-fin-01 : (x : ℕ ) → x < 3 → Bool |
|
273
192263adfc02
depth first trace in nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
272
diff
changeset
|
107 data-fin-01 zero lt = true |
|
192263adfc02
depth first trace in nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
272
diff
changeset
|
108 data-fin-01 (suc zero) lt = true |
|
192263adfc02
depth first trace in nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
272
diff
changeset
|
109 data-fin-01 (suc (suc zero)) lt = true |
|
270
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
110 data-fin-01 (suc (suc (suc x))) (s≤s (s≤s (s≤s ()))) |
|
dd98e7e5d4a5
derive worked but finiteness is difficult
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
269
diff
changeset
|
111 |
| 25 | 112 transition3 : States1 → In2 → States1 → Bool |
| 113 transition3 sr i0 sr = true | |
| 114 transition3 sr i1 ss = true | |
| 115 transition3 sr i1 sr = true | |
| 116 transition3 ss i0 sr = true | |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
117 transition3 ss i1 st = true |
| 25 | 118 transition3 st i0 sr = true |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
119 transition3 st i1 st = true |
| 25 | 120 transition3 _ _ _ = false |
| 121 | |
| 122 fin1 : States1 → Bool | |
| 123 fin1 st = true | |
| 124 fin1 ss = false | |
| 125 fin1 sr = false | |
| 126 | |
| 141 | 127 test5 = existsS1 (λ q → fin1 q ) |
| 332 | 128 test6 = to-list LStates1 (λ q → fin1 q ) |
| 141 | 129 |
| 25 | 130 start1 : States1 → Bool |
| 131 start1 sr = true | |
|
29
2887577a3d63
simpler exists , nfa accept dones not wokred
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
132 start1 _ = false |
| 25 | 133 |
| 134 am2 : NAutomaton States1 In2 | |
| 69 | 135 am2 = record { Nδ = transition3 ; Nend = fin1} |
| 136 | |
| 141 | 137 example2-1 = Naccept am2 existsS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) |
| 138 example2-2 = Naccept am2 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 139 | |
| 140 t-1 : List ( List States1 ) | |
| 332 | 141 t-1 = Ntrace am2 LStates1 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ (sr ∷ ss ∷ st ∷ []) ∷ (st ∷ []) ∷ [] |
| 142 t-2 = Ntrace am2 LStates1 existsS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ [] ∷ [] | |
| 406 | 143 -- t-3 = NtraceDepth am2 start1 LStates1 ( i1 ∷ i1 ∷ i1 ∷ [] ) |
| 144 -- t-4 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ i0 ∷ [] ) | |
| 145 -- t-5 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ [] ) | |
| 25 | 146 |
| 69 | 147 transition4 : States1 → In2 → States1 → Bool |
| 148 transition4 sr i0 sr = true | |
| 149 transition4 sr i1 ss = true | |
| 150 transition4 sr i1 sr = true | |
| 151 transition4 ss i0 ss = true | |
| 152 transition4 ss i1 st = true | |
| 153 transition4 st i0 st = true | |
| 154 transition4 st i1 st = true | |
| 155 transition4 _ _ _ = false | |
| 156 | |
| 157 fin4 : States1 → Bool | |
| 158 fin4 st = true | |
| 159 fin4 _ = false | |
| 160 | |
| 161 start4 : States1 → Bool | |
| 162 start4 ss = true | |
| 163 start4 _ = false | |
| 164 | |
| 165 am4 : NAutomaton States1 In2 | |
| 166 am4 = record { Nδ = transition4 ; Nend = fin4} | |
| 167 | |
| 141 | 168 example4-1 = Naccept am4 existsS1 start4 ( i0 ∷ i1 ∷ i1 ∷ i0 ∷ [] ) |
| 169 example4-2 = Naccept am4 existsS1 start4 ( i0 ∷ i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 25 | 170 |
| 30 | 171 fin0 : States1 → Bool |
| 172 fin0 st = false | |
| 173 fin0 ss = false | |
| 174 fin0 sr = false | |
| 25 | 175 |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
176 test0 : Bool |
| 141 | 177 test0 = existsS1 fin0 |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
178 |
| 30 | 179 test1 : Bool |
| 141 | 180 test1 = existsS1 fin1 |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
181 |
| 141 | 182 test2 = Nmoves am2 existsS1 start1 |
| 183 | |
| 184 open import automaton | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
185 |
| 141 | 186 am2def : Automaton (States1 → Bool ) In2 |
| 187 am2def = record { δ = λ qs s q → existsS1 (λ qn → qs q /\ Nδ am2 q s qn ) | |
| 188 ; aend = λ qs → existsS1 (λ q → qs q /\ Nend am2 q) } | |
| 44 | 189 |
| 141 | 190 dexample4-1 = accept am2def start1 ( i0 ∷ i1 ∷ i1 ∷ i0 ∷ [] ) |
| 191 texample4-1 = trace am2def start1 ( i0 ∷ i1 ∷ i1 ∷ i0 ∷ [] ) | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
192 |
| 267 | 193 -- LStates1 contains all states in States1 |
| 194 | |
| 195 -- a list of Q contains (q : Q) | |
| 196 | |
| 197 eqState1? : (x y : States1) → Dec ( x ≡ y ) | |
| 198 eqState1? sr sr = yes refl | |
| 199 eqState1? ss ss = yes refl | |
| 200 eqState1? st st = yes refl | |
| 201 eqState1? sr ss = no (λ ()) | |
| 202 eqState1? sr st = no (λ ()) | |
| 203 eqState1? ss sr = no (λ ()) | |
| 204 eqState1? ss st = no (λ ()) | |
| 205 eqState1? st sr = no (λ ()) | |
| 206 eqState1? st ss = no (λ ()) | |
| 207 | |
| 208 | |
| 209 list-contains : {Q : Set} → ( (x y : Q ) → Dec ( x ≡ y ) ) → (qs : List Q) → (q : Q ) → Bool | |
| 210 list-contains {Q} eq? [] q = false | |
| 211 list-contains {Q} eq? (x ∷ qs) q with eq? x q | |
| 212 ... | yes _ = true | |
| 213 ... | no _ = list-contains eq? qs q | |
| 214 | |
| 215 containsP : {Q : Set} → ( eq? : (x y : Q ) → Dec ( x ≡ y )) → (qs : List Q) → (q : Q ) → Set | |
| 216 containsP eq? qs q = list-contains eq? qs q ≡ true | |
| 217 | |
| 218 contains-all : (q : States1 ) → containsP eqState1? LStates1 q | |
| 219 contains-all sr = refl | |
| 220 contains-all ss = refl | |
| 221 contains-all st = refl | |
| 222 | |
| 268 | 223 -- foldr : (A → B → B) → B → List A → B |
| 224 -- foldr c n [] = n | |
| 225 -- foldr c n (x ∷ xs) = c x (foldr c n xs) | |
| 226 | |
| 227 ssQ : {Q : Set } ( qs : Q → Bool ) → List Q → List Q | |
| 228 ssQ qs [] = [] | |
| 229 ssQ qs (x ∷ t) with qs x | |
| 230 ... | true = x ∷ ssQ qs t | |
| 231 ... | false = ssQ qs t | |
| 232 | |
| 233 bool-t1 : {b : Bool } → b ≡ true → (true /\ b) ≡ true | |
| 234 bool-t1 refl = refl | |
| 235 | |
| 236 bool-1t : {b : Bool } → b ≡ true → (b /\ true) ≡ true | |
| 237 bool-1t refl = refl | |
| 238 | |
| 239 to-list1 : {Q : Set } (qs : Q → Bool ) → (all : List Q) → foldr (λ q x → qs q /\ x ) true (ssQ qs all ) ≡ true | |
| 240 to-list1 qs [] = refl | |
| 405 | 241 to-list1 qs (x ∷ all) with qs x in eq |
| 242 ... | false = to-list1 qs all | |
| 243 ... | true = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) ) | |
| 268 | 244 |
| 245 existsS1-valid : ¬ ( (qs : States1 → Bool ) → ( existsS1 qs ≡ true ) ) | |
| 246 existsS1-valid n = ¬-bool refl ( n ( λ x → false )) | |
| 247 |