Mercurial > hg > Members > kono > Proof > automaton

comparison agda/automaton.agda @ 141:b3f05cd08d24

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 27 Dec 2020 13:26:44 +0900
parents b9679ebd1156
children
comparison
equal deleted inserted replaced
140:4c3fbfde1bc2 141:b3f05cd08d24
1 module automaton where 1 module automaton where
2 2
3 -- open import Level renaming ( suc to succ ; zero to Zero )
4 open import Data.Nat 3 open import Data.Nat
5 open import Data.List 4 open import Data.List
6 open import Data.Maybe
7 -- open import Data.Bool using ( Bool ; true ; false ; _∧_ )
8 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 5 open import Relation.Binary.PropositionalEquality hiding ( [_] )
9 open import Relation.Nullary using (¬_; Dec; yes; no)
10 open import logic 6 open import logic
11 -- open import Data.Bool renaming ( _∧_ to _and_ ; _∨_ to _or )
12 7
13 record Automaton ( Q : Set ) ( Σ : Set ) 8 record Automaton ( Q : Set ) ( Σ : Set )
14 : Set where 9 : Set where
15 field 10 field
16 δ : Q → Σ → Q 11 δ : Q → Σ → Q
17 aend : Q → Bool 12 aend : Q → Bool
18 13
19 open Automaton 14 open Automaton
20 15
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 } 16 accept : { Q : Set } { Σ : Set }
49 → Automaton Q Σ 17 → Automaton Q Σ
50 → (astart : Q) 18 → (astart : Q)
51 → List Σ → Bool 19 → List Σ → Bool
52 accept {Q} { Σ} M q [] = aend M q 20 accept {Q} { Σ} M q [] = aend M q
53 accept {Q} { Σ} M q ( H ∷ T ) = accept M ( (δ M) q H ) T 21 accept {Q} { Σ} M q ( H ∷ T ) = accept M ( (δ M) q H ) T
54 22
55 test1 : accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ false
56 test1 = refl
57 test2 = accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] )
58
59 data States1 : Set where
60 sr : States1
61 ss : States1
62 st : States1
63
64 moves : { Q : Set } { Σ : Set } 23 moves : { Q : Set } { Σ : Set }
65 → Automaton Q Σ 24 → Automaton Q Σ
66 → Q → List Σ → Q 25 → Q → List Σ → Q
67 moves {Q} { Σ} M q L = move q L 26 moves {Q} { Σ} M q [] = q
68 where 27 moves {Q} { Σ} M q ( H ∷ T ) = moves M ( δ M q H) T
69 move : (q : Q ) ( L : List Σ ) → Q
70 move q [] = q
71 move q ( H ∷ T ) = move ( δ M q H) T
72 28
73 transition1 : States1 → In2 → States1 29 trace : { Q : Set } { Σ : Set }
74 transition1 sr i0 = sr 30 → Automaton Q Σ
75 transition1 sr i1 = ss 31 → Q → List Σ → List Q
76 transition1 ss i0 = sr 32 trace {Q} { Σ} M q [] = q ∷ []
77 transition1 ss i1 = st 33 trace {Q} { Σ} M q ( H ∷ T ) = q ∷ trace M ( (δ M) q H ) T
78 transition1 st i0 = sr
79 transition1 st i1 = st
80
81 fin1 : States1 → Bool
82 fin1 st = true
83 fin1 ss = false
84 fin1 sr = false
85
86 am1 : Automaton States1 In2
87 am1 = record { δ = transition1 ; aend = fin1 }
88
89
90 example1-1 = accept am1 sr ( i0 ∷ i1 ∷ i0 ∷ [] )
91 example1-2 = accept am1 sr ( i1 ∷ i1 ∷ i1 ∷ [] )
92 34
93 reachable : { Q : Set } { Σ : Set } 35 reachable : { Q : Set } { Σ : Set }
94 → (M : Automaton Q Σ ) 36 → (M : Automaton Q Σ )
95 → (astart q : Q ) 37 → (astart q : Q )
96 → (L : List Σ ) → Set 38 → (L : List Σ ) → Set
97 reachable M astart q L = moves M astart L ≡ q 39 reachable M astart q L = moves M astart L ≡ q
98 40
99 example1-3 = reachable am1 sr st ( i1 ∷ i1 ∷ i1 ∷ [] )
100
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 ( λ () )
106
107 inputnn : { n : ℕ } → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ
108 inputnn {zero} {_} _ _ s = s
109 inputnn {suc n} x y s = x ∷ ( inputnn {n} x y ( y ∷ s ) )
110
111 -- lemmaNN : { Q : Set } { Σ : Set } → (M : Automaton Q Σ) → ¬ accept M ( inputnn {n} x y [] )
112 -- lemmaNN = ?
113