|
37
|
1 -title: 正規表現
|
|
|
2
|
|
326
|
3 Regular language は union / concat / * について閉じているので、この演算を
|
|
|
4 使って構築する方法がある。
|
|
|
5
|
|
37
|
6 --受理集合と演算
|
|
|
7
|
|
|
8 x 文字列そのもの
|
|
|
9 x+y 文字列の結合
|
|
|
10 * 文字列の繰り返し
|
|
|
11 x|y 文字列の選択
|
|
|
12
|
|
|
13 これらを使って文字列の集合を決めると、それは文字列に対するパターンマッチとなる。
|
|
|
14
|
|
|
15 これを正規表現という。
|
|
|
16
|
|
|
17 ---正規表現の例
|
|
|
18
|
|
|
19 + は省略しても良いことにしよう。a+b+c の代わりに、
|
|
|
20
|
|
|
21 abc
|
|
|
22
|
|
|
23 文字集合の要素を全部選択したものを . と書くことにしよう。(Shell では?が多い。* は .* を意味する)
|
|
|
24
|
|
|
25 .*abc
|
|
|
26
|
|
|
27 .*abcabc
|
|
|
28
|
|
|
29 曖昧さを避けるために()を使う。
|
|
|
30
|
|
|
31 (abc|bcd)
|
|
|
32
|
|
|
33 .*(abc|bcd)
|
|
|
34
|
|
|
35 --問題5.1
|
|
|
36
|
|
|
37 egrep / Perl などを使って、これらのパターンに対するテストプログラムを作成せよ。C で書くとどうなるか?
|
|
|
38
|
|
|
39 C の regcomp を使ってみよ。
|
|
|
40
|
|
|
41 Option : 実行時間を測定してみよう。
|
|
|
42
|
|
326
|
43 (a|b)*a(a|b)n
|
|
|
44
|
|
|
45 (a|b)n は(a|b)のn個の連続は指数関数時間がかか4ることが知られている。 ReDOS 攻撃と呼ばれている。
|
|
|
46
|
|
37
|
47 --正規表現を表すデータ構造
|
|
|
48
|
|
|
49 再帰的な構文木を表すには data を使うことができる。
|
|
|
50
|
|
|
51 data Regex ( Σ : Set ) : Set where
|
|
|
52 _* : Regex Σ → Regex Σ
|
|
|
53 _&_ : Regex Σ → Regex Σ → Regex Σ
|
|
|
54 _||_ : Regex Σ → Regex Σ → Regex Σ
|
|
|
55 <_> : Σ → Regex Σ
|
|
|
56
|
|
|
57 List Σ を用いて < 文字列 > とすることもできるが、基本的なデータ構造をなるべく簡単にすることにしよう。
|
|
|
58
|
|
326
|
59 <a href="../agda/regex.agda"> regex.agda </a>
|
|
37
|
60
|
|
|
61 上の例題は、
|
|
|
62
|
|
|
63 < a > & < b > & < c >
|
|
|
64
|
|
|
65 any = a || b || c
|
|
|
66
|
|
|
67 ( any * ) & ( < a > & < b > & < c > )
|
|
|
68
|
|
|
69 ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
|
|
|
70
|
|
|
71 ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
|
|
|
72
|
|
|
73 ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
|
|
|
74
|
|
|
75 となる。
|
|
|
76
|
|
326
|
77 <a href="../agda/regex1.agda"> regex1.agda </a>
|
|
|
78
|
|
37
|
79 --正規言語
|
|
|
80
|
|
|
81 ある正規表現が受け付ける文字列の集合を正規言語という。これは文字列の集合全体 ( List Σ )の部分集合になる。
|
|
|
82 部分集合は Bool への関数として表すことができる。
|
|
|
83
|
|
|
84 List Σ → Bool
|
|
|
85
|
|
|
86 正規言語は以下の論理式で表すことができる。
|
|
|
87
|
|
|
88 regular-language : {Σ : Set} → Regex Σ → List Σ → Bool
|
|
|
89
|
|
|
90 Regex Σはdataなので場合分けとなる。
|
|
|
91
|
|
|
92
|
|
|
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
|
|
326
|
102 で良い。そうでないなら、
|
|
37
|
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
|
|
331
|
126 -- x || Y
|
|
|
127
|
|
|
128
|
|
|
129 regular-language (x || y) f = ( regular-language x f ) ∨ ( regular-language y f )
|
|
|
130
|
|
37
|
131
|
|
|
132 -- x & y
|
|
|
133
|
|
331
|
134 --begin-comment:
|
|
|
135
|
|
|
136 教科書の定義の通りに定義するべき
|
|
|
137
|
|
|
138 regular-language (x & y) f = ( regular-language x g ) ∧ ( regular-language y h )
|
|
|
139 ∧ ( g ++ h ≡ f )
|
|
|
140
|
|
|
141 record Concat {Σ : Set} (x y : List Σ → Bool ) (f : List Σ) : Set where
|
|
|
142 field
|
|
|
143 g h : List Σ
|
|
|
144 f=gh : g ++ h ≡ f
|
|
|
145 match : ( regular-language x g ) ∧ ( regular-language y h ) ≡ true
|
|
|
146
|
|
|
147 --end-comment:
|
|
|
148
|
|
|
149
|
|
|
150
|
|
37
|
151 これは
|
|
|
152
|
|
|
153 split : {Σ : Set} → (List Σ → Bool)
|
|
|
154 → ( List Σ → Bool) → List Σ → Bool
|
|
326
|
155 split x y [] = x [] ∧ y []
|
|
|
156 split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨
|
|
|
157 split (λ t1 → x ( ( h ∷ [] ) ++ t1 )) (λ t2 → y t2 ) t
|
|
|
158
|
|
37
|
159
|
|
|
160 があれば、
|
|
|
161
|
|
326
|
162 regular-language (x & y) cmp = split ( λ z → regular-language x cmp z ) (λ z → regular-language y cmp z )
|
|
37
|
163
|
|
326
|
164 -- x *
|
|
37
|
165
|
|
|
166 repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
|
|
|
167 repeat x [] = true
|
|
|
168 repeat {Σ} x ( h ∷ t ) = split x (repeat {Σ} x) ( h ∷ t )
|
|
|
169
|
|
|
170 regular-language (x *) f = repeat ( regular-language x f )
|
|
|
171
|
|
|
172
|
|
|
173
|
|
|
174 --問題5.2 - 5.7
|
|
|
175
|
|
|
176 いくつかの正規表現に関する例題
|
|
|
177
|
|
|
178 <a href="../exercise/002.html"> 問題5.2 - 5.7 </a> <!--- Exercise 5.2 --->
|
|
|
179
|
|
|
180 <a href=""> </a> <!--- Exercise 5.3 --->
|
|
|
181 <a href=""> </a> <!--- Exercise 5.4 --->
|
|
|
182 <a href=""> </a> <!--- Exercise 5.5 --->
|
|
|
183 <a href=""> </a> <!--- Exercise 5.6 --->
|
|
|
184 <a href=""> </a> <!--- Exercise 5.7 --->
|
|
|
185
|
|
331
|
186 --begin-comment:
|
|
|
187
|
|
|
188 正規表現がどんな文字列にマッチするかという問題
|
|
|
189
|
|
|
190 マッチして欲しいパターンに対する正規表現を作る問題
|
|
|
191
|
|
|
192 --end-comment:
|
|
37
|
193
|
|
|
194
|
|
|
195
|
|
|
196
|
|
|
197
|
|
|
198
|
|
|
199
|
|
|
200
|
|
|
201
|
|
|
202
|
|
|
203
|
|
|
204
|
|
|
205
|
