正規表現

Regular 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 > )

となる。

regex1.agda

正規言語

ある正規表現が受け付ける文字列の集合を正規言語という。これは文字列の集合全体 ( List Σ )の部分集合になる。部分集合は Bool への関数として表すことができる。

    List Σ → Bool

正規言語は以下の論理式で表すことができる。

   regular-language : {Σ : Set} → Regex Σ → List Σ → Bool

Regex Σは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

いくつかの正規表現に関する例題

問題5.2 - 5.7