-title: 正規表現

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 Σ を用いて < 文字列 > とすることもできるが、基本的なデータ構造をなるべく簡単にすることにしよう。

<a href="../agda/regex.agda"> regex.agda </a>

上の例題は、

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

となる。

<a href="../agda/regex1.agda"> regex1.agda </a>

--正規言語

ある正規表現が受け付ける文字列の集合を正規言語という。これは文字列の集合全体 ( 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

--begin-comment:

教科書の定義の通りに定義するべき

    regular-language (x & y) f =  ( regular-language x g )  ∧ ( regular-language y h )
           ∧ ( g ++ h ≡ f )

    record Concat {Σ : Set}  (x y : List Σ → Bool ) (f : List Σ) : Set where
       field 
          g h : List Σ
          f=gh : g ++ h ≡ f  
          match  : ( regular-language x g )  ∧ ( regular-language y h ) ≡ true

--end-comment:



これは 

    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

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

<a href="../exercise/002.html"> 問題5.2 - 5.7 </a>  <!---  Exercise 5.2 --->

<a href=""> </a>  <!---  Exercise 5.3 --->
<a href=""> </a>  <!---  Exercise 5.4 --->
<a href=""> </a>  <!---  Exercise 5.5 --->
<a href=""> </a>  <!---  Exercise 5.6 --->
<a href=""> </a>  <!---  Exercise 5.7 --->

--begin-comment:

正規表現がどんな文字列にマッチするかという問題

マッチして欲しいパターンに対する正規表現を作る問題

--end-comment: