Mercurial > hg > Members > kono > Proof > automaton
annotate agda/automaton.agda @ 108:0117144967bb
case1 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 17 Nov 2019 12:02:17 +0900 |
| parents | b9679ebd1156 |
| children | b3f05cd08d24 |
| rev | line source |
|---|---|
| 0 | 1 module automaton where |
| 2 | |
| 24 | 3 -- open import Level renaming ( suc to succ ; zero to Zero ) |
| 2 | 4 open import Data.Nat |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
5 open import Data.List |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
6 open import Data.Maybe |
| 58 | 7 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ ) |
| 8 open import Relation.Binary.PropositionalEquality hiding ( [_] ) | |
| 9 | 9 open import Relation.Nullary using (¬_; Dec; yes; no) |
| 58 | 10 open import logic |
| 64 | 11 -- open import Data.Bool renaming ( _∧_ to _and_ ; _∨_ to _or ) |
| 0 | 12 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
13 record Automaton ( Q : Set ) ( Σ : Set ) |
| 0 | 14 : Set where |
| 1 | 15 field |
| 16 δ : Q → Σ → Q | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
17 aend : Q → Bool |
| 1 | 18 |
| 19 open Automaton | |
| 0 | 20 |
| 65 | 21 data StatesQ : Set where |
| 22 q1 : StatesQ | |
| 23 q2 : StatesQ | |
| 24 q3 : StatesQ | |
| 25 | |
| 26 data In2 : Set where | |
| 27 i0 : In2 | |
| 28 i1 : In2 | |
| 29 | |
| 30 transitionQ : StatesQ → In2 → StatesQ | |
| 31 transitionQ q1 i0 = q1 | |
| 32 transitionQ q1 i1 = q2 | |
| 33 transitionQ q2 i0 = q3 | |
| 34 transitionQ q2 i1 = q2 | |
| 35 transitionQ q3 i0 = q2 | |
| 36 transitionQ q3 i1 = q2 | |
| 37 | |
| 38 aendQ : StatesQ → Bool | |
| 39 aendQ q2 = true | |
| 40 aendQ _ = false | |
| 41 | |
| 42 a1 : Automaton StatesQ In2 | |
| 43 a1 = record { | |
| 44 δ = transitionQ | |
| 45 ; aend = aendQ | |
| 46 } | |
| 47 | |
| 48 accept : { Q : Set } { Σ : Set } | |
| 49 → Automaton Q Σ | |
| 50 → (astart : Q) | |
| 51 → List Σ → Bool | |
| 52 accept {Q} { Σ} M q [] = aend M q | |
| 53 accept {Q} { Σ} M q ( H ∷ T ) = accept M ( (δ M) q H ) T | |
| 54 | |
| 55 test1 : accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ false | |
| 56 test1 = refl | |
| 57 test2 = accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) | |
| 58 | |
| 0 | 59 data States1 : Set where |
| 1 | 60 sr : States1 |
| 61 ss : States1 | |
| 62 st : States1 | |
| 0 | 63 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
64 moves : { Q : Set } { Σ : Set } |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
65 → Automaton Q Σ |
| 0 | 66 → Q → List Σ → Q |
| 1 | 67 moves {Q} { Σ} M q L = move q L |
| 0 | 68 where |
| 69 move : (q : Q ) ( L : List Σ ) → Q | |
| 70 move q [] = q | |
| 24 | 71 move q ( H ∷ T ) = move ( δ M q H) T |
| 0 | 72 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
73 transition1 : States1 → In2 → States1 |
| 1 | 74 transition1 sr i0 = sr |
| 75 transition1 sr i1 = ss | |
| 76 transition1 ss i0 = sr | |
| 77 transition1 ss i1 = st | |
| 78 transition1 st i0 = sr | |
| 79 transition1 st i1 = st | |
| 0 | 80 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
81 fin1 : States1 → Bool |
| 1 | 82 fin1 st = true |
| 24 | 83 fin1 ss = false |
| 84 fin1 sr = false | |
| 0 | 85 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
86 am1 : Automaton States1 In2 |
| 60 | 87 am1 = record { δ = transition1 ; aend = fin1 } |
| 0 | 88 |
| 89 | |
| 60 | 90 example1-1 = accept am1 sr ( i0 ∷ i1 ∷ i0 ∷ [] ) |
| 91 example1-2 = accept am1 sr ( i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 0 | 92 |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
93 reachable : { Q : Set } { Σ : Set } |
| 1 | 94 → (M : Automaton Q Σ ) |
| 60 | 95 → (astart q : Q ) |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
9
diff
changeset
|
96 → (L : List Σ ) → Set |
| 60 | 97 reachable M astart q L = moves M astart L ≡ q |
| 0 | 98 |
| 60 | 99 example1-3 = reachable am1 sr st ( i1 ∷ i1 ∷ i1 ∷ [] ) |
| 0 | 100 |
| 24 | 101 ieq : (i i' : In2 ) → Dec ( i ≡ i' ) |
| 102 ieq i0 i0 = yes refl | |
| 103 ieq i1 i1 = yes refl | |
| 104 ieq i0 i1 = no ( λ () ) | |
| 105 ieq i1 i0 = no ( λ () ) | |
| 0 | 106 |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
107 inputnn : { n : ℕ } → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
108 inputnn {zero} {_} _ _ s = s |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
109 inputnn {suc n} x y s = x ∷ ( inputnn {n} x y ( y ∷ s ) ) |
|
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
110 |
| 39 | 111 -- lemmaNN : { Q : Set } { Σ : Set } → (M : Automaton Q Σ) → ¬ accept M ( inputnn {n} x y [] ) |
| 112 -- lemmaNN = ? | |
|
38
ab265470c2d0
push down automaton example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
24
diff
changeset
|
113 |