Mercurial > hg > Members > kono > Proof > automaton
annotate agda/nfa.agda @ 89:e919e82e95a2
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 Nov 2019 12:21:44 +0900 |
| parents | f124fceba460 |
| children | b3f05cd08d24 |
| rev | line source |
|---|---|
| 25 | 1 module nfa where |
| 2 | |
| 3 -- open import Level renaming ( suc to succ ; zero to Zero ) | |
| 4 open import Data.Nat | |
| 5 open import Data.List | |
| 27 | 6 open import Data.Fin hiding ( _<_ ) |
| 25 | 7 open import Data.Maybe |
| 27 | 8 open import Relation.Nullary |
| 9 open import Data.Empty | |
| 69 | 10 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ ) |
| 25 | 11 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 12 open import Relation.Nullary using (¬_; Dec; yes; no) | |
| 44 | 13 open import finiteSet |
| 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 | |
|
29
2887577a3d63
simpler exists , nfa accept dones not wokred
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
34 finState1 : FiniteSet States1 |
| 25 | 35 finState1 = record { |
| 30 | 36 Q←F = Q←F |
| 26 | 37 ; F←Q = F←Q |
| 38 ; finiso→ = finiso→ | |
| 39 ; finiso← = finiso← | |
| 25 | 40 } where |
| 27 | 41 Q←F : Fin 3 → States1 |
| 25 | 42 Q←F zero = sr |
| 43 Q←F (suc zero) = ss | |
| 44 Q←F (suc (suc zero)) = st | |
| 26 | 45 F←Q : States1 → Fin 3 |
| 46 F←Q sr = zero | |
| 69 | 47 F←Q ss = suc zero |
| 48 F←Q st = suc (suc zero) | |
| 26 | 49 finiso→ : (q : States1) → Q←F (F←Q q) ≡ q |
| 50 finiso→ sr = refl | |
| 51 finiso→ ss = refl | |
| 52 finiso→ st = refl | |
| 53 finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f | |
| 54 finiso← zero = refl | |
| 55 finiso← (suc zero) = refl | |
| 56 finiso← (suc (suc zero)) = refl | |
| 27 | 57 finiso← (suc (suc (suc ()))) |
| 26 | 58 |
| 25 | 59 |
| 60 open FiniteSet | |
| 61 | |
| 62 Nmoves : { Q : Set } { Σ : Set } | |
| 63 → NAutomaton Q Σ | |
|
29
2887577a3d63
simpler exists , nfa accept dones not wokred
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
64 → {n : ℕ } → FiniteSet Q {n} |
| 69 | 65 → ( Qs : Q → Bool ) → (s : Σ ) → Q → Bool |
| 25 | 66 Nmoves {Q} { Σ} M fin Qs s q = |
| 69 | 67 exists fin ( λ qn → (Qs qn /\ ( Nδ M qn s q ) )) |
| 25 | 68 |
| 69 | |
| 70 Naccept : { Q : Set } { Σ : Set } | |
| 71 → NAutomaton Q Σ | |
|
29
2887577a3d63
simpler exists , nfa accept dones not wokred
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
72 → {n : ℕ } → FiniteSet Q {n} |
| 69 | 73 → (Nstart : Q → Bool) → List Σ → Bool |
| 74 Naccept M fin sb [] = exists fin ( λ q → sb q /\ Nend M q ) | |
| 75 Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M fin sb i ) t | |
| 25 | 76 |
| 77 | |
| 78 transition3 : States1 → In2 → States1 → Bool | |
| 79 transition3 sr i0 sr = true | |
| 80 transition3 sr i1 ss = true | |
| 81 transition3 sr i1 sr = true | |
| 82 transition3 ss i0 sr = true | |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
83 transition3 ss i1 st = true |
| 25 | 84 transition3 st i0 sr = true |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
85 transition3 st i1 st = true |
| 25 | 86 transition3 _ _ _ = false |
| 87 | |
| 88 fin1 : States1 → Bool | |
| 89 fin1 st = true | |
| 90 fin1 ss = false | |
| 91 fin1 sr = false | |
| 92 | |
| 93 start1 : States1 → Bool | |
| 94 start1 sr = true | |
|
29
2887577a3d63
simpler exists , nfa accept dones not wokred
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
95 start1 _ = false |
| 25 | 96 |
| 97 am2 : NAutomaton States1 In2 | |
| 69 | 98 am2 = record { Nδ = transition3 ; Nend = fin1} |
| 99 | |
| 100 example2-1 = Naccept am2 finState1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) | |
| 101 example2-2 = Naccept am2 finState1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 25 | 102 |
| 69 | 103 transition4 : States1 → In2 → States1 → Bool |
| 104 transition4 sr i0 sr = true | |
| 105 transition4 sr i1 ss = true | |
| 106 transition4 sr i1 sr = true | |
| 107 transition4 ss i0 ss = true | |
| 108 transition4 ss i1 st = true | |
| 109 transition4 st i0 st = true | |
| 110 transition4 st i1 st = true | |
| 111 transition4 _ _ _ = false | |
| 112 | |
| 113 fin4 : States1 → Bool | |
| 114 fin4 st = true | |
| 115 fin4 _ = false | |
| 116 | |
| 117 start4 : States1 → Bool | |
| 118 start4 ss = true | |
| 119 start4 _ = false | |
| 120 | |
| 121 am4 : NAutomaton States1 In2 | |
| 122 am4 = record { Nδ = transition4 ; Nend = fin4} | |
| 123 | |
| 124 example4-1 = Naccept am4 finState1 start4 ( i0 ∷ i1 ∷ i1 ∷ i0 ∷ [] ) | |
| 125 example4-2 = Naccept am4 finState1 start4 ( i0 ∷ i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 25 | 126 |
| 30 | 127 fin0 : States1 → Bool |
| 128 fin0 st = false | |
| 129 fin0 ss = false | |
| 130 fin0 sr = false | |
| 25 | 131 |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
132 test0 : Bool |
|
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
133 test0 = exists finState1 fin0 |
|
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
134 |
| 30 | 135 test1 : Bool |
| 136 test1 = exists finState1 fin1 | |
| 137 | |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
138 test2 = Nmoves am2 finState1 start1 |
|
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
139 |
| 36 | 140 -- test4 : Fin 2 → Bool |
| 141 -- test4 zero = {!!} | |
| 142 -- test4 (suc zero) = {!!} | |
| 143 -- test4 (suc (suc ())) | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
144 |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
145 -- 0011 |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
146 -- 00000111111 |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
147 inputnn : { n : ℕ } → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
148 inputnn {zero} {_} _ _ s = s |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
149 inputnn {suc n} x y s = x ∷ ( inputnn {n} x y ( y ∷ s ) ) |
| 44 | 150 |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
151 -- lemmaNN : { Q : Set } { Σ : Set } → ( x y : Σ ) → (M : NAutomaton Q Σ) |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
152 -- → ( n : ℕ ) → (fin : FiniteSet Q {n} ) |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
153 -- → Naccept M fin ( inputnn {n} x y [] ) ≡ true |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
154 -- → Naccept M fin ( inputnn {suc n} x y [] ) ≡ false |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
155 -- lemmaNN {Q} {Σ} x y M n fin nac = {!!} |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
156 |