正規表現
MenuRegular language は union / concat / * について閉じているので、この演算を使って構築する方法がある。
受理集合と演算
x 文字列そのもの x+y 文字列の結合 * 文字列の繰り返し x|y 文字列の選択これらを使って文字列の集合を決めると、それは文字列に対するパターンマッチとなる。
これを正規表現という。
正規表現の例
+ は省略しても良いことにしよう。a+b+c の代わりに、
abc文字集合の要素を全部選択したものを . と書くことにしよう。(Shell では?が多い。* は .* を意味する)
.*abc .*abcabc曖昧さを避けるために()を使う。
(abc|bcd) .*(abc|bcd)
問題5.1
egrep / Perl などを使って、これらのパターンに対するテストプログラムを作成せよ。C で書くとどうなるか?
C の regcomp を使ってみよ。
Option : 実行時間を測定してみよう。
(a|b)*a(a|b)n(a|b)n は(a|b)のn個の連続は指数関数時間がかか4ることが知られている。 ReDOS 攻撃と呼ばれている。
正規表現を表すデータ構造
再帰的な構文木を表すには data を使うことができる。
data Regex ( Σ : Set ) : Set where _* : Regex Σ → Regex Σ _&_ : Regex Σ → Regex Σ → Regex Σ _||_ : Regex Σ → Regex Σ → Regex Σ <_> : Σ → Regex ΣList Σ を用いて < 文字列 > とすることもできるが、基本的なデータ構造をなるべく簡単にすることにしよう。
regex.agda 上の例題は、
< a > & < b > & < c > any = a || b || c ( any * ) & ( < a > & < b > & < c > ) ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > ) ( < a > & < b > & < c > ) || ( < b > & < c > & < d > ) ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )となる。
正規言語
ある正規表現が受け付ける文字列の集合を正規言語という。これは文字列の集合全体 ( List Σ )の部分集合になる。部分集合は Bool への関数として表すことができる。
List Σ → Bool正規言語は以下の論理式で表すことができる。
regular-language : {Σ : Set} → Regex Σ → List Σ → BoolRegex Σはdataなので場合分けとなる。
< a >
もし、Σがデータなら (例えば In2 )
regular-language < h > f (i0 ∷ [] ) = true regular-language < h > f (i1 ∷ [] ) = true regular-language < h > f _ = falseで良い。そうでないなら、
cmp : (x y : Σ )→ Dec ( x ≡ y )みたいなのがあれば、
regular-language < h > (h1 ∷ [] ) with cmp h h1 ... | yes _ = true ... | no _ = false regular-language < h > _ = falseと書ける。Dec は、条件分岐を理由付きで得るためのもの。理由がないと証明できない。
in Relation.Nullary
¬_ : ∀ {ℓ} → Set ℓ → Set ℓ ¬ P = P → ⊥ -- Decidable relations. data Dec {p} (P : Set p) : Set p where yes : ( p : P) → Dec P no : (¬p : ¬ P) → Dec P
x || Y
regular-language (x || y) f = ( regular-language x f ) ∨ ( regular-language y f )
x & y
これは
split : {Σ : Set} → (List Σ → Bool) → ( List Σ → Bool) → List Σ → Bool split x y [] = x [] ∧ y [] split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨ split (λ t1 → x ( ( h ∷ [] ) ++ t1 )) (λ t2 → y t2 ) tがあれば、
regular-language (x & y) cmp = split ( λ z → regular-language x cmp z ) (λ z → regular-language y cmp z )
x *
repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool repeat x [] = true repeat {Σ} x ( h ∷ t ) = split x (repeat {Σ} x) ( h ∷ t ) regular-language (x *) f = repeat ( regular-language x f )
問題5.2 - 5.7
いくつかの正規表現に関する例題