Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/nfa136.agda @ 410:db02b6938e04
StarProp and Ntrace
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 22 Nov 2023 17:07:01 +0900 |
| parents | 3d0aa205edf9 |
| children |
| rev | line source |
|---|---|
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 module nfa136 where |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import logic |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import nfa |
| 141 | 5 open import automaton |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Data.List |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import Data.Fin |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 data StatesQ : Set where |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 q1 : StatesQ |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 q2 : StatesQ |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 q3 : StatesQ |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 data A2 : Set where |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 a0 : A2 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 b0 : A2 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 transition136 : StatesQ → A2 → StatesQ → Bool |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 transition136 q1 b0 q2 = true |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 transition136 q1 a0 q1 = true -- q1 → ep → q3 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 transition136 q2 a0 q2 = true |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 transition136 q2 a0 q3 = true |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 transition136 q2 b0 q3 = true |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 transition136 q3 a0 q1 = true |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 transition136 _ _ _ = false |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 end136 : StatesQ → Bool |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 end136 q1 = true |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 end136 _ = false |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 start136 : StatesQ → Bool |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 start136 q1 = true |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 start136 _ = false |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 |
| 141 | 36 exists136 : (StatesQ → Bool) → Bool |
| 37 exists136 f = f q1 \/ f q2 \/ f q3 | |
| 38 | |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 nfa136 : NAutomaton StatesQ A2 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 nfa136 = record { Nδ = transition136; Nend = end136 } |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 |
| 332 | 42 states136 = q1 ∷ q2 ∷ q3 ∷ [] |
| 43 | |
| 141 | 44 example136-1 = Naccept nfa136 exists136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] ) |
| 45 | |
| 332 | 46 t146-1 = Ntrace nfa136 states136 exists136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] ) |
| 47 | |
| 408 | 48 -- test111 = ? |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 |
| 141 | 50 example136-0 = Naccept nfa136 exists136 start136( a0 ∷ [] ) |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 |
| 141 | 52 example136-2 = Naccept nfa136 exists136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] ) |
| 332 | 53 t146-2 = Ntrace nfa136 states136 exists136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] ) |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 nx : (StatesQ → Bool) → (List A2 ) → StatesQ → Bool |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 nx now [] = now |
| 141 | 57 nx now ( i ∷ ni ) = (Nmoves nfa136 exists136 (nx now ni) i ) |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 |
| 332 | 59 example136-3 = to-list states136 start136 |
| 60 example136-4 = to-list states136 (nx start136 ( a0 ∷ b0 ∷ a0 ∷ [] )) | |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 open import sbconst2 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 fm136 : Automaton ( StatesQ → Bool ) A2 |
| 141 | 65 fm136 = subset-construction exists136 nfa136 |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 open NAutomaton |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 |
| 141 | 69 lemma136 : ( x : List A2 ) → Naccept nfa136 exists136 start136 x ≡ accept fm136 start136 x |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 lemma136 x = lemma136-1 x start136 where |
|
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 lemma136-1 : ( x : List A2 ) → ( states : StatesQ → Bool ) |
| 141 | 72 → Naccept nfa136 exists136 states x ≡ accept fm136 states x |
|
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 lemma136-1 [] _ = refl |
| 141 | 74 lemma136-1 (h ∷ t) states = lemma136-1 t (δconv exists136 (Nδ nfa136) states h) |
| 332 | 75 |
| 76 data Σ2 : Set where | |
| 77 ca : Σ2 | |
| 78 cb : Σ2 | |
| 79 cc : Σ2 | |
| 80 cf : Σ2 | |
| 81 | |
| 82 data Q2 : Set where | |
| 83 a0 : Q2 | |
| 84 a1 : Q2 | |
| 85 ae : Q2 | |
| 408 | 86 af : Q2 |
| 332 | 87 b0 : Q2 |
| 88 b1 : Q2 | |
| 89 be : Q2 | |
| 408 | 90 bf : Q2 |
| 332 | 91 |
| 92 -- a.*f | |
| 93 | |
| 94 a-end : Q2 → Bool | |
| 95 a-end ae = true | |
| 96 a-end _ = false | |
| 97 | |
| 408 | 98 aδ : Q2 → Σ2 → Q2 |
| 99 aδ a0 ca = a1 | |
| 410 | 100 aδ a0 cb = af |
| 101 aδ a0 cc = af | |
| 102 aδ a0 cf = af | |
| 408 | 103 aδ a1 cf = ae |
| 104 aδ a1 _ = a1 | |
| 105 aδ ae cf = ae | |
| 106 aδ ae _ = a1 | |
| 107 aδ _ _ = af | |
| 108 fa-a : Automaton Q2 Σ2 | |
| 109 fa-a = record { δ = aδ ; aend = a-end } | |
| 110 | |
| 111 test111 : Bool | |
| 112 test111 = accept fa-a a0 ( ca ∷ cf ∷ ca ∷ [] ) | |
| 113 | |
| 410 | 114 -- b.*f |
| 115 | |
| 408 | 116 b-end : Q2 → Bool |
| 117 b-end be = true | |
| 118 b-end _ = false | |
| 119 | |
| 120 bδ : Q2 → Σ2 → Q2 | |
| 410 | 121 bδ ae cb = b1 |
| 122 bδ ae _ = bf | |
| 408 | 123 bδ b1 cf = be |
| 124 bδ b1 _ = b1 | |
| 125 bδ be cf = be | |
| 126 bδ be _ = b1 | |
| 127 bδ _ _ = bf | |
| 128 fa-b : Automaton Q2 Σ2 | |
| 129 fa-b = record { δ = bδ ; aend = b-end } | |
| 130 | |
| 131 test115 : Bool | |
| 132 test115 = accept fa-b b0 ( cb ∷ cf ∷ cf ∷ [] ) | |
| 133 | |
| 134 open import regular-language | |
| 135 | |
| 410 | 136 -- (a.*f)(b.*f) -- a.*(fb).*f |
| 408 | 137 test116 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ cb ∷ cf ∷ cf ∷ [] ) |
| 410 | 138 -- a0 ae b0 b1 be |
| 139 test117 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ ca ∷ cb ∷ ca ∷ cf ∷ cf ∷ [] ) | |
| 140 -- a0 ae a0 b0 b1 be | |
| 141 -- a0 ae ae b0 b1 be | |
| 408 | 142 |
| 143 naδ : Q2 → Σ2 → Q2 → Bool | |
| 144 naδ a0 ca a1 = true | |
| 145 naδ a0 _ _ = false | |
| 146 naδ a1 cf ae = true | |
| 147 naδ a1 _ a1 = true | |
| 410 | 148 naδ ae cf ae = true |
| 149 naδ ae _ a1 = true | |
| 408 | 150 naδ _ _ _ = false |
| 151 | |
| 332 | 152 a-start : Q2 → Bool |
| 153 a-start a0 = true | |
| 154 a-start _ = false | |
| 155 | |
| 156 nfa-a : NAutomaton Q2 Σ2 | |
| 408 | 157 nfa-a = record { Nδ = naδ ; Nend = a-end } |
| 332 | 158 |
| 159 nfa-a-exists : (Q2 → Bool) → Bool | |
| 160 nfa-a-exists p = p a0 \/ p a1 \/ p ae | |
| 161 | |
| 162 test-a1 : Bool | |
| 163 test-a1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ [] ) | |
| 164 | |
| 408 | 165 -- test-a2 = map reverse ( NtraceDepth nfa-a a-start (a0 ∷ a1 ∷ ae ∷ []) ( ca ∷ cf ∷ cf ∷ [] ) ) |
| 332 | 166 |
| 167 -- b.*f | |
| 168 | |
| 408 | 169 nbδ : Q2 → Σ2 → Q2 → Bool |
| 170 nbδ ae cb b1 = true | |
| 171 nbδ ae _ _ = false | |
| 172 nbδ b1 cf be = true | |
| 173 nbδ b1 _ b1 = true | |
| 410 | 174 nbδ be cf be = true |
| 175 nbδ be _ b1 = true | |
| 408 | 176 nbδ _ _ _ = false |
| 332 | 177 |
| 178 b-start : Q2 → Bool | |
| 179 b-start ae = true | |
| 180 b-start _ = false | |
| 181 | |
| 182 nfa-b : NAutomaton Q2 Σ2 | |
| 408 | 183 nfa-b = record { Nδ = nbδ ; Nend = b-end } |
| 332 | 184 |
| 185 nfa-b-exists : (Q2 → Bool) → Bool | |
| 410 | 186 nfa-b-exists p = p b0 \/ p b1 \/ p be |
| 332 | 187 |
| 188 -- (a.*f)(b.*f) | |
| 189 | |
| 190 abδ : Q2 → Σ2 → Q2 → Bool | |
| 408 | 191 abδ x i y = naδ x i y \/ nbδ x i y |
| 332 | 192 |
| 193 nfa-ab : NAutomaton Q2 Σ2 | |
| 194 nfa-ab = record { Nδ = abδ ; Nend = b-end } | |
| 195 | |
| 196 nfa-ab-exists : (Q2 → Bool) → Bool | |
| 197 nfa-ab-exists p = nfa-a-exists p \/ nfa-b-exists p | |
| 198 | |
| 410 | 199 test-ab1-data : List Σ2 |
| 200 test-ab1-data = ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ) | |
| 201 | |
| 332 | 202 test-ab1 : Bool |
| 410 | 203 test-ab1 = Naccept nfa-ab nfa-ab-exists a-start test-ab1-data -- should be false |
| 204 | |
| 205 test-ab2-data : List Σ2 | |
| 206 test-ab2-data = ( ca ∷ cf ∷ ca ∷ cf ∷ cb ∷ cb ∷ cf ∷ [] ) | |
| 332 | 207 |
| 208 test-ab2 : Bool | |
| 410 | 209 test-ab2 = Naccept nfa-ab nfa-ab-exists a-start test-ab2-data -- should be true |
| 210 | |
| 211 q2-list : List Q2 | |
| 212 q2-list = a0 ∷ a1 ∷ ae ∷ af ∷ b0 ∷ b1 ∷ be ∷ bf ∷ [] | |
| 213 | |
| 214 test-tr : List (List Q2) | |
| 215 test-tr = Ntrace nfa-ab q2-list nfa-ab-exists a-start ( ca ∷ cf ∷ cf ∷ cb ∷ cb ∷ cf ∷ [] ) | |
| 332 | 216 |
| 408 | 217 -- test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae ∷ b0 ∷ b1 ∷ be ∷ []) ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )) |
| 332 | 218 |
| 219 test112 : Automaton (Q2 → Bool) Σ2 | |
| 220 test112 = subset-construction nfa-ab-exists nfa-ab | |
| 221 | |
| 222 test114 = Automaton.δ (subset-construction nfa-ab-exists nfa-ab) | |
| 223 | |
| 224 test113 : Bool | |
| 225 test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] ) | |
| 226 | |
| 408 | 227 -- |
| 410 | 228 open import regex |
| 229 open import Relation.Nullary using (¬_; Dec; yes; no) | |
| 230 | |
| 231 Σ2-cmp : (x y : Σ2 ) → Dec (x ≡ y) | |
| 232 Σ2-cmp ca ca = yes refl | |
| 233 Σ2-cmp ca cb = no (λ ()) | |
| 234 Σ2-cmp ca cc = no (λ ()) | |
| 235 Σ2-cmp ca cf = no (λ ()) | |
| 236 Σ2-cmp cb ca = no (λ ()) | |
| 237 Σ2-cmp cb cb = yes refl | |
| 238 Σ2-cmp cb cc = no (λ ()) | |
| 239 Σ2-cmp cb cf = no (λ ()) | |
| 240 Σ2-cmp cc ca = no (λ ()) | |
| 241 Σ2-cmp cc cb = no (λ ()) | |
| 242 Σ2-cmp cc cc = yes refl | |
| 243 Σ2-cmp cc cf = no (λ ()) | |
| 244 Σ2-cmp cf ca = no (λ ()) | |
| 245 Σ2-cmp cf cb = no (λ ()) | |
| 246 Σ2-cmp cf cc = no (λ ()) | |
| 247 Σ2-cmp cf cf = yes refl | |
| 248 | |
| 249 Σ2-any : Regex Σ2 | |
| 250 Σ2-any = < ca > || < cb > || < cc > || < cf > | |
| 251 | |
| 252 test-ab1-regex : regex-language ( (< ca > & (Σ2-any *) & < cf > ) & (< cb > & (Σ2-any *) & < cf > ) ) Σ2-cmp test-ab1-data ≡ false | |
| 253 test-ab1-regex = refl | |
| 254 | |
| 255 test-ab2-regex : regex-language ( (< ca > & (Σ2-any *) & < cf > ) & (< cb > & (Σ2-any *) & < cf > ) ) Σ2-cmp test-ab2-data ≡ true | |
| 256 test-ab2-regex = refl | |
| 408 | 257 |
| 258 | |
| 259 | |
| 260 |