-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 Σ を用いて < 文字列 > とすることもできるが、基本的なデータ構造をなるべく簡単にすることにしよう。
regex1.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 Σ → 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 の構成
nfa.agda
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 問題5.2 - 5.7