Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/nfa136.agda @ 408:3d0aa205edf9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 15 Nov 2023 16:24:07 +0900 |
| parents | 6f3636fbc481 |
| children | db02b6938e04 |
| 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 | |
| 100 aδ a0 _ = af | |
| 101 aδ a1 cf = ae | |
| 102 aδ a1 _ = a1 | |
| 103 aδ ae cf = ae | |
| 104 aδ ae _ = a1 | |
| 105 aδ _ _ = af | |
| 106 fa-a : Automaton Q2 Σ2 | |
| 107 fa-a = record { δ = aδ ; aend = a-end } | |
| 108 | |
| 109 test111 : Bool | |
| 110 test111 = accept fa-a a0 ( ca ∷ cf ∷ ca ∷ [] ) | |
| 111 | |
| 112 b-end : Q2 → Bool | |
| 113 b-end be = true | |
| 114 b-end _ = false | |
| 115 | |
| 116 bδ : Q2 → Σ2 → Q2 | |
| 117 bδ b0 cb = b1 | |
| 118 bδ b0 _ = bf | |
| 119 bδ b1 cf = be | |
| 120 bδ b1 _ = b1 | |
| 121 bδ be cf = be | |
| 122 bδ be _ = b1 | |
| 123 bδ _ _ = bf | |
| 124 fa-b : Automaton Q2 Σ2 | |
| 125 fa-b = record { δ = bδ ; aend = b-end } | |
| 126 | |
| 127 test115 : Bool | |
| 128 test115 = accept fa-b b0 ( cb ∷ cf ∷ cf ∷ [] ) | |
| 129 | |
| 130 open import regular-language | |
| 131 | |
| 132 test116 = split (accept fa-a a0) (accept fa-b b0) ( ca ∷ cf ∷ cb ∷ cf ∷ cf ∷ [] ) | |
| 133 | |
| 134 naδ : Q2 → Σ2 → Q2 → Bool | |
| 135 naδ a0 ca a1 = true | |
| 136 naδ a0 _ _ = false | |
| 137 naδ a1 cf ae = true | |
| 138 naδ a1 _ a1 = true | |
| 139 naδ _ _ _ = false | |
| 140 | |
| 332 | 141 a-start : Q2 → Bool |
| 142 a-start a0 = true | |
| 143 a-start _ = false | |
| 144 | |
| 145 nfa-a : NAutomaton Q2 Σ2 | |
| 408 | 146 nfa-a = record { Nδ = naδ ; Nend = a-end } |
| 332 | 147 |
| 148 nfa-a-exists : (Q2 → Bool) → Bool | |
| 149 nfa-a-exists p = p a0 \/ p a1 \/ p ae | |
| 150 | |
| 151 test-a1 : Bool | |
| 152 test-a1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ [] ) | |
| 153 | |
| 408 | 154 -- test-a2 = map reverse ( NtraceDepth nfa-a a-start (a0 ∷ a1 ∷ ae ∷ []) ( ca ∷ cf ∷ cf ∷ [] ) ) |
| 332 | 155 |
| 156 -- b.*f | |
| 157 | |
| 408 | 158 nbδ : Q2 → Σ2 → Q2 → Bool |
| 159 nbδ ae cb b1 = true | |
| 160 nbδ ae _ _ = false | |
| 161 nbδ b1 cf be = true | |
| 162 nbδ b1 _ b1 = true | |
| 163 nbδ _ _ _ = false | |
| 332 | 164 |
| 165 b-start : Q2 → Bool | |
| 166 b-start ae = true | |
| 167 b-start _ = false | |
| 168 | |
| 169 nfa-b : NAutomaton Q2 Σ2 | |
| 408 | 170 nfa-b = record { Nδ = nbδ ; Nend = b-end } |
| 332 | 171 |
| 172 nfa-b-exists : (Q2 → Bool) → Bool | |
| 173 nfa-b-exists p = p b0 \/ p b1 \/ p ae | |
| 174 | |
| 175 -- (a.*f)(b.*f) | |
| 176 | |
| 177 abδ : Q2 → Σ2 → Q2 → Bool | |
| 408 | 178 abδ x i y = naδ x i y \/ nbδ x i y |
| 332 | 179 |
| 180 nfa-ab : NAutomaton Q2 Σ2 | |
| 181 nfa-ab = record { Nδ = abδ ; Nend = b-end } | |
| 182 | |
| 183 nfa-ab-exists : (Q2 → Bool) → Bool | |
| 184 nfa-ab-exists p = nfa-a-exists p \/ nfa-b-exists p | |
| 185 | |
| 186 test-ab1 : Bool | |
| 187 test-ab1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ) | |
| 188 | |
| 189 test-ab2 : Bool | |
| 190 test-ab2 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] ) | |
| 191 | |
| 408 | 192 -- test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae ∷ b0 ∷ b1 ∷ be ∷ []) ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )) |
| 332 | 193 |
| 194 test112 : Automaton (Q2 → Bool) Σ2 | |
| 195 test112 = subset-construction nfa-ab-exists nfa-ab | |
| 196 | |
| 197 test114 = Automaton.δ (subset-construction nfa-ab-exists nfa-ab) | |
| 198 | |
| 199 test113 : Bool | |
| 200 test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] ) | |
| 201 | |
| 408 | 202 -- |
| 203 | |
| 204 | |
| 205 | |
| 206 | |
| 207 | |
| 208 |