|
37
|
1 -title: 決定性オートマトン
|
|
|
2
|
|
163
|
3 数学の本に書いてあることを Agda で定義してみる。なるべく、数学の本に近くする。
|
|
|
4
|
|
|
5 Agda は関数型言語なので、数字の添字を使うものは合わない。そのあたりは修正する。
|
|
|
6
|
|
|
7 Agda は直観主義論理なので、排他律が成立しない。存在を示すには構成的、つまり関数で構成する必要がある。
|
|
|
8
|
|
|
9 数学の本でも、構成的な証明かどうかは(選択公理を使っているかどうかなどで)区別されていることが多い。
|
|
|
10
|
|
37
|
11 -- Automaton オートマトンの定義 ( Q, Σ, σ, q0, F )
|
|
|
12
|
|
163
|
13 教科書では以下のようになっている。
|
|
|
14
|
|
37
|
15 1. Q is a finte set calles states
|
|
|
16 2. Σ is a finte set calles alphabet
|
|
|
17 3. δ : Q x Σ is the transition function
|
|
|
18 4. q0 ∈ Q is the start state
|
|
|
19 5. F ⊆ Q is the set of accept states
|
|
|
20
|
|
|
21 これを Agda で表すには record を使う。
|
|
|
22
|
|
|
23 record Automaton ( Q : Set ) ( Σ : Set )
|
|
|
24 : Set where
|
|
|
25 field
|
|
|
26 δ : Q → Σ → Q
|
|
|
27 aend : Q → Bool
|
|
|
28
|
|
163
|
29 どれがどこにん対応しているかを確認しよう。
|
|
|
30
|
|
37
|
31 <a href="../agda/automaton.agda"> automaton.agda </a>
|
|
65
|
32 <br>
|
|
|
33 <a href="../agda/logic.agda"> logic.agda </a>
|
|
|
34 <br>
|
|
37
|
35
|
|
|
36 record は名前のついた数学的構造で、二つの集合 Q と Σの関係定義する関数からなる。
|
|
|
37
|
|
|
38 record は直積で複数の集合の組だが、ここでは関係を表す論理式/関数の型の組になっている。
|
|
|
39
|
|
|
40 δ : Q → Σ → Q
|
|
|
41
|
|
|
42 は関数で、引数を二つ持っている。ここでは論理式ではない。入力となるaplhabet(文字) とstate (状態)から次の状態を指定する関数である。
|
|
|
43 transition function (状態遷移関数)と呼ばれる。
|
|
|
44
|
|
|
45 aend : Q → Bool
|
|
|
46
|
|
|
47 これはQの部分集合を指定している。Bool は
|
|
|
48
|
|
|
49 data Bool : Set where
|
|
|
50 true : Bool
|
|
|
51 false : Bool
|
|
|
52
|
|
326
|
53 で、true false の二つの要素を持つ集合である。(これでどうして部分集合になるのか? F ⊆ Q を Agda ではどう定義するべきか? Set を使わないのはなぜか)
|
|
37
|
54
|
|
63
|
55 start state はrecordで定義しない方が便利だと言うことがこの後わかる。
|
|
|
56
|
|
37
|
57 --オートマトンの入力
|
|
|
58
|
|
|
59 オートマトンの入力は文字列である。文字列を表すには List を用いる。
|
|
|
60
|
|
|
61 data List (A : Set ) : Set where
|
|
|
62 [] : List A
|
|
|
63 _∷_ : A → List A → List A
|
|
|
64
|
|
|
65 l2 = a ∷ b ∷ a ∷ c ∷ []
|
|
|
66
|
|
|
67 だったことを思い出そう。(Agda のbuiltinのListは ∷ を使う)
|
|
|
68
|
|
|
69
|
|
|
70 --状態遷移
|
|
|
71
|
|
|
72 状態遷移関数をListに適用する。
|
|
|
73
|
|
|
74 moves : { Q : Set } { Σ : Set }
|
|
|
75 → Automaton Q Σ
|
|
|
76 → Q → List Σ → Q
|
|
|
77 moves {Q} { Σ} M q L = move q L
|
|
|
78 where
|
|
|
79 move : (q : Q ) ( L : List Σ ) → Q
|
|
|
80 move q [] = q
|
|
|
81 move q ( H ∷ T ) = move ( (δ M) q H ) T
|
|
|
82
|
|
|
83 List に沿って、状態が変わる。
|
|
|
84
|
|
|
85 accept : { Q : Set } { Σ : Set }
|
|
|
86 → Automaton Q Σ
|
|
63
|
87 → (astart : Q)
|
|
37
|
88 → List Σ → Bool
|
|
63
|
89 accept {Q} { Σ} M astart L = move astart L
|
|
37
|
90 where
|
|
|
91 move : (q : Q ) ( L : List Σ ) → Bool
|
|
|
92 move q [] = aend M q
|
|
|
93 move q ( H ∷ T ) = move ( (δ M) q H ) T
|
|
|
94
|
|
63
|
95
|
|
37
|
96 最後の状態が aend ならば accept される。これらを、record Automaton 内で定義しても良い。
|
|
|
97
|
|
|
98 ---具体的なオートマトン
|
|
|
99
|
|
|
100 reccord Automaton は抽象的なオートマトンで実装がない。(Java/C++ の abstract classと同じ)
|
|
|
101 実装を与えるには、record のfield の型を持つ関数を与えれば良い。
|
|
|
102
|
|
|
103 まず、状態と文字を定義する。
|
|
|
104
|
|
|
105 data States1 : Set where
|
|
|
106 sr : States1
|
|
|
107 ss : States1
|
|
|
108 st : States1
|
|
|
109
|
|
|
110 data In2 : Set where
|
|
|
111 i0 : In2
|
|
|
112 i1 : In2
|
|
|
113
|
|
|
114 状態遷移関数と accept state を作ろう。
|
|
|
115
|
|
|
116 transition1 : States1 → In2 → States1
|
|
|
117 transition1 sr i0 = sr
|
|
|
118 transition1 sr i1 = ss
|
|
|
119 transition1 ss i0 = sr
|
|
|
120 transition1 ss i1 = st
|
|
|
121 transition1 st i0 = sr
|
|
|
122 transition1 st i1 = st
|
|
|
123
|
|
|
124 fin1 : States1 → Bool
|
|
|
125 fin1 st = true
|
|
|
126 fin1 _ = false
|
|
|
127
|
|
|
128 st になればok。record は以下のように作る。
|
|
|
129
|
|
|
130 am1 : Automaton States1 In2
|
|
63
|
131 am1 = record { δ = transition1 ; aend = fin1 }
|
|
37
|
132
|
|
|
133 これを動かすには、
|
|
|
134
|
|
|
135 example1-1 = accept am1 ( i0 ∷ i1 ∷ i0 ∷ [] )
|
|
|
136 example1-2 = accept am1 ( i1 ∷ i1 ∷ i1 ∷ [] )
|
|
|
137
|
|
|
138 とする。( example1-1 の型は何か?)
|
|
|
139
|
|
163
|
140 <a href="../agda/automaton-ex.agda"> Agda による Automaton の例題 </a>
|
|
|
141
|
|
37
|
142 --問題 3.1
|
|
|
143
|
|
|
144 教科書のAutomatonの例のいくつかを Agda で定義してみよ。
|
|
|
145
|
|
|
146 accept される入力と accept されない入力を示し、Agda で true false を確認せよ。
|
|
|
147
|
|
|
148 <a href=""> </a> <!--- Exercise 3.1 --->
|
|
|
149
|
|
|
150
|
|
59
|
151 --Regular Language
|
|
37
|
152
|
|
163
|
153 Automaton は List Σ に対して true / false を返す。つまり、文字列の部分集合を決定する。
|
|
59
|
154
|
|
163
|
155 文字列の部分集合を (Automaton の専門用語として) Language という。でたらめの発声の部分集合が日本語なので言語といえなくもない。
|
|
|
156
|
|
326
|
157 language : { Σ : Set } → Set
|
|
|
158 language {Σ} = List Σ → Bool
|
|
|
159
|
|
163
|
160 なんらかのAutomaton が受け付ける文字列の部分集合を Regular Language という。この範囲に収まらない Language も後で調べる。
|
|
59
|
161
|
|
326
|
162
|
|
|
163 --Agda によるRegular Languageの集合演算
|
|
|
164
|
|
|
165 何かのAutomaton で判定される言語は ∃ automaton だが、これを record で書く。
|
|
|
166
|
|
|
167 record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
|
|
|
168 field
|
|
|
169 states : Set
|
|
|
170 astart : states
|
|
|
171 automaton : Automaton states Σ
|
|
|
172 contain : List Σ → Bool
|
|
|
173 contain x = accept automaton astart x
|
|
|
174
|
|
|
175 contain が language の定義の形になっていることを確認しよう。
|
|
|
176
|
|
59
|
177 --Regular Languageの演算
|
|
|
178
|
|
163
|
179 Regular Languageは以下の演算に付いて閉じていることが知られている。閉じているとは以下の集合演算をしても、それはやはり
|
|
|
180 Regular Language つまり、Automaton で、その集合に入っているかどうかを判定できる。
|
|
59
|
181
|
|
163
|
182 二つの文字列集合から、その結合を集める Concatenation
|
|
59
|
183
|
|
163
|
184 文字列の集合の和集合 Union
|
|
|
185
|
|
|
186 結合の繰り返し Star
|
|
59
|
187
|
|
65
|
188 <a href="../agda/regular-language.agda"> Agda での Regular Language </a>
|
|
59
|
189
|
|
326
|
190 Union は Bool 演算を使って簡単に表される。
|
|
163
|
191
|
|
|
192 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
193 Union {Σ} A B x = (A x ) \/ (B x)
|
|
|
194
|
|
|
195 Concat はそんなに簡単ではない。ある文字列が、前半はAの要素で、後半がBの要素であれば良いのだが、
|
|
|
196
|
|
|
197 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
198 Concat {Σ} A B x = ?
|
|
|
199
|
|
|
200 前半と後半の分け方には非決定性がある。
|
|
|
201
|
|
326
|
202 --Split による List の分割
|
|
163
|
203
|
|
|
204 i0 ∷ i1 ∷ i0 ∷ [] の分け方は and と or で以下のようになる。
|
|
|
205
|
|
|
206 ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/
|
|
|
207 ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/
|
|
|
208 ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
|
|
|
209 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B [] )
|
|
|
210
|
|
326
|
211 Agda は高階論理なので、これを任意長の List に対して定義できる。
|
|
163
|
212
|
|
|
213 split : {Σ : Set} → (List Σ → Bool)
|
|
|
214 → ( List Σ → Bool) → List Σ → Bool
|
|
|
215 split x y [] = x [] /\ y []
|
|
|
216 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/
|
|
|
217 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
218
|
|
|
219 これが、実際に文字列の分解になっていることを確認する。
|
|
|
220
|
|
|
221 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
|
|
|
222 ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/
|
|
|
223 ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/
|
|
|
224 ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
|
|
|
225 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B [] )
|
|
|
226 )
|
|
|
227 test-AB→split {_} {A} {B} = refl
|
|
|
228
|
|
|
229 これを使って Concat と Star を書ける。
|
|
|
230
|
|
|
231 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
232 Concat {Σ} A B = split A B
|
|
|
233
|
|
|
234 {-# TERMINATING #-}
|
|
|
235 Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
|
|
326
|
236 Star {Σ} A [] = true
|
|
|
237 Star {Σ} A (h ∷ t) = split A ( Star {Σ} A ) (h ∷ t)
|
|
163
|
238
|
|
326
|
239 {-# TERMINATING #-}は Agda が停止性を判定できないというエラーを抑止するのだった。
|
|
163
|
240
|
|
|
241 --Union が RegularLanguage で閉じていること
|
|
|
242
|
|
|
243 RegularLanguage かどうかは以下の命題を作れるかどうかでわかる。
|
|
|
244
|
|
|
245 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
|
|
|
246 isRegular A x r = A x ≡ contain r x
|
|
|
247
|
|
|
248 たとえば Union に付いて閉じているかどうかは
|
|
|
249
|
|
|
250 closed-in-union : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
|
|
|
251
|
|
|
252 とかける。この時に
|
|
|
253
|
|
|
254 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
|
|
|
255
|
|
|
256 で、これは Automaton を具体的に作る必要がある。
|
|
|
257
|
|
326
|
258 この証明は M-Union の定義とUnionが同じことなので簡単に証明できる。
|
|
163
|
259
|
|
|
260
|
|
|
261 --Concat が RegularLanguage で閉じていること
|
|
|
262
|
|
|
263 これは割と難しい。Automaton の状態が有限であることが必要になる。
|
|
|
264
|
|
326
|
265 A x ≡ contain r x は両辺が true の場合と false の場合がある。これを示すことになる。
|
|
163
|
266
|
|
326
|
267 ≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
|
|
|
268
|
|
|
269 をつかって
|
|
163
|
270
|
|
326
|
271 closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
|
|
|
272 closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
|
|
|
273 closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
|
|
|
274 closed-in-concat→ = ?
|
|
|
275 closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
|
|
|
276 closed-in-concat← = ?
|
|
163
|
277
|
|
326
|
278 とする。
|
|
|
279
|
|
|
280 問題は M-Concat A B つまり、Concat を受け付ける automaton をどうやって定義するかになる。
|
|
|
281
|
|
|
282 これは次の lecture で行う。
|
|
|
283
|
|
|
284 --Star が RegularLanguage で閉じていること
|
|
|
285
|
|
|
286 これも問題は上と同じだが...
|
|
|
287
|
