-title: 正規表現

--受理集合と演算

automaton で受理されるのは文字列。あるautomatonnは受理される文字列の集合を決める。

文字列の集合への演算を考えよう

   x      文字列そのもの
   x+y    文字列の結合
   *      文字列の繰り返し
   x|y    文字列の選択

これらを使って文字列の集合を決めると、それは文字列に対するパターンマッチとなる。

これを正規表現という。

---正規表現の例

+ は省略しても良いことにしよう。a+b+c  の代わりに、

   abc

文字集合の要素を全部選択したものを . と書くことにしよう。(Shell では?が多い。* は .* を意味する)

   .*abc

   .*abcabc

曖昧さを避けるために()を使う。

   (abc|bcd)

   .*(abc|bcd)

--問題5.1

egrep / Perl などを使って、これらのパターンに対するテストプログラムを作成せよ。C で書くとどうなるか?

C の regcomp を使ってみよ。

Option : 実行時間を測定してみよう。

--正規表現を表すデータ構造

再帰的な構文木を表すには data を使うことができる。

    data Regex   ( Σ : Set  ) : Set  where
       _*    : Regex  Σ → Regex  Σ
       _&_   : Regex  Σ → Regex  Σ → Regex Σ
       _||_  : Regex  Σ → Regex  Σ → Regex Σ
       <_>   : Σ → Regex  Σ

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

<a href="../agda/regex1.agda"> regex1.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 > )

となる。

--正規言語

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

    List Σ → Bool

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

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

Regex Σはdataなので場合分けとなる。

例えば、

    _‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool
    x ‖ y = λ s → x s ∨ y s

    regular-language (x || y) f = ( regular-language x f ) ‖ ( regular-language y f )

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

--Finite Set

有限集合 Fin n は、

    test1 : Fin 2 → Bool
    test1 0 → true
    test1 1 → true
    test1 2 → true

などのように使いたい。0,1,2 は Data.Nat なのでだめである。Agda には Data.Fin が用意されている。

    data Fin : ℕ → Set where
      zero : {n : ℕ} → Fin (suc n)
      suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

実際に test1 がどのようになるかを Agda で確認すると、

    test4 : Fin 2 → Bool
    test4 zero = { }0
    test4 (suc zero) = { }1
    test4 (suc (suc ()))

ここで () はあり得ない入力を表す。あり得ないので body は空である。

(Agda での否定を思い出そう)

--Finite Set の構成

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

    record FiniteSet ( Q : Set ) { n : ℕ }
            : Set  where
         field
            Q←F : Fin n → Q
            F←Q : Q → Fin n
            finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
            finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
         lt0 : (n : ℕ) →  n Data.Nat.≤ n
         lt0 zero = z≤n
         lt0 (suc n) = s≤s (lt0 n)
         lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
         lt2 {zero} lt = z≤n
         lt2 {suc m} {zero} ()
         lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
         exists : ( Q → Bool ) → Bool
         exists p = exists1 n (lt0 n) p where
             exists1 : (m : ℕ ) → m Data.Nat.≤ n  → ( Q → Bool ) → Bool
             exists1  zero  _ _ = false
             exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) ∨ exists1 m (lt2 m<n) p

    finState1 : FiniteSet States1
    finState1 = record {
            Q←F = Q←F
          ; F←Q  = F←Q
          ; finiso→ = finiso→
          ; finiso← = finiso←
       } where
           Q←F : Fin 3 → States1
           Q←F zero = sr
           Q←F (suc zero) = ss
           Q←F (suc (suc zero)) = st
           Q←F (suc (suc (suc ())))
           F←Q : States1 → Fin 3
           F←Q sr = zero
           F←Q ss = suc (zero)
           F←Q st = suc ( suc zero )
           finiso→ : (q : States1) → Q←F (F←Q q) ≡ q
           finiso→ sr = refl
           finiso→ ss = refl
           finiso→ st = refl
           finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f
           finiso← zero = refl
           finiso← (suc zero) = refl
           finiso← (suc (suc zero)) = refl
           finiso← (suc (suc (suc ())))



-- x & y

これは 

    split : {Σ : Set} → (List Σ → Bool)
          → ( List Σ → Bool) → List Σ → Bool

があれば、

    _・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
    x ・ y = λ z → split x y z

    regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f )

-- x & y

    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 )


--split

    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


--問題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 --->