|
37
|
1 -title: 正規表現
|
|
|
2
|
|
|
3 --受理集合と演算
|
|
|
4
|
|
|
5 automaton で受理されるのは文字列。あるautomatonnは受理される文字列の集合を決める。
|
|
|
6
|
|
|
7 文字列の集合への演算を考えよう
|
|
|
8
|
|
|
9 x 文字列そのもの
|
|
|
10 x+y 文字列の結合
|
|
|
11 * 文字列の繰り返し
|
|
|
12 x|y 文字列の選択
|
|
|
13
|
|
|
14 これらを使って文字列の集合を決めると、それは文字列に対するパターンマッチとなる。
|
|
|
15
|
|
|
16 これを正規表現という。
|
|
|
17
|
|
|
18 ---正規表現の例
|
|
|
19
|
|
|
20 + は省略しても良いことにしよう。a+b+c の代わりに、
|
|
|
21
|
|
|
22 abc
|
|
|
23
|
|
|
24 文字集合の要素を全部選択したものを . と書くことにしよう。(Shell では?が多い。* は .* を意味する)
|
|
|
25
|
|
|
26 .*abc
|
|
|
27
|
|
|
28 .*abcabc
|
|
|
29
|
|
|
30 曖昧さを避けるために()を使う。
|
|
|
31
|
|
|
32 (abc|bcd)
|
|
|
33
|
|
|
34 .*(abc|bcd)
|
|
|
35
|
|
|
36 --問題5.1
|
|
|
37
|
|
|
38 egrep / Perl などを使って、これらのパターンに対するテストプログラムを作成せよ。C で書くとどうなるか?
|
|
|
39
|
|
|
40 C の regcomp を使ってみよ。
|
|
|
41
|
|
|
42 Option : 実行時間を測定してみよう。
|
|
|
43
|
|
|
44 --正規表現を表すデータ構造
|
|
|
45
|
|
|
46 再帰的な構文木を表すには data を使うことができる。
|
|
|
47
|
|
|
48 data Regex ( Σ : Set ) : Set where
|
|
|
49 _* : Regex Σ → Regex Σ
|
|
|
50 _&_ : Regex Σ → Regex Σ → Regex Σ
|
|
|
51 _||_ : Regex Σ → Regex Σ → Regex Σ
|
|
|
52 <_> : Σ → Regex Σ
|
|
|
53
|
|
|
54 List Σ を用いて < 文字列 > とすることもできるが、基本的なデータ構造をなるべく簡単にすることにしよう。
|
|
|
55
|
|
|
56 <a href="../agda/regex1.agda"> regex1.agda </a>
|
|
|
57
|
|
|
58 上の例題は、
|
|
|
59
|
|
|
60 < a > & < b > & < c >
|
|
|
61
|
|
|
62 any = a || b || c
|
|
|
63
|
|
|
64 ( any * ) & ( < a > & < b > & < c > )
|
|
|
65
|
|
|
66 ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
|
|
|
67
|
|
|
68 ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
|
|
|
69
|
|
|
70 ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
|
|
|
71
|
|
|
72 となる。
|
|
|
73
|
|
|
74 --正規言語
|
|
|
75
|
|
|
76 ある正規表現が受け付ける文字列の集合を正規言語という。これは文字列の集合全体 ( List Σ )の部分集合になる。
|
|
|
77 部分集合は Bool への関数として表すことができる。
|
|
|
78
|
|
|
79 List Σ → Bool
|
|
|
80
|
|
|
81 正規言語は以下の論理式で表すことができる。
|
|
|
82
|
|
|
83 regular-language : {Σ : Set} → Regex Σ → List Σ → Bool
|
|
|
84
|
|
|
85 Regex Σはdataなので場合分けとなる。
|
|
|
86
|
|
|
87 例えば、
|
|
|
88
|
|
|
89 _‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool
|
|
|
90 x ‖ y = λ s → x s ∨ y s
|
|
|
91
|
|
|
92 regular-language (x || y) f = ( regular-language x f ) ‖ ( regular-language y f )
|
|
|
93
|
|
|
94 -- < a >
|
|
|
95
|
|
|
96 もし、Σがデータなら (例えば In2 )
|
|
|
97
|
|
|
98 regular-language < h > f (i0 ∷ [] ) = true
|
|
|
99 regular-language < h > f (i1 ∷ [] ) = true
|
|
|
100 regular-language < h > f _ = false
|
|
|
101
|
|
|
102 で良い。そうっでないなら、
|
|
|
103
|
|
|
104 cmp : (x y : Σ )→ Dec ( x ≡ y )
|
|
|
105
|
|
|
106 みたいなのがあれば、
|
|
|
107
|
|
|
108 regular-language < h > (h1 ∷ [] ) with cmp h h1
|
|
|
109 ... | yes _ = true
|
|
|
110 ... | no _ = false
|
|
|
111 regular-language < h > _ = false
|
|
|
112
|
|
|
113 と書ける。Dec は、条件分岐を理由付きで得るためのもの。理由がないと証明できない。
|
|
|
114
|
|
|
115 in Relation.Nullary
|
|
|
116
|
|
|
117 ¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
|
|
|
118 ¬ P = P → ⊥
|
|
|
119
|
|
|
120 -- Decidable relations.
|
|
|
121
|
|
|
122 data Dec {p} (P : Set p) : Set p where
|
|
|
123 yes : ( p : P) → Dec P
|
|
|
124 no : (¬p : ¬ P) → Dec P
|
|
|
125
|
|
|
126 --Finite Set
|
|
|
127
|
|
|
128 有限集合 Fin n は、
|
|
|
129
|
|
|
130 test1 : Fin 2 → Bool
|
|
|
131 test1 0 → true
|
|
|
132 test1 1 → true
|
|
|
133 test1 2 → true
|
|
|
134
|
|
|
135 などのように使いたい。0,1,2 は Data.Nat なのでだめである。Agda には Data.Fin が用意されている。
|
|
|
136
|
|
|
137 data Fin : ℕ → Set where
|
|
|
138 zero : {n : ℕ} → Fin (suc n)
|
|
|
139 suc : {n : ℕ} (i : Fin n) → Fin (suc n)
|
|
|
140
|
|
|
141 実際に test1 がどのようになるかを Agda で確認すると、
|
|
|
142
|
|
|
143 test4 : Fin 2 → Bool
|
|
|
144 test4 zero = { }0
|
|
|
145 test4 (suc zero) = { }1
|
|
|
146 test4 (suc (suc ()))
|
|
|
147
|
|
|
148 ここで () はあり得ない入力を表す。あり得ないので body は空である。
|
|
|
149
|
|
|
150 (Agda での否定を思い出そう)
|
|
|
151
|
|
|
152 --Finite Set の構成
|
|
|
153
|
|
|
154 <a href="../agda/nfa.agda"> nfa.agda </a>
|
|
|
155
|
|
|
156 record FiniteSet ( Q : Set ) { n : ℕ }
|
|
|
157 : Set where
|
|
|
158 field
|
|
|
159 Q←F : Fin n → Q
|
|
|
160 F←Q : Q → Fin n
|
|
|
161 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
|
|
|
162 finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
|
|
|
163 lt0 : (n : ℕ) → n Data.Nat.≤ n
|
|
|
164 lt0 zero = z≤n
|
|
|
165 lt0 (suc n) = s≤s (lt0 n)
|
|
|
166 lt2 : {m n : ℕ} → m < n → m Data.Nat.≤ n
|
|
|
167 lt2 {zero} lt = z≤n
|
|
|
168 lt2 {suc m} {zero} ()
|
|
|
169 lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
|
|
|
170 exists : ( Q → Bool ) → Bool
|
|
|
171 exists p = exists1 n (lt0 n) p where
|
|
|
172 exists1 : (m : ℕ ) → m Data.Nat.≤ n → ( Q → Bool ) → Bool
|
|
|
173 exists1 zero _ _ = false
|
|
|
174 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) ∨ exists1 m (lt2 m<n) p
|
|
|
175
|
|
|
176 finState1 : FiniteSet States1
|
|
|
177 finState1 = record {
|
|
|
178 Q←F = Q←F
|
|
|
179 ; F←Q = F←Q
|
|
|
180 ; finiso→ = finiso→
|
|
|
181 ; finiso← = finiso←
|
|
|
182 } where
|
|
|
183 Q←F : Fin 3 → States1
|
|
|
184 Q←F zero = sr
|
|
|
185 Q←F (suc zero) = ss
|
|
|
186 Q←F (suc (suc zero)) = st
|
|
|
187 Q←F (suc (suc (suc ())))
|
|
|
188 F←Q : States1 → Fin 3
|
|
|
189 F←Q sr = zero
|
|
|
190 F←Q ss = suc (zero)
|
|
|
191 F←Q st = suc ( suc zero )
|
|
|
192 finiso→ : (q : States1) → Q←F (F←Q q) ≡ q
|
|
|
193 finiso→ sr = refl
|
|
|
194 finiso→ ss = refl
|
|
|
195 finiso→ st = refl
|
|
|
196 finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f
|
|
|
197 finiso← zero = refl
|
|
|
198 finiso← (suc zero) = refl
|
|
|
199 finiso← (suc (suc zero)) = refl
|
|
|
200 finiso← (suc (suc (suc ())))
|
|
|
201
|
|
|
202
|
|
|
203
|
|
|
204 -- x & y
|
|
|
205
|
|
|
206 これは
|
|
|
207
|
|
|
208 split : {Σ : Set} → (List Σ → Bool)
|
|
|
209 → ( List Σ → Bool) → List Σ → Bool
|
|
|
210
|
|
|
211 があれば、
|
|
|
212
|
|
|
213 _・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
|
|
|
214 x ・ y = λ z → split x y z
|
|
|
215
|
|
|
216 regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f )
|
|
|
217
|
|
|
218 -- x & y
|
|
|
219
|
|
|
220 repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
|
|
|
221 repeat x [] = true
|
|
|
222 repeat {Σ} x ( h ∷ t ) = split x (repeat {Σ} x) ( h ∷ t )
|
|
|
223
|
|
|
224 regular-language (x *) f = repeat ( regular-language x f )
|
|
|
225
|
|
|
226
|
|
|
227 --split
|
|
|
228
|
|
|
229 split : {Σ : Set} → (List Σ → Bool)
|
|
|
230 → ( List Σ → Bool) → List Σ → Bool
|
|
|
231 split x y [] = x [] ∧ y []
|
|
|
232 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
|
|
|
233 split (λ t1 → x ( ( h ∷ [] ) ++ t1 )) (λ t2 → y t2 ) t
|
|
|
234
|
|
|
235
|
|
|
236 --問題5.2 - 5.7
|
|
|
237
|
|
|
238 いくつかの正規表現に関する例題
|
|
|
239
|
|
|
240 <a href="../exercise/002.html"> 問題5.2 - 5.7 </a> <!--- Exercise 5.2 --->
|
|
|
241
|
|
|
242 <a href=""> </a> <!--- Exercise 5.3 --->
|
|
|
243 <a href=""> </a> <!--- Exercise 5.4 --->
|
|
|
244 <a href=""> </a> <!--- Exercise 5.5 --->
|
|
|
245 <a href=""> </a> <!--- Exercise 5.6 --->
|
|
|
246 <a href=""> </a> <!--- Exercise 5.7 --->
|
|
|
247
|
|
|
248
|
|
|
249
|
|
|
250
|
|
|
251
|
|
|
252
|
|
|
253
|
|
|
254
|
|
|
255
|
|
|
256
|
|
|
257
|
|
|
258
|
|
|
259
|
|
|
260
|
|
|
261
|
