-title: 正規表現とオートマトン 正規表現は、Automaton と同じ言語であることが期待される。つまり、  正規表現から、それと同じ language を受け付ける Automaton を作ればよい。 --ε遷移と非決定性オートマトンの合成による方法 教科書にはこの方法が記述されている。 文字の入力がなくても状態遷移が可能であるとすると、オートマトンの組合せが楽になる。 文字を消費しない遷移を ε遷移と言う。ε遷移可能な状態をまとめて一つの状態と見れば、ε遷移のないNFAに変換できる。 そして、それを subset construction で DFA にすれば良い。 実際に、M-Concat などで合成を実行することができる。 しかし、もう少し直接的な方法も存在する。 --微分法 ある正規表現を考えた時に、それを   空列を受け付けるかどうか   個々の文字列を一文字受け付けたらどうなるか と考える。
まず空列を受け付けるかどうか判定する。 empty? : Regex Σ → Bool empty? ε = true empty? φ = false empty? (x *) = true empty? (x & y) = empty? x /\ empty? y empty? (x || y) = empty? x \/ empty? y empty? < x > = false 正規表現の変形を実行する derivative : Regex Σ → Σ → Regex Σ derivative ε s = φ derivative φ s = φ derivative (x *) s with derivative x s ... | ε = x * ... | φ = φ ... | t = t & (x *) derivative (x & y) s with empty? x ... | true with derivative x s | derivative y s ... | ε | φ = φ ... | ε | t = y || t ... | φ | t = t ... | x1 | φ = x1 & y ... | x1 | y1 = (x1 & y) || y1 derivative (x & y) s | false with derivative x s ... | ε = y ... | φ = φ ... | t = t & y derivative (x || y) s with derivative x s | derivative y s ... | φ | y1 = y1 ... | x1 | φ = x1 ... | x1 | y1 = x1 || y1 derivative < x > s with eq? x s ... | yes _ = ε ... | no _ = φ ここで、 eq? : (x y : Σ) → Dec (x ≡ y) があることを使っている。 これの繰り返しで選れる正規表現の集合を data を使って表現できる。 data regex-states (x : Regex Σ ) : Regex Σ → Set where unit : regex-states x x derive : { y : Regex Σ } → regex-states x y → (s : Σ) → regex-states x ( derivative y s ) record Derivative (x : Regex Σ ) : Set where field state : Regex Σ is-derived : regex-states x state これを状態にして Automaton を構成できる。 regex→automaton : (r : Regex Σ) → Automaton (Derivative r) Σ regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive-step d s} ; aend = λ d → empty? (state d) } where derive-step : (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s) derive-step d0 s = derive (is-derived d0) s 実際に match を実行するには以下のようにする。 regex-match : (r : Regex Σ) → (List Σ) → Bool regex-match ex is = accept ( regex→automaton ex ) record { state = ex ; is-derived = unit } is ここではいくつかの問題が残っている。   生成される状態は有限か? (つまり微分法は停止するのか) 停止するかどうかに関係なく、regex-match は具体的な有限文字列に対して実行可能である。 ただし、Agda では具体的ではない文字列も用意できる。 微分法で定義した Automaton は、正規表現でしていされた言語に一致するのか? これも証明する必要がある。 --オートマトンから正規表現を生成する 状態遷移の条件を正規表現した一般化オートマトンを考える。 普通のオートマトンから始めて、状態を組み合わせて遷移条件を正規表現にしていく。 状態が一つになったら正規表現が得られる。 --実際の正規表現エンジン grep のソースコード --Boyer-Moore Search 固定文字列を検索するなら、正規表現よりも高速な手法がある。 例えば、engine を検索するとする。   6文字目がeでなければ、先頭の文字列からengineであることはない なので、6文字見なくてもだめなことはわかる。しかし、7文字目からengineを探すと、   xxxxxn   the engine を見落とす可能性がある。つまり、   6文字目が検索文字列に含まれる文字列だと途中からマッチする可能性がある 何文字目からマッチする可能性があるかは、あらかじめ調べることができる。   e 6文字目   n 2文字目   g 3文字目   i 4文字目   ? 7文字目 これを繰り返せば良い。   .*engine をDFAに変換して探す場合とどれくらい速度が違うか調べてみよう。 --複数文字列に対する Boyer-Moore Search ---問題6.1 正規表現の決定性オートマトンへの変換 例題