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