|
0
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
|
2 module automaton where
|
|
|
3 open import Level hiding ( suc ; zero )
|
|
|
4 open import Data.Empty
|
|
|
5 open import Relation.Nullary
|
|
|
6 open import Relation.Binary.PropositionalEquality -- hiding (_⇔_)
|
|
|
7 open import logic
|
|
|
8 open import Data.List
|
|
|
9
|
|
|
10 record Automaton {n : Level} (Q : Set n) (Σ : Set ) : Set ((Level.suc n) ) where
|
|
|
11 field
|
|
|
12 δ : Q → Σ → Q
|
|
|
13 F : Q → Set
|
|
|
14
|
|
|
15 open Automaton
|
|
|
16
|
|
|
17 accept : {n : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → Q → List Σ → Set
|
|
2
|
18 accept {n} {Q} {Σ} atm q [] = F atm q
|
|
|
19 accept {n} {Q} {Σ} atm q (x ∷ input) =
|
|
0
|
20 accept atm (δ atm q x ) input
|
|
|
21
|
|
18
|
22 -- data Dec' {n : Level} (P : Set n) : Set n where -- Law of Exclude Middle / LEM
|
|
|
23 -- yes' : (p : P ) → Dec' P
|
|
|
24 -- no' : (p : ¬ P ) → Dec' P
|
|
|
25
|
|
|
26 record Automaton-Language {n : Level} (Q : Set n) (Σ : Set ) : Set ((Level.suc n) ) where
|
|
|
27 field
|
|
|
28 ATM : Automaton Q Σ
|
|
|
29 field
|
|
|
30 startq : Q
|
|
|
31 decF : (q : Q) → Dec (F ATM q )
|
|
|
32 accept-by : (x : List Σ ) → (q : Q) → Dec ( accept ATM q x)
|
|
|
33 -- Accept : (x : List Σ ) → accept-by x startq where
|
|
|
34 -- accept-by : (x : List Σ ) → (q : Q) → Dec ( accept ATM q x)
|
|
|
35 -- accept-by [] q = decF q
|
|
|
36 -- accept-by (x ∷ t) q = accept-by t (δ ATM q x)
|
|
|
37
|
|
0
|
38 trace : {n : Level} {Q : Set n} {Σ : Set } → (A : Automaton Q Σ) → (start : Q) → (input : List Σ ) → accept A start input → List Q
|
|
|
39 trace {n} {Q} {Σ} A q [] a = q ∷ []
|
|
|
40 trace {n} {Q} {Σ} A q (x ∷ t) a = q ∷ ( trace A (δ A q x) t a )
|
|
|
41
|
|
18
|
42 trace' : {n : Level} {Q : Set n} {Σ : Set } → (A : Automaton Q Σ) → (start : Q) → (input : List Σ ) → List Q
|
|
|
43 trace' {n} {Q} {Σ} A q [] = q ∷ []
|
|
|
44 trace' {n} {Q} {Σ} A q (x ∷ t) = q ∷ ( trace' A (δ A q x) t )
|
|
|
45
|
|
0
|
46 data Q3 : Set where
|
|
|
47 q₁ : Q3
|
|
|
48 q₂ : Q3
|
|
|
49 q₃ : Q3
|
|
|
50
|
|
|
51 data Σ2 : Set where
|
|
|
52 s0 : Σ2
|
|
|
53 s1 : Σ2
|
|
|
54
|
|
|
55 δ16 : Q3 → Σ2 → Q3
|
|
|
56 δ16 q₁ s0 = q₁
|
|
|
57 δ16 q₁ s1 = q₂
|
|
|
58 δ16 q₂ s0 = q₃
|
|
|
59 δ16 q₂ s1 = q₂
|
|
|
60 δ16 q₃ s0 = q₂
|
|
|
61 δ16 q₃ s1 = q₂
|
|
|
62
|
|
|
63 δ16' : Q3 → Σ2 → Q3
|
|
|
64 δ16' q₁ s0 = q₁
|
|
|
65 δ16' q₁ s1 = q₂
|
|
|
66 δ16' q₂ s0 = q₃
|
|
|
67 δ16' q₂ s1 = q₂
|
|
|
68 δ16' q₃ s0 = q₂
|
|
|
69 δ16' q₃ s1 = q₃
|
|
|
70
|
|
|
71 data a16end : Q3 → Set where
|
|
|
72 a16q2 : a16end q₂
|
|
|
73
|
|
|
74 a16 : Automaton Q3 Σ2
|
|
1
|
75 a16 = record { δ = δ16 ; F = λ q → a16end q }
|
|
0
|
76
|
|
|
77 a16' : Automaton Q3 Σ2
|
|
1
|
78 a16' = record { δ = δ16' ; F = λ q → q ≡ q₂ }
|
|
0
|
79
|
|
|
80 --
|
|
|
81 -- ∷ → ∷ → ∷ → []
|
|
|
82 -- ↓ ↓ ↓
|
|
|
83 -- s0 s0 s1
|
|
|
84 --
|
|
|
85 input1 : List Σ2
|
|
|
86 input1 = s0 ∷ s0 ∷ s1 ∷ []
|
|
|
87
|
|
|
88 input2 : List Σ2
|
|
|
89 input2 = s0 ∷ s0 ∷ s0 ∷ []
|
|
|
90
|
|
|
91 test1 : accept a16 q₁ input1
|
|
|
92 test1 = a16q2
|
|
|
93
|
|
|
94 lemma0 : accept a16 q₁ input1 ≡ a16end q₂
|
|
|
95 lemma0 = begin
|
|
|
96 accept a16 q₁ ( s0 ∷ s0 ∷ s1 ∷ [] )
|
|
|
97 ≡⟨ refl ⟩ -- x ≡ x
|
|
|
98 accept a16 q₁ ( s0 ∷ s1 ∷ [] )
|
|
|
99 ≡⟨⟩
|
|
|
100 accept a16 q₁ ( s1 ∷ [] )
|
|
|
101 ≡⟨⟩
|
|
|
102 accept a16 q₂ []
|
|
|
103 ≡⟨⟩
|
|
|
104 a16end q₂
|
|
|
105 ∎ where open ≡-Reasoning
|
|
|
106
|
|
|
107 lemma1 : List Q3
|
|
|
108 lemma1 = trace a16 q₁ input1 a16q2
|
|
|
109
|
|
|
110 test1' : accept a16' q₁ input1
|
|
|
111 test1' = refl
|
|
|
112
|
|
|
113 lemma2 : List Q3
|
|
|
114 lemma2 = trace a16' q₁ input1 refl
|
|
|
115
|
|
|
116 test2 : ¬ ( accept a16 q₁ input2 )
|
|
|
117 test2 ()
|
|
|
118
|
|
|
119 open import Data.Bool
|
|
|
120 open import Data.Unit
|
|
|
121
|
|
|
122 -- contains at least 1 s1
|
|
|
123 c1 : List Σ2 → Set
|
|
|
124 c1 [] = ⊥
|
|
|
125 c1 (s1 ∷ t) = ⊤
|
|
|
126 c1 (_ ∷ t) = c1 t
|
|
|
127
|
|
|
128 -- even number of s0
|
|
|
129 even0 : List Σ2 → Set
|
|
|
130 odd0 : List Σ2 → Set
|
|
|
131 odd0 [] = ⊥
|
|
|
132 odd0 (s0 ∷ t) = even0 t
|
|
|
133 odd0 (s1 ∷ t) = odd0 t
|
|
|
134 even0 [] = ⊤
|
|
|
135 even0 (s0 ∷ t) = odd0 t
|
|
|
136 even0 (s1 ∷ t) = even0 t
|
|
|
137
|
|
|
138 -- after
|
|
|
139
|
|
|
140 a0 : List Σ2 → Set
|
|
|
141 a0 [] = ⊥
|
|
|
142 a0 (s1 ∷ t ) = even0 t
|
|
|
143 a0 (s0 ∷ t ) = a0 t
|
|
|
144
|
|
|
145 -- data ⊥ : Set
|
|
|
146 --
|
|
|
147 -- data ⊤ : Set where
|
|
|
148 -- tt : ⊤
|
|
|
149 -- tt : ⊤
|
|
|
150
|
|
|
151 lemma-a : (x : List Σ2 ) → accept a16' q₁ x → a0 x
|
|
|
152 lemma-a x a = a1 x a where
|
|
|
153 a3 : (x : List Σ2 ) → accept a16' q₃ x → odd0 x
|
|
|
154 a2 : (x : List Σ2 ) → accept a16' q₂ x → even0 x
|
|
|
155 a3 [] ()
|
|
|
156 a3 (s0 ∷ t) a = a2 t a
|
|
|
157 a3 (s1 ∷ t) a = a3 t a
|
|
|
158 a2 [] a = tt
|
|
|
159 a2 (s0 ∷ t) a = a3 t a
|
|
|
160 a2 (s1 ∷ t) a = a2 t a
|
|
|
161 a1 : (x : List Σ2 ) → accept a16' q₁ x → a0 x
|
|
|
162 a1 [] () -- a16' does not accept []
|
|
|
163 a1 (s0 ∷ t) a = a1 t a
|
|
|
164 a1 (s1 ∷ t) a = a2 t a
|
|
|
165
|
|
|
166 -- ¬_ : Set → Set
|
|
|
167 -- ¬_ _ = ⊥
|
|
|
168
|
|
|
169 lemma-not-a : ¬ ( (x : List Σ2 ) → accept a16 q₁ x → a0 x )
|
|
|
170 lemma-not-a not1 with not1 (s1 ∷ s0 ∷ s1 ∷ [] ) a16q2
|
|
|
171 ... | ()
|
|
|
172
|
|
|
173 -- can we prove negation similar to the lemma-a?
|
|
|
174 -- lemma-not-a' : ¬ ((x : List Σ2 ) → accept a16 q₁ x → a0 x)
|
|
|
175 -- lemma-not-a' not = {!!} where
|
|
|
176 -- a3 : (x : List Σ2 ) → accept a16 q₃ x → odd0 x
|
|
|
177 -- a2 : (x : List Σ2 ) → accept a16 q₂ x → even0 x
|
|
|
178 -- a3 (s0 ∷ t) a = a2 t a
|
|
|
179 -- a3 (s1 ∷ t) a = {!!}
|
|
|
180 -- a2 [] a = tt
|
|
|
181 -- a2 (s0 ∷ t) a = a3 t a
|
|
|
182 -- a2 (s1 ∷ t) a = a2 t a
|
|
|
183 -- a1 : (x : List Σ2 ) → accept a16 q₁ x → a0 x
|
|
|
184 -- a1 [] ()
|
|
|
185 -- a1 (s0 ∷ t) a = a1 t a
|
|
|
186 -- a1 (s1 ∷ t) a = a2 t a
|
|
|
187
|
|
|
188 open import Data.Nat
|
|
|
189
|
|
|
190 evenℕ : ℕ → Set
|
|
|
191 oddℕ : ℕ → Set
|
|
|
192 oddℕ zero = ⊥
|
|
|
193 oddℕ (suc n) = evenℕ n
|
|
|
194 evenℕ zero = ⊤
|
|
|
195 evenℕ (suc n) = oddℕ n
|
|
|
196
|
|
|
197 count-s0 : (x : List Σ2 ) → ℕ
|
|
|
198 count-s0 [] = zero
|
|
|
199 count-s0 (s0 ∷ t) = suc ( count-s0 t )
|
|
|
200 count-s0 (s1 ∷ t) = count-s0 t
|
|
|
201
|
|
|
202 e1 : (x : List Σ2 ) → even0 x → evenℕ ( count-s0 x )
|
|
|
203 o1 : (x : List Σ2 ) → odd0 x → oddℕ ( count-s0 x )
|
|
|
204 e1 [] e = tt
|
|
|
205 e1 (s0 ∷ t) o = o1 t o
|
|
|
206 e1 (s1 ∷ t) e = e1 t e
|
|
|
207 o1 [] ()
|
|
|
208 o1 (s0 ∷ t) e = e1 t e
|
|
|
209 o1 (s1 ∷ t) o = o1 t o
|
|
|
210
|
|
|
211 δ19 : Q3 → Σ2 → Q3
|
|
|
212 δ19 q₁ s0 = q₁
|
|
|
213 δ19 q₁ s1 = q₂
|
|
|
214 δ19 q₂ s0 = q₁
|
|
|
215 δ19 q₂ s1 = q₂
|
|
|
216 δ19 q₃ _ = q₁
|
|
|
217
|
|
|
218 a19 : Automaton Q3 Σ2
|
|
1
|
219 a19 = record { δ = δ19 ; F = λ q → q ≡ q₁ }
|
|
0
|
220
|
|
|
221 -- input is empty or ends in s0
|
|
|
222
|
|
|
223 end0 : List Σ2 → Set
|
|
|
224 end0 [] = ⊤
|
|
|
225 end0 (s0 ∷ [] ) = ⊤
|
|
|
226 end0 (s1 ∷ [] ) = ⊥
|
|
|
227 end0 (x ∷ t ) = end0 t
|
|
|
228
|
|
|
229 lemma-b : (x : List Σ2 ) → accept a19 q₁ x → end0 x
|
|
|
230 lemma-b = {!!}
|
|
|
231
|
