Mercurial > hg > Members > kono > Proof > automaton
annotate agda/nfa.agda @ 143:f896c112f01f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 29 Dec 2020 15:32:57 +0900 |
| parents | b3f05cd08d24 |
| children |
| 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 ( _<_ ) |
| 25 | 8 open import Data.Maybe |
| 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 |
| 141 | 41 -- extract list of q which qs q is true |
| 42 to-listS1 : ( States1 → Bool ) → List States1 | |
| 43 to-listS1 qs = ss1 LStates1 where | |
| 44 ss1 : List States1 → List States1 | |
| 45 ss1 [] = [] | |
| 46 ss1 (x ∷ t) with qs x | |
| 47 ... | true = x ∷ ss1 t | |
| 48 ... | false = ss1 t | |
| 25 | 49 |
| 50 Nmoves : { Q : Set } { Σ : Set } | |
| 51 → NAutomaton Q Σ | |
| 141 | 52 → (exists : ( Q → Bool ) → Bool) |
| 69 | 53 → ( Qs : Q → Bool ) → (s : Σ ) → Q → Bool |
| 141 | 54 Nmoves {Q} { Σ} M exists Qs s q = |
| 55 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 | |
| 64 Ntrace : { Q : Set } { Σ : Set } | |
| 65 → NAutomaton Q Σ | |
| 66 → (exists : ( Q → Bool ) → Bool) | |
| 67 → (to-list : ( Q → Bool ) → List Q ) | |
| 68 → (Nstart : Q → Bool) → List Σ → List (List Q) | |
| 69 Ntrace M exists to-list sb [] = to-list ( λ q → sb q /\ Nend M q ) ∷ [] | |
| 70 Ntrace M exists to-list sb (i ∷ t ) = | |
| 71 to-list (λ q → sb q ) ∷ | |
| 72 Ntrace M exists to-list (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t | |
| 25 | 73 |
| 74 | |
| 75 transition3 : States1 → In2 → States1 → Bool | |
| 76 transition3 sr i0 sr = true | |
| 77 transition3 sr i1 ss = true | |
| 78 transition3 sr i1 sr = true | |
| 79 transition3 ss i0 sr = true | |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
80 transition3 ss i1 st = true |
| 25 | 81 transition3 st i0 sr = true |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
82 transition3 st i1 st = true |
| 25 | 83 transition3 _ _ _ = false |
| 84 | |
| 85 fin1 : States1 → Bool | |
| 86 fin1 st = true | |
| 87 fin1 ss = false | |
| 88 fin1 sr = false | |
| 89 | |
| 141 | 90 test5 = existsS1 (λ q → fin1 q ) |
| 91 test6 = to-listS1 (λ q → fin1 q ) | |
| 92 | |
| 25 | 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 | |
| 141 | 100 example2-1 = Naccept am2 existsS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) |
| 101 example2-2 = Naccept am2 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 102 | |
| 103 t-1 : List ( List States1 ) | |
| 104 t-1 = Ntrace am2 existsS1 to-listS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 105 t-2 = Ntrace am2 existsS1 to-listS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) | |
| 25 | 106 |
| 69 | 107 transition4 : States1 → In2 → States1 → Bool |
| 108 transition4 sr i0 sr = true | |
| 109 transition4 sr i1 ss = true | |
| 110 transition4 sr i1 sr = true | |
| 111 transition4 ss i0 ss = true | |
| 112 transition4 ss i1 st = true | |
| 113 transition4 st i0 st = true | |
| 114 transition4 st i1 st = true | |
| 115 transition4 _ _ _ = false | |
| 116 | |
| 117 fin4 : States1 → Bool | |
| 118 fin4 st = true | |
| 119 fin4 _ = false | |
| 120 | |
| 121 start4 : States1 → Bool | |
| 122 start4 ss = true | |
| 123 start4 _ = false | |
| 124 | |
| 125 am4 : NAutomaton States1 In2 | |
| 126 am4 = record { Nδ = transition4 ; Nend = fin4} | |
| 127 | |
| 141 | 128 example4-1 = Naccept am4 existsS1 start4 ( i0 ∷ i1 ∷ i1 ∷ i0 ∷ [] ) |
| 129 example4-2 = Naccept am4 existsS1 start4 ( i0 ∷ i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 25 | 130 |
| 30 | 131 fin0 : States1 → Bool |
| 132 fin0 st = false | |
| 133 fin0 ss = false | |
| 134 fin0 sr = false | |
| 25 | 135 |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
136 test0 : Bool |
| 141 | 137 test0 = existsS1 fin0 |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
138 |
| 30 | 139 test1 : Bool |
| 141 | 140 test1 = existsS1 fin1 |
|
31
9b00dc130ede
nfa using subset mapping done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
30
diff
changeset
|
141 |
| 141 | 142 test2 = Nmoves am2 existsS1 start1 |
| 143 | |
| 144 open import automaton | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
145 |
| 141 | 146 am2def : Automaton (States1 → Bool ) In2 |
| 147 am2def = record { δ = λ qs s q → existsS1 (λ qn → qs q /\ Nδ am2 q s qn ) | |
| 148 ; aend = λ qs → existsS1 (λ q → qs q /\ Nend am2 q) } | |
| 44 | 149 |
| 141 | 150 dexample4-1 = accept am2def start1 ( i0 ∷ i1 ∷ i1 ∷ i0 ∷ [] ) |
| 151 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
|
152 |